Module

Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.lean

Nyll.SchemeTheory.Cohomology.Cech.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen

53 declarations indexed from sourceView source ↗

Module documentation

Positive-degree exactness of affine-cover Cech cochains

For a separated structure morphism and an affine open, the positive-degree Cech complex of an ordered affine cover of the open is exact.

Imports5

Mathlib.Util.WithWeakNamespace
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.RingTheory.LocalProperties.Submodule
Mathlib.RingTheory.Localization.Away.Basic
Nyll.SchemeTheory.Cohomology.Cech.OrderedAffineCoverOf

Imported by5

abbrev

altImg

L55 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altImg

Documentation

The finite set of chart indices occurring in an ordered Čech index.

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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altOfFinset

Documentation

The ordered Čech index obtained by enumerating a finite set of chart indices.

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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altPos

Documentation

The position of a chart index in an ordered Čech index.

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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altInsert

Documentation

The ordered Čech index obtained by inserting a new chart index.

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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.insPos

Documentation

The position occupied by the inserted chart index.

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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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 τ)

theorem

altOpen_altInsert

L237 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altOpen_altInsert

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_succ_le_range_d_of_isAffineOpen
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 WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀

Lean source · statement

theorem altOpen_altInsert {i : ℕ} (s : K.Idx i)
    (hj : i₀ ∉ altImg K s) :
    K.inter (altInsert K s i₀ hj)
      = K.inter s

def

htpy

L260 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.htpy

Documentation

The Čech contracting homotopy associated to the chart covering the entire base open.

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_succ_le_range_d_of_isAffineOpen
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 WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀

Lean source · full declaration

def htpy (i : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    K.cochain (i + 1) →ₗ[R] K.cochain i :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections π
  LinearMap.pi fun σ =>
    if hσ : i₀ ∈ altImg K σ then 0
    else ((-1 : ℤ) ^ ((insPos K σ i₀ hσ : ℕ))) •
      ((Scheme.OrderedAffineCoverOf.res π
        (ge_of_eq (altOpen_altInsert K i₀ hi₀ σ hσ))).comp
        (LinearMap.proj (R := R) (altInsert K σ i₀ hσ)))

theorem

htpy_apply

L271 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.htpy_apply

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_succ_le_range_d_of_isAffineOpen
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 WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀

Lean source · full declaration

theorem htpy_apply (i : ℕ) (z : K.cochain (i + 1))
    (σ : K.Idx i) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    htpy π K i₀ hi₀ i z σ =
      if hσ : i₀ ∈ altImg K σ then 0
      else ((-1 : ℤ) ^ ((insPos K σ i₀ hσ : ℕ))) •
        (V.presheaf.map (homOfLE (ge_of_eq
          (altOpen_altInsert K i₀ hi₀ σ hσ))).op).hom
          (z (altInsert K σ i₀ hσ)) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections π
  simp only [htpy, LinearMap.pi_apply]
  split_ifs with h
  · rfl
  · simp only [LinearMap.smul_apply, LinearMap.comp_apply, LinearMap.proj_apply,
      Scheme.OrderedAffineCoverOf.res_apply]

theorem

notMem_altImg_altFace

L288 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.notMem_altImg_altFace

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen
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 WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀
omit hi₀ in

Lean source · statement

theorem notMem_altImg_altFace {i : ℕ} (σ : K.Idx (i + 1))
    (hσ : i₀ ∉ altImg K σ) (p : Fin (i + 2)) :
    i₀ ∉ altImg K (K.face σ p)

theorem

sign_rel

L294 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.sign_rel

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen
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 WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀
omit hi₀ in

Lean source · statement

theorem sign_rel {i : ℕ} (σ : K.Idx (i + 1))
    (hσ : i₀ ∉ altImg K σ) (p : Fin (i + 2)) :
    K.face (altInsert K σ i₀ hσ)
        ((insPos K σ i₀ hσ).succAbove p)
      = altInsert K (K.face σ p) i₀
          (notMem_altImg_altFace K i₀ σ hσ p)
    ∧ (insPos K σ i₀ hσ : ℕ)
        + ((insPos K σ i₀ hσ).succAbove p : ℕ)
      = (p : ℕ) + (insPos K (K.face σ p) i₀
          (notMem_altImg_altFace K i₀ σ hσ p) : ℕ) + 1

theorem

htpy_rel

L362 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.htpy_rel

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_succ_le_range_d_of_isAffineOpen
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 WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀

Lean source · full declaration

theorem htpy_rel (i : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    K.d π i ∘ₗ htpy π K i₀ hi₀ i
      + htpy π K i₀ hi₀ (i + 1) ∘ₗ K.d π (i + 1)
      = LinearMap.id := by
  let := Scheme.OrderedAffineCoverOf.moduleSections π
  refine LinearMap.ext fun z => funext fun σ => ?_
  simp only [LinearMap.add_apply, LinearMap.comp_apply, LinearMap.id_apply, Pi.add_apply]
  by_cases hσ : i₀ ∈ altImg K σ
  · rw [htpy_apply π K i₀ hi₀, dite_eq_left hσ, add_zero,
      Scheme.OrderedAffineCoverOf.d_apply]
    set p₀ := altPos K σ i₀ hσ with hp₀
    have hjp₀ : i₀ ∉ altImg K (K.face σ p₀) := by
      rw [altImg_altFace, hp₀, altIdx_val_altPos]
      exact Finset.notMem_erase _ _
    rw [Finset.sum_eq_single p₀]
    · rw [htpy_apply π K i₀ hi₀, dite_eq_right hjp₀,
        insPos_altFace_altPos K σ i₀ hσ hjp₀, map_zsmul, smul_smul,
        ← pow_add, Even.neg_one_pow ⟨_, rfl⟩, one_smul,
        res_res,
        altC_at_eq z (altInsert_altFace_altPos K σ i₀ hσ hjp₀)
          _ le_rfl,
        res_refl]
    · intro j _ hj
      have hjmem : i₀ ∈ altImg K (K.face σ j) := by
        rw [altImg_altFace]
        refine Finset.mem_erase.mpr ⟨fun heq => hj ?_, hσ⟩
        have h1 : σ.1 j = σ.1 p₀ :=
          heq.symm.trans (altIdx_val_altPos K σ i₀ hσ).symm
        exact σ.2.injective h1
      rw [htpy_apply π K i₀ hi₀, dite_eq_left hjmem, map_zero, smul_zero]
    · intro h; exact absurd (Finset.mem_univ _) h
  · rw [htpy_apply π K i₀ hi₀, dite_eq_right hσ,
      Scheme.OrderedAffineCoverOf.d_apply π K (i + 1) z,
      Fin.sum_univ_succAbove _ (insPos K σ i₀ hσ), map_add, smul_add,
      map_zsmul, smul_smul, ← pow_add, Even.neg_one_pow ⟨_, rfl⟩, one_smul,
      res_res,
      altC_at_eq z (altFace_altInsert_insPos K σ i₀ hσ) _ le_rfl,
      res_refl, map_sum, Finset.smul_sum,
      Scheme.OrderedAffineCoverOf.d_apply π K i,
      add_comm (z σ), ← add_assoc, add_eq_right, ← Finset.sum_add_distrib]
    refine Finset.sum_eq_zero fun p _ => ?_
    have hjp := notMem_altImg_altFace K i₀ σ hσ p
    obtain ⟨heq, hparity⟩ := sign_rel K i₀ σ hσ p
    rw [htpy_apply π K i₀ hi₀, dite_eq_right hjp,
      map_zsmul, smul_smul, ← pow_add, res_res,
      map_zsmul, smul_smul, ← pow_add, res_res,
      altC_at_eq z heq _
        ((K.inter_le_inter_face σ p).trans
          (ge_of_eq (altOpen_altInsert K i₀ hi₀ _ hjp))),
      hparity, pow_succ, mul_neg_one, neg_smul, add_neg_cancel]

def

idx0

L416 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.idx0

Documentation

The degree-zero Čech index consisting of the chosen chart.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen
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 WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀
omit hi₀ in

Lean source · statement

def idx0 : K.Idx 0

theorem

altOpen_idx0

L419 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altOpen_idx0

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_succ_le_range_d_of_isAffineOpen
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 WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀

Lean source · statement

theorem altOpen_idx0 :
    K.inter (idx0 K i₀) = W

def

hAug

L424 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.hAug

Documentation

The augmentation given by restriction to the chosen chart covering the base open.

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_succ_le_range_d_of_isAffineOpen
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 WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀

Lean source · full declaration

def hAug :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    K.cochain 0 →ₗ[R] Γ(V, W) :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections π
  (Scheme.OrderedAffineCoverOf.res π (altOpen_idx0 K i₀ hi₀).ge).comp
    (LinearMap.proj (idx0 K i₀))

theorem

htpy_rel₀

L431 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.htpy_rel₀

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_succ_le_range_d_of_isAffineOpen
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 WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀

Lean source · full declaration

theorem htpy_rel₀ :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    (htpy π K i₀ hi₀ 0 ∘ₗ K.d π 0
        + K.aug π ∘ₗ hAug π K i₀ hi₀ = LinearMap.id)
      ∧ hAug π K i₀ hi₀ ∘ₗ K.aug π = LinearMap.id := by
  let := Scheme.OrderedAffineCoverOf.moduleSections π
  have hone : ∀ (a : Fin 2), (a : ℕ) + ((a.succAbove 0 : Fin 2) : ℕ) = 1 := by decide
  have hle_idx0 : ∀ (σ : K.Idx 0),
      K.inter σ ≤ K.inter (idx0 K i₀) :=
    fun σ => (K.inter_le_base σ).trans (altOpen_idx0 K i₀ hi₀).ge
  refine ⟨LinearMap.ext fun z => funext fun σ => ?_, LinearMap.ext fun w => ?_⟩
  · simp only [LinearMap.add_apply, LinearMap.comp_apply, LinearMap.id_apply, Pi.add_apply,
      Scheme.OrderedAffineCoverOf.aug, hAug, LinearMap.pi_apply, LinearMap.proj_apply,
      Scheme.OrderedAffineCoverOf.res_apply, res_res]
    by_cases hσ : i₀ ∈ altImg K σ
    · have hσ0 : σ.1 0 = i₀ := by
        obtain ⟨j, -, hj⟩ := Finset.mem_image.mp hσ; rwa [Fin.fin_one_eq_zero j] at hj
      have hσeq : σ = idx0 K i₀ :=
        Subtype.ext (funext fun j => by rw [Fin.fin_one_eq_zero j]; exact hσ0)
      rw [htpy_apply, dite_eq_left hσ, zero_add,
        altC_at_eq z hσeq.symm (hle_idx0 σ) le_rfl, res_refl]
    · rw [htpy_apply, dite_eq_right hσ, Scheme.OrderedAffineCoverOf.d_apply,
        Fin.sum_univ_succAbove _ (insPos K σ i₀ hσ), Fin.sum_univ_one,
        map_add, smul_add, map_zsmul, smul_smul, ← pow_add, Even.neg_one_pow ⟨_, rfl⟩, one_smul,
        res_res,
        altC_at_eq z (altFace_altInsert_insPos K σ i₀ hσ) _ le_rfl,
        res_refl,
        map_zsmul, smul_smul, ← pow_add, hone, pow_one, neg_one_smul,
        res_res]
      have hne : i₀ ≠ σ.1 0 := fun h =>
        hσ (altImg_deg0 K σ ▸ Finset.mem_singleton.mpr h)
      have hface0 : K.face (altInsert K σ i₀ hσ)
          ((insPos K σ i₀ hσ).succAbove 0) = idx0 K i₀ := by
        apply altIdx_eq_of_altImg
        have hval0 : (altInsert K σ i₀ hσ).1
            ((insPos K σ i₀ hσ).succAbove 0) = σ.1 0 :=
          congrFun (congrArg Subtype.val
            (altFace_altInsert_insPos K σ i₀ hσ)) 0
        rw [altImg_altFace, altImg_altInsert, hval0,
          altImg_deg0, altImg_deg0,
          Finset.erase_insert_of_ne hne]
        simp only [Finset.erase_singleton, Finset.insert_empty]
        rfl
      rw [altC_at_eq z hface0 _ (hle_idx0 σ)]
      abel
  · simp only [LinearMap.comp_apply, LinearMap.id_apply, hAug,
      Scheme.OrderedAffineCoverOf.aug, LinearMap.pi_apply, LinearMap.proj_apply,
      Scheme.OrderedAffineCoverOf.res_apply, res_res, res_refl]

theorem

wholeSpace_exact

L480 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.wholeSpace_exact

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_succ_le_range_d_of_isAffineOpen
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 WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀

Lean source · full declaration

theorem wholeSpace_exact (i : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    LinearMap.ker (K.d π (i + 1))
      ≤ LinearMap.range (K.d π i) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections π
  intro z hz
  have key := htpy_rel π K i₀ hi₀ i
  have : z = K.d π i (htpy π K i₀ hi₀ i z) := by
    have := LinearMap.congr_fun key z
    simp only [LinearMap.add_apply, LinearMap.comp_apply, LinearMap.id_apply,
      LinearMap.mem_ker.mp hz, map_zero, add_zero] at this
    exact this.symm
  exact ⟨_, this.symm⟩

theorem

wholeSpace_exact₀

L494 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.wholeSpace_exact₀

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_succ_le_range_d_of_isAffineOpen
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 WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀

Lean source · full declaration

theorem wholeSpace_exact₀ :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    LinearMap.ker (K.d π 0) = LinearMap.range (K.aug π) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections π
  obtain ⟨hrel, hid⟩ := htpy_rel₀ π K i₀ hi₀
  refine le_antisymm (fun z hz => ?_) ?_
  · have := LinearMap.congr_fun hrel z
    simp only [LinearMap.add_apply, LinearMap.comp_apply, LinearMap.id_apply,
      LinearMap.mem_ker.mp hz, map_zero, zero_add] at this
    exact ⟨_, this⟩
  · 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

isAffineOpen_altOpen

L520 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.isAffineOpen_altOpen

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_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π

Lean source · statement

theorem isAffineOpen_altOpen :
    ∀ {i : ℕ} (σ : K.Idx i),
      IsAffineOpen (K.inter σ)

def

moduleW_altC

L544 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.moduleW_altC

Documentation

The action of sections on the base open on its Čech cochains.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
omit π in

Lean source · statement

def moduleW_altC (i : ℕ) :
    Module Γ(V, W) (K.cochain i)

theorem

smulW_apply

L550 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.smulW_apply

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
omit π in

Lean source · full declaration

theorem smulW_apply {i : ℕ} (a : Γ(V, W)) (x : K.cochain i)
    (σ : K.Idx i) :
    letI := moduleW_altC K i
    (a • x) σ = (V.presheaf.map (homOfLE (K.inter_le_base σ)).op).hom a * x σ :=
  rfl

theorem

altd_smulW

L557 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altd_smulW

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
omit [IsSeparated π] in

Lean source · full declaration

theorem altd_smulW (i : ℕ) (a : Γ(V, W)) (x : K.cochain i) :
    letI := moduleW_altC K i
    letI := moduleW_altC K (i + 1)
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    K.d π i (a • x) = a • K.d π i x := by
  let := Scheme.OrderedAffineCoverOf.moduleSections π
  funext τ
  rw [Scheme.OrderedAffineCoverOf.d_apply, smulW_apply, Scheme.OrderedAffineCoverOf.d_apply,
    Finset.mul_sum]
  refine Finset.sum_congr rfl fun j _ => ?_
  rw [smulW_apply, map_mul, res_res, mul_smul_comm]

def

rangeW

L570 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.rangeW

Documentation

The Čech coboundaries as a submodule over sections on the base open.

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_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π

Lean source · full declaration

def rangeW (p : ℕ) :
    letI := moduleW_altC K (p + 1)
    Submodule Γ(V, W) (K.cochain (p + 1)) :=
  letI := moduleW_altC K (p + 1)
  letI := moduleW_altC K p
  letI := Scheme.OrderedAffineCoverOf.moduleSections π
  { carrier := Set.range (K.d π p)
    add_mem' := fun ⟨w₁, h₁⟩ ⟨w₂, h₂⟩ => ⟨w₁ + w₂, by rw [map_add, h₁, h₂]⟩
    zero_mem' := ⟨0, map_zero _⟩
    smul_mem' := fun a _ ⟨w, hw⟩ =>
      ⟨a • w, (altd_smulW π K p a w).trans (congrArg (a • ·) hw)⟩ }

def

restrictBasic

L583 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.restrictBasic

Documentation

The affine cover obtained by intersecting the given cover with a basic open.

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_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π

Lean source · statement

def restrictBasic (hW : IsAffineOpen W) (f : Γ(V, W)) :
    Scheme.OrderedAffineCoverOf (V.basicOpen f)

theorem

altOpen_restrictBasic

L592 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altOpen_restrictBasic

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_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π

Lean source · statement

theorem altOpen_restrictBasic (hW : IsAffineOpen W) (f : Γ(V, W))
    {i : ℕ} (σ : Scheme.OrderedAffineCoverOf.Idx (restrictBasic π K hW f) i) :
    Scheme.OrderedAffineCoverOf.inter (restrictBasic π K hW f) σ
      = K.inter σ ⊓ V.basicOpen f

theorem

altOpen_restrictBasic_le

L599 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altOpen_restrictBasic_le

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_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π

Lean source · statement

theorem altOpen_restrictBasic_le (hW : IsAffineOpen W) (f : Γ(V, W))
    {i : ℕ} (σ : Scheme.OrderedAffineCoverOf.Idx (restrictBasic π K hW f) i) :
    Scheme.OrderedAffineCoverOf.inter (restrictBasic π K hW f) σ
      ≤ K.inter σ

def

resBasic

L606 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.resBasic

Documentation

The restriction of Čech cochains to the induced basic-open cover.

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_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π

Lean source · full declaration

def resBasic (hW : IsAffineOpen W) (f : Γ(V, W)) (q : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    K.cochain q
      →ₗ[R] Scheme.OrderedAffineCoverOf.cochain (restrictBasic π K hW f) q :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections π
  LinearMap.pi fun σ =>
    (Scheme.OrderedAffineCoverOf.res π (altOpen_restrictBasic_le π K hW f σ)).comp
      (LinearMap.proj (R := R) (φ := fun τ : K.Idx q => Γ(V, K.inter τ))
        (show K.Idx q from σ))

theorem

resBasic_apply

L616 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.resBasic_apply

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_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π

Lean source · full declaration

theorem resBasic_apply (hW : IsAffineOpen W) (f : Γ(V, W)) (q : ℕ)
    (x : K.cochain q)
    (σ : Scheme.OrderedAffineCoverOf.Idx (restrictBasic π K hW f) q) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    resBasic π K hW f q x σ
      = (V.presheaf.map (homOfLE
          (altOpen_restrictBasic_le π K hW f σ)).op).hom (x σ) := by
  rfl

theorem

altd_resBasic

L625 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altd_resBasic

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_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π

Lean source · full declaration

theorem altd_resBasic (hW : IsAffineOpen W) (f : Γ(V, W)) (q : ℕ)
    (x : K.cochain q) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    Scheme.OrderedAffineCoverOf.d π (restrictBasic π K hW f) q
        (resBasic π K hW f q x)
      = resBasic π K hW f (q + 1) (K.d π q x) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections π
  funext τ
  erw [Scheme.OrderedAffineCoverOf.d_apply, resBasic_apply, Scheme.OrderedAffineCoverOf.d_apply,
    map_sum]
  refine Finset.sum_congr rfl fun j _ => ?_
  erw [resBasic_apply, map_zsmul, res_res,
    res_res]
  rfl

theorem

away_surj

L640 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.away_surj

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_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π

Lean source · statement

theorem away_surj (hW : IsAffineOpen W) (f : Γ(V, W))
    {q : ℕ} (σ : Scheme.OrderedAffineCoverOf.Idx (restrictBasic π K hW f) q)
    (y : Γ(V, Scheme.OrderedAffineCoverOf.inter (restrictBasic π K hW f) σ)) :
    ∃ (n : ℕ) (a : Γ(V, K.inter σ)),
      (V.presheaf.map (homOfLE
          (altOpen_restrictBasic_le π K hW f σ)).op).hom a
        = (V.presheaf.map (homOfLE
            (((altOpen_restrictBasic π K hW f σ).le.trans inf_le_right).trans
              (V.basicOpen_le f))).op).hom f ^ n * y

theorem

away_ker

L665 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.away_ker

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_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π

Lean source · statement

theorem away_ker (hW : IsAffineOpen W) (f : Γ(V, W))
    {q : ℕ} (σ : Scheme.OrderedAffineCoverOf.Idx (restrictBasic π K hW f) q)
    (x : Γ(V, K.inter σ))
    (hx : (V.presheaf.map (homOfLE
        (altOpen_restrictBasic_le π K hW f σ)).op).hom x = 0) :
    ∃ m : ℕ,
      (V.presheaf.map (homOfLE (K.inter_le_base σ)).op).hom f ^ m * x = 0

theorem

exists_refinement

L688 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.exists_refinement

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
omit π in

Lean source · statement

theorem exists_refinement (hW : IsAffineOpen W) :
    ∃ (s : Set Γ(V, W)) (ι : s → K.ι),
      Ideal.span s = ⊤ ∧ ∀ r : s, V.basicOpen (r : Γ(V, W)) ≤ K.U (ι r)

theorem

smul_pow_mem_range

L705 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.smul_pow_mem_range

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_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π

Lean source · full declaration

theorem smul_pow_mem_range (hW : IsAffineOpen W)
    (f : Γ(V, W)) (i₀ : K.ι) (hfi : V.basicOpen f ≤ K.U i₀)
    (p : ℕ) (z : K.cochain (p + 1))
    (hz : letI := Scheme.OrderedAffineCoverOf.moduleSections π
          K.d π (p + 1) z = 0) :
    letI := moduleW_altC K (p + 1)
    ∃ N : ℕ, f ^ N • z ∈ rangeW π K p := by
  let := Scheme.OrderedAffineCoverOf.moduleSections π
  let := moduleW_altC K (p + 1)
  let := moduleW_altC K p
  set Kf := restrictBasic π K hW f with hKf
  have hi₀f : Kf.U i₀ = V.basicOpen f := inf_eq_right.mpr hfi
  have hzf : Scheme.OrderedAffineCoverOf.d π Kf (p + 1) (resBasic π K hW f (p + 1) z)
      = 0 := by
    rw [altd_resBasic, hz, map_zero]
  obtain ⟨w, hw⟩ := wholeSpace_exact π Kf i₀ hi₀f p
    (LinearMap.mem_ker.mpr hzf)
  choose nσ aσ haσ using fun σ => away_surj π K hW f σ (w σ)
  set N₁ : ℕ := Finset.univ.sup nσ with hN₁
  have hN₁le : ∀ σ, nσ σ ≤ N₁ := fun σ => Finset.le_sup (Finset.mem_univ σ)
  set a : K.cochain p := fun σ =>
    (V.presheaf.map (homOfLE (K.inter_le_base σ)).op).hom f ^ (N₁ - nσ σ) * aσ σ
    with ha_def
  have hresA : ∀ σ, resBasic π K hW f p a σ
      = (V.presheaf.map (homOfLE (((altOpen_restrictBasic π K hW f σ).le.trans
          inf_le_right).trans (V.basicOpen_le f))).op).hom f ^ N₁ * w σ := by
    intro σ
    rw [resBasic_apply, ha_def, map_mul, map_pow, res_res,
      haσ σ, ← mul_assoc, ← pow_add, Nat.sub_add_cancel (hN₁le σ)]
  have hstep : resBasic π K hW f (p + 1) (K.d π p a)
      = resBasic π K hW f (p + 1) (f ^ N₁ • z) := by
    rw [← altd_resBasic]
    funext τ
    erw [Scheme.OrderedAffineCoverOf.d_apply]
    conv_rhs =>
      erw [resBasic_apply, smulW_apply, map_pow, map_mul, map_pow, res_res]
    have hwτ := congrFun hw τ
    erw [Scheme.OrderedAffineCoverOf.d_apply, resBasic_apply] at hwτ
    rw [← hwτ, Finset.mul_sum]
    refine Finset.sum_congr rfl fun j _ => ?_
    erw [hresA, map_mul, map_pow, res_res, mul_smul_comm]
  have hker : ∀ τ : K.Idx (p + 1), ∃ m : ℕ,
      (V.presheaf.map (homOfLE (K.inter_le_base τ)).op).hom f ^ m
        * (K.d π p a τ - (f ^ N₁ • z) τ) = 0 := by
    intro τ
    refine away_ker π K hW f τ _ ?_
    have := congrFun hstep τ
    erw [resBasic_apply, resBasic_apply] at this
    rw [map_sub, this, sub_self]
  choose mτ hmτ using hker
  set N₂ : ℕ := Finset.univ.sup mτ
  refine ⟨N₁ + N₂, f ^ N₂ • a, ?_⟩
  rw [altd_smulW]
  funext τ
  rw [smulW_apply, smulW_apply, map_pow, map_pow]
  have hN₂le : mτ τ ≤ N₂ := Finset.le_sup (f := mτ) (Finset.mem_univ τ)
  have key := hmτ τ
  rw [smulW_apply, map_pow] at key
  have key2 : (V.presheaf.map (homOfLE (K.inter_le_base τ)).op).hom f ^ N₂
      * (K.d π p a τ
        - (V.presheaf.map (homOfLE (K.inter_le_base τ)).op).hom f ^ N₁ * z τ)
      = 0 := by
    conv_lhs => rw [← Nat.sub_add_cancel hN₂le, pow_add, mul_assoc, key]
    exact mul_zero _
  rw [mul_sub, ← mul_assoc, ← pow_add, sub_eq_zero, add_comm N₂ N₁] at key2
  exact key2

theorem

affine_acyclic

L772 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen.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_succ_le_range_d_of_isAffineOpen
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 AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π

Lean source · full declaration

theorem affine_acyclic (hW : IsAffineOpen W) (p : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    LinearMap.ker (K.d π (p + 1))
      ≤ LinearMap.range (K.d π p) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections π
  let := moduleW_altC K (p + 1)
  intro z hz
  obtain ⟨s, ιs, hspan, hle⟩ := exists_refinement K hW
  have : z ∈ rangeW π K p :=
    Submodule.mem_of_span_eq_top_of_smul_pow_mem _ s hspan z fun r =>
      smul_pow_mem_range π K hW r (ιs r) (hle r) p z hz
  exact this

theorem

ker_d_succ_le_range_d_of_isAffineOpen

L797 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.ker_d_succ_le_range_d_of_isAffineOpen

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_succ_le_range_d_of_isAffineOpen
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_succ_le_range_d_of_isAffineOpen.AlgebraicGeometry in
with_weak_namespace Scheme_OrderedAffineCoverOf_ker_d_succ_le_range_d_of_isAffineOpen

Lean source · full declaration

theorem
    _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.ker_d_succ_le_range_d_of_isAffineOpen
    {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] {W : V.Opens}
    (K : V.OrderedAffineCoverOf W) (hW : IsAffineOpen W) (p : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    LinearMap.ker (K.d π (p + 1)) ≤ LinearMap.range (K.d π p) :=
  Scheme.OrderedAffineCoverOf.Acyclic.affine_acyclic π K hW p

Module documentation

Positive-degree exactness of affine-cover Cech cochains

Declarations