NYLL
Module

ProjSpace_exists_forall_subsingleton_HSucc_twist.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_forall_subsingleton_HSucc_twist
18 declarations indexed from sourceView source ↗

Module documentation

Proj Space exists forall subsingleton HSucc twist

Imports8
Imported by4

Declarations

def

idxEquiv

L61 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.idxEquiv
Documentation

The index equivalence removing the universe lift from tuples in the pulled-back standard cover.

Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
Lean source · full declaration
def idxEquiv (i : ℕ) : (ProjSpace.stdCoverPullback φ).Idx i ≃ ProjSpaceCech.Idx N i where
  toFun s := ⟨fun k => (s.1 k).down, fun _ _ h => (s.2 h : _)⟩
  invFun s := ⟨fun k => ULift.up (s.1 k), fun _ _ h => (s.2 h : _)⟩
  left_inv _ := Subtype.ext rfl
  right_inv _ := Subtype.ext rfl
theorem

img_nonempty

L67 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.img_nonempty
Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
omit [IsAffineHom φ] in
Lean source · statement
theorem img_nonempty {i : ℕ} (s : ProjSpaceCech.Idx N i) : (ProjSpaceCech.Idx.img N s).Nonempty
theorem

inter_eq

L70 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.inter_eq
Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
Lean source · statement
theorem inter_eq (i : ℕ) (s : (ProjSpace.stdCoverPullback φ).Idx i) :
    (ProjSpace.stdCoverPullback φ).inter s = ⨅ j ∈ ProjSpaceCech.Idx.img N (idxEquiv φ i s),
      ProjSpace.pullbackChart φ j
theorem

twistRes_val

L79 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.twistRes_val
Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
omit [IsAffineHom φ] in
Lean source · statement
theorem twistRes_val {U V : X.Opens} (h : U ≤ V) (g : ProjSpace.twistObj π φ m V) (i : Fin (N + 1))
  :
    (ProjSpace.twistRes π φ m h g).val i = ProjSpace.restrictFun (inf_le_inf_right _ h) (g.val i)
theorem

twistRes_twistRes

L84 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.twistRes_twistRes
Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
omit [IsAffineHom φ] in
Lean source · statement
theorem twistRes_twistRes {U V W : X.Opens} (h : U ≤ V) (h' : V ≤ W) (g : ProjSpace.twistObj π φ m
  W) :
    ProjSpace.twistRes π φ m h (ProjSpace.twistRes π φ m h' g) = ProjSpace.twistRes π φ m (h.trans
      h') g
theorem

twistRes_self

L91 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.twistRes_self
Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
omit [IsAffineHom φ] in
Lean source · statement
theorem twistRes_self {U : X.Opens} (h : U ≤ U) (g : ProjSpace.twistObj π φ m U) :
  ProjSpace.twistRes π φ m h g = g
def

chainFwd

L101 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.chainFwd
Documentation

The cochain map from shifted graded sections to twisted sections on the pulled-back standard cover.

Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
Lean source · statement
def chainFwd (i : ℕ) :
    ProjSpaceCech.GradedModule.cochain ((ProjSpace.twistGradedModule φ π).shift (m : ℤ)) i
      →ₗ[A] (ProjSpace.twist π φ m).cochain (ProjSpace.stdCoverPullback φ) i
def

chainBwd

L112 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.chainBwd
Documentation

The inverse cochain map from twisted sections on the standard cover to shifted graded sections.

Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
Lean source · statement
def chainBwd (i : ℕ) :
    (ProjSpace.twist π φ m).cochain (ProjSpace.stdCoverPullback φ) i
      →ₗ[A] ProjSpaceCech.GradedModule.cochain ((ProjSpace.twistGradedModule φ π).shift (m : ℤ)) i
theorem

chainFwd_apply

L121 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.chainFwd_apply
Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
Lean source · statement
theorem chainFwd_apply (i : ℕ) (f : ProjSpaceCech.GradedModule.cochain
  ((ProjSpace.twistGradedModule φ π).shift (m : ℤ)) i)
    (s : (ProjSpace.stdCoverPullback φ).Idx i) :
    chainFwd φ π m i f s = ProjSpace.twistRes π φ m (inter_eq φ i s).le
      ((AlgebraicGeometry.ProjSpace.exists_sec_shift_twistGradedModule_equiv φ π m).choose
        (ProjSpaceCech.Idx.img N (idxEquiv φ i s)) (img_nonempty _) (f (idxEquiv φ i s)))
theorem

chainBwd_apply

L128 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.chainBwd_apply
Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
Lean source · statement
theorem chainBwd_apply (i : ℕ) (g : (ProjSpace.twist π φ m).cochain (ProjSpace.stdCoverPullback φ)
  i) (s : ProjSpaceCech.Idx N i) :
    chainBwd φ π m i g s = ((AlgebraicGeometry.ProjSpace.exists_sec_shift_twistGradedModule_equiv φ
      π m).choose (ProjSpaceCech.Idx.img N s) (img_nonempty s)).symm
      (ProjSpace.twistRes π φ m (inter_eq φ i ((idxEquiv φ i).symm s)).ge (g ((idxEquiv φ i).symm
        s)))
def

chainEquiv

L139 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.chainEquiv
Documentation

The linear equivalence between shifted graded cochains and twisted cochains on the standard cover.

Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
Lean source · statement
def chainEquiv (i : ℕ) :
    ProjSpaceCech.GradedModule.cochain ((ProjSpace.twistGradedModule φ π).shift (m : ℤ)) i
      ≃ₗ[A] (ProjSpace.twist π φ m).cochain (ProjSpace.stdCoverPullback φ) i
theorem

chainEquiv_apply

L163 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.chainEquiv_apply
Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
Lean source · statement
theorem chainEquiv_apply (i : ℕ) (f : ProjSpaceCech.GradedModule.cochain
  ((ProjSpace.twistGradedModule φ π).shift (m : ℤ)) i)
    (s : (ProjSpace.stdCoverPullback φ).Idx i) :
    chainEquiv φ π m i f s = ProjSpace.twistRes π φ m (inter_eq φ i s).le
      ((AlgebraicGeometry.ProjSpace.exists_sec_shift_twistGradedModule_equiv φ π m).choose
        (ProjSpaceCech.Idx.img N (idxEquiv φ i s)) (img_nonempty _) (f (idxEquiv φ i s)))
theorem

idxEquiv_face

L170 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.idxEquiv_face
Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
Lean source · statement
theorem idxEquiv_face (i : ℕ) (s : (ProjSpace.stdCoverPullback φ).Idx (i + 1)) (j : Fin (i + 2)) :
    idxEquiv φ i ((ProjSpace.stdCoverPullback φ).face s j) = ProjSpaceCech.Idx.face N (idxEquiv φ
      (i + 1) s) j
theorem

chainEquiv_comm

L174 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.chainEquiv_comm
Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
Lean source · statement
theorem chainEquiv_comm (i : ℕ) (f : ProjSpaceCech.GradedModule.cochain
  ((ProjSpace.twistGradedModule φ π).shift (m : ℤ)) i) :
    chainEquiv φ π m (i + 1) (ProjSpaceCech.GradedModule.d _ i f)
      = (ProjSpace.twist π φ m).d (ProjSpace.stdCoverPullback φ) i (chainEquiv φ π m i f)
theorem

nonempty_H_equiv_HSucc

L197 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.Pack.nonempty_H_equiv_HSucc
Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace Pack
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (π : X ⟶ Spec
    (.of A)) (m : ℕ)
Lean source · statement
theorem nonempty_H_equiv_HSucc (i : ℕ) :
    Nonempty (ProjSpaceCech.GradedModule.H ((ProjSpace.twistGradedModule φ π).shift (m : ℤ)) (i + 1)
      ≃ₗ[A] (ProjSpace.twist π φ m).HSucc (ProjSpace.stdCoverPullback φ) i)
theorem

sat_shift

L231 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.TV.sat_shift
Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace TV
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsFinite φ] (π : X ⟶ Spec
    (.of A))
omit [IsNoetherianRing A] [IsFinite φ] in
Lean source · statement
theorem sat_shift {M' : ProjSpaceCech.GradedModule A N} (ψ : ProjSpaceCech.GradedModule.Hom M'
  (ProjSpace.twistGradedModule φ π))
    (hsat : ∀ (j : Fin (N + 1)) (e : ℤ), ∀ x ∈ (ProjSpace.twistGradedModule φ π).grade e,
      ∃ k : ℕ, ∃ x' ∈ M'.grade (e + k), ψ.toLinearMap x' = ((ProjSpace.twistGradedModule φ π).xMul
        j ^ k) x) (m : ℕ) :
    ∀ (j : Fin (N + 1)) (e : ℤ), ∀ x ∈ ((ProjSpace.twistGradedModule φ π).shift (m : ℤ)).grade e,
      ∃ k : ℕ, ∃ x' ∈ (M'.shift (m : ℤ)).grade (e + k),
        (ψ.shift (m : ℤ)).toLinearMap x' = (((ProjSpace.twistGradedModule φ π).shift (m : ℤ)).xMul
          j ^ k) x
theorem

exists_forall_subsingleton_HSucc_twist

L246 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_forall_subsingleton_HSucc_twist.AlgebraicGeometry.ProjSpace.TV.exists_forall_subsingleton_HSucc_twist
Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
noncomputable section
open CategoryTheory Opposite MvPolynomial HomogeneousLocalization TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace TV
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] [IsNoetherianRing A] {N : ℕ} {X : Scheme.{u}}
  (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsFinite φ] (π : X ⟶ Spec
    (.of A))
Lean source · statement
theorem exists_forall_subsingleton_HSucc_twist (hπ : φ ≫ ProjSpace.π A N = π) :
    ∃ m₀ : ℕ, ∀ m : ℕ, m₀ ≤ m → ∀ i : ℕ,
      Subsingleton ((ProjSpace.twist π φ m).HSucc (ProjSpace.stdCoverPullback φ) i)
theorem

exists_forall_subsingleton_HSucc_twist

L267 ↗
AlgebraicGeometry.ProjSpace.exists_forall_subsingleton_HSucc_twist
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_forall_subsingleton_HSucc_twist
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
Lean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.exists_forall_subsingleton_HSucc_twist
    {A : Type u} [CommRing A] [IsNoetherianRing A] {N : ℕ} {X : Scheme.{u}}
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsFinite φ]
    (π : X ⟶ Spec (.of A)) (hπ : φ ≫ ProjSpace.π A N = π) :
    ∃ m₀ : ℕ, ∀ m : ℕ, m₀ ≤ m → ∀ i : ℕ,
      Subsingleton ((ProjSpace.twist π φ m).HSucc (ProjSpace.stdCoverPullback φ) i)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.