NYLL
Module

Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.lean

Nyll.SchemeTheory.Cohomology.Cech.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
27 declarations indexed from sourceView source ↗

Module documentation

Degree-zero exactness of the affine-cover Cech complex

Sections on an open are exactly the degree-zero cochains whose Cech differential vanishes. The increasing-index construction is compared with the finite-subset description.

Imports5
Imported by6

Declarations

abbrev

altImg

L55 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altImg
Documentation

The finite set of cover indices occurring in an increasing Cech tuple.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
abbrev altImg {i : ℕ} (s : K.Idx i) : Finset K.ι
theorem

card_altImg

L58 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.card_altImg
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem card_altImg {i : ℕ} (s : K.Idx i) :
    (altImg K s).card = i + 1
theorem

altIdx_canonical

L62 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altIdx_canonical
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altIdx_canonical {i : ℕ} (s : K.Idx i) :
    s.1 = (altImg K s).orderEmbOfFin (card_altImg K s)
theorem

altIdx_eq_of_altImg

L66 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altIdx_eq_of_altImg
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altIdx_eq_of_altImg {i : ℕ} {s t : K.Idx i}
    (h : altImg K s = altImg K t) : s = t
theorem

altOpen_eq_biInf

L73 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altOpen_eq_biInf
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altOpen_eq_biInf {i : ℕ} (s : K.Idx i) :
    K.inter s = ⨅ j ∈ altImg K s, K.U j
theorem

altImg_altFace

L80 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altImg_altFace
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altImg_altFace {i : ℕ} (s : K.Idx (i + 1))
    (j : Fin (i + 2)) :
    altImg K (K.face s j)
      = (altImg K s).erase (s.1 j)
def

altOfFinset

L95 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altOfFinset
Documentation

The increasing Cech tuple obtained by enumerating a finite set of the required cardinality.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
def altOfFinset {i : ℕ} (T : Finset K.ι) (hT : T.card = i + 1) :
    K.Idx i
theorem

altImg_altOfFinset

L99 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altImg_altOfFinset
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altImg_altOfFinset {i : ℕ} (T : Finset K.ι) (hT : T.card = i + 1) :
    altImg K (altOfFinset K T hT) = T
theorem

altImg_deg0

L103 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altImg_deg0
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altImg_deg0 (σ : K.Idx 0) :
    altImg K σ = {σ.1 0}
def

altPos

L110 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altPos
Documentation

The position of a member of the finite index set in its increasing Cech tuple.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
def altPos {i : ℕ} (s : K.Idx i) (j : K.ι)
    (hj : j ∈ altImg K s) : Fin (i + 1)
theorem

altIdx_val_altPos

L114 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altIdx_val_altPos
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altIdx_val_altPos {i : ℕ} (s : K.Idx i)
    (j : K.ι) (hj : j ∈ altImg K s) :
    s.1 (altPos K s j hj) = j
theorem

altPos_val

L120 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altPos_val
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altPos_val {i : ℕ} (s : K.Idx i) (p : Fin (i + 1)) :
    altPos K s (s.1 p) (Finset.mem_image_of_mem _ (Finset.mem_univ p)) = p
def

altInsert

L125 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altInsert
Documentation

Insert a new cover index and enumerate the enlarged finite set in increasing order.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
def altInsert {i : ℕ} (s : K.Idx i) (j : K.ι)
    (hj : j ∉ altImg K s) : K.Idx (i + 1)
theorem

altImg_altInsert

L130 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altImg_altInsert
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altImg_altInsert {i : ℕ} (s : K.Idx i)
    (j : K.ι) (hj : j ∉ altImg K s) :
    altImg K (altInsert K s j hj)
      = insert j (altImg K s)
def

insPos

L137 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.insPos
Documentation

The position of the new cover index in the increasing tuple obtained by insertion.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
def insPos {i : ℕ} (s : K.Idx i) (j : K.ι)
    (hj : j ∉ altImg K s) : Fin (i + 2)
theorem

altInsert_val_insPos

L142 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altInsert_val_insPos
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altInsert_val_insPos {i : ℕ} (s : K.Idx i)
    (j : K.ι) (hj : j ∉ altImg K s) :
    (altInsert K s j hj).1 (insPos K s j hj) = j
theorem

altFace_altInsert_insPos

L147 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altFace_altInsert_insPos
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altFace_altInsert_insPos {i : ℕ} (s : K.Idx i)
    (j : K.ι) (hj : j ∉ altImg K s) :
    K.face (altInsert K s j hj)
      (insPos K s j hj) = s
theorem

altPos_congr

L155 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altPos_congr
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altPos_congr {i : ℕ} {s t : K.Idx i}
    (h : s = t) (j : K.ι) (hjs : j ∈ altImg K s)
    (hjt : j ∈ altImg K t) :
    altPos K s j hjs = altPos K t j hjt
theorem

altInsert_altFace_altPos

L161 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altInsert_altFace_altPos
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altInsert_altFace_altPos {i : ℕ} (σ : K.Idx (i + 1))
    (j : K.ι) (hj : j ∈ altImg K σ)
    (hjp : j ∉ altImg K
      (K.face σ (altPos K σ j hj))) :
    altInsert K (K.face σ (altPos K σ j hj))
      j hjp = σ
theorem

insPos_altFace_altPos

L171 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.insPos_altFace_altPos
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem insPos_altFace_altPos {i : ℕ} (σ : K.Idx (i + 1))
    (j : K.ι) (hj : j ∈ altImg K σ)
    (hjp : j ∉ altImg K
      (K.face σ (altPos K σ j hj))) :
    insPos K (K.face σ (altPos K σ j hj)) j hjp
      = altPos K σ j hj
theorem

altFace_altInsert_ne

L181 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altFace_altInsert_ne
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altFace_altInsert_ne {i : ℕ} (s : K.Idx (i + 1))
    (j : K.ι) (hj : j ∉ altImg K s)
    (k : Fin (i + 3)) (hk : k ≠ insPos K s j hj) :
    ∃ (p : Fin (i + 2)) (hjp : j ∉ altImg K (K.face s p)),
      K.face (altInsert K s j hj) k
        = altInsert K (K.face s p) j hjp
      ∧ (altInsert K s j hj).1 k = s.1 p
theorem

res_refl

L211 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.res_refl
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section ResHelpers
variable {V : Scheme.{u}}
Lean source · statement
theorem res_refl {O : V.Opens} (h : O ≤ O) (x : Γ(V, O)) :
    (V.presheaf.map (homOfLE h).op).hom x = x
theorem

res_res

L216 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.res_res
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section ResHelpers
variable {V : Scheme.{u}}
Lean source · statement
theorem res_res {O₁ O₂ O₃ : V.Opens} (h12 : O₁ ≤ O₂) (h23 : O₂ ≤ O₃)
    (x : Γ(V, O₃)) :
    (V.presheaf.map (homOfLE h12).op).hom ((V.presheaf.map (homOfLE h23).op).hom x)
      = (V.presheaf.map (homOfLE (h12.trans h23)).op).hom x
theorem

altC_at_eq

L222 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altC_at_eq
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section ResHelpers
variable {V : Scheme.{u}}
Lean source · statement
theorem altC_at_eq {W : V.Opens} {K : Scheme.OrderedAffineCoverOf W}
    {n : ℕ} (z : K.cochain n) {σ τ : K.Idx n} (h : σ = τ)
    {O : V.Opens} (hσ : O ≤ K.inter σ) (hτ : O ≤ K.inter τ) :
    (V.presheaf.map (homOfLE hσ).op).hom (z σ)
      = (V.presheaf.map (homOfLE hτ).op).hom (z τ)
def

idx0

L235 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.idx0
Documentation

The degree-zero Cech index determined by a single cover member.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section Idx0
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι)
Lean source · statement
def idx0 : K.Idx 0
theorem

affine_acyclic₀

L245 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.affine_acyclic₀
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section Acyclic0
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · full declaration
theorem affine_acyclic₀ :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    LinearMap.ker (K.d π 0) = LinearMap.range (K.aug π) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections π
  refine le_antisymm (fun z hz => ?_) ?_
  · have hcov : W ≤ ⨆ σ : K.Idx 0, K.inter σ := by
      refine K.iSup_eq.ge.trans (iSup_le fun i => ?_)
      exact le_iSup_of_le (idx0 K i) (le_iInf fun _ => le_rfl)
    have hcore : ∀ (a b : K.ι), a < b → ∀ (σ τ : K.Idx 0),
        σ.1 0 = a → τ.1 0 = b → ∀ {O : V.Opens}
        (hOσ : O ≤ K.inter σ) (hOτ : O ≤ K.inter τ),
        O ≤ K.U a ⊓ K.U b →
        (V.presheaf.map (homOfLE hOσ).op).hom (z σ)
          = (V.presheaf.map (homOfLE hOτ).op).hom (z τ) := by
      intro a b hab σ τ hσ hτ O hOσ hOτ hOab
      let ρ : K.Idx 1 := ⟨![a, b], by
        intro c d hcd; fin_cases c <;> fin_cases d <;> simp_all⟩
      have hρ0 : K.face ρ 0 = τ := altIdx_eq_of_altImg K
        (by rw [altImg_deg0, altImg_deg0, hτ]; rfl)
      have hρ1 : K.face ρ 1 = σ := altIdx_eq_of_altImg K
        (by rw [altImg_deg0, altImg_deg0, hσ]; rfl)
      have hOρ : O ≤ K.inter ρ :=
        le_iInf fun j => by fin_cases j
                            · exact hOab.trans inf_le_left
                            · exact hOab.trans inf_le_right
      have hker := congrFun (LinearMap.mem_ker.mp hz) ρ
      rw [Scheme.OrderedAffineCoverOf.d_apply, Fin.sum_univ_two] at hker
      simp only [Fin.val_zero, Fin.val_one, pow_zero, pow_one, one_smul, neg_one_smul,
        Pi.zero_apply, add_neg_eq_zero] at hker
      have key := congrArg (V.presheaf.map (homOfLE hOρ).op).hom hker
      rw [res_res, res_res,
        altC_at_eq z hρ0 _ hOτ,
        altC_at_eq z hρ1 _ hOσ] at key
      exact key.symm
    have hcompat : TopCat.Presheaf.IsCompatible V.sheaf.1
        (K.inter (i := 0)) z := by
      intro σ τ
      have hOab : K.inter σ ⊓ K.inter τ
          ≤ K.U (σ.1 0) ⊓ K.U (τ.1 0) :=
        inf_le_inf (iInf_le _ 0) (iInf_le _ 0)
      rcases lt_trichotomy (σ.1 0) (τ.1 0) with h | h | h
      · exact hcore _ _ h σ τ rfl rfl inf_le_left inf_le_right hOab
      · have heq : σ = τ := altIdx_eq_of_altImg K
          (by rw [altImg_deg0, altImg_deg0, h])
        subst heq; rfl
      · exact (hcore _ _ h τ σ rfl rfl inf_le_right inf_le_left
          (hOab.trans (inf_comm _ _).le)).symm
    obtain ⟨w, hw, -⟩ := V.sheaf.existsUnique_gluing' (K.inter (i := 0)) W
      (fun σ => homOfLE (K.inter_le_base σ)) hcov z hcompat
    exact ⟨w, funext fun σ => hw σ⟩
  · rintro _ ⟨w, rfl⟩
    refine LinearMap.mem_ker.mpr (funext fun τ => ?_)
    rw [Scheme.OrderedAffineCoverOf.d_apply, Fin.sum_univ_two]
    simp only [Scheme.OrderedAffineCoverOf.aug, LinearMap.pi_apply,
        Scheme.OrderedAffineCoverOf.res_apply,
      res_res, Fin.val_zero, Fin.val_one, pow_zero, pow_one, one_smul,
      neg_one_smul, Pi.zero_apply, add_neg_cancel]
theorem

ker_d_zero_eq_range_aug

L315 ↗
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.ker_d_zero_eq_range_aug
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
universe u
with_weak_namespace _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open _root_.AlgebraicGeometry
    Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug.AlgebraicGeometry in
with_weak_namespace Scheme_OrderedAffineCoverOf_ker_d_zero_eq_range_aug
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.ker_d_zero_eq_range_aug {R : Type
    u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) {W : V.Opens}
    (K : V.OrderedAffineCoverOf W) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    LinearMap.ker (K.d π 0) = LinearMap.range (K.aug π) :=
  Scheme.OrderedAffineCoverOf.Acyclic.affine_acyclic₀ π K

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