Module

OModulePresheaf_Leray_rows_exact.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_rows_exact

10 declarations indexed from sourceView source ↗

Module documentation

Exactness of the Leray bicomplex rows for a quasicoherent module presheaf.

Imports5

Imported by4

theorem

res_self'

L50 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact.AlgebraicGeometry.OModulePresheaf.Leray.res_self'

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}}

Lean source · statement

theorem res_self' {O : V.Opens} (h : O ≤ O) (x : Γ(V, O)) : (V.presheaf.map (homOfLE h).op).hom x
    = x

theorem

unit_d_apply'

L54 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact.AlgebraicGeometry.OModulePresheaf.Leray.unit_d_apply'

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}}

Lean source · statement

theorem unit_d_apply' (π : V ⟶ Spec (.of R)) (K : V.OrderedAffineCover) (i : ℕ)
    (f : (OModulePresheaf.unit π).cochain K i) (s : K.Idx (i + 1)) :
    ((OModulePresheaf.unit π).d K i f s : Γ(V, K.inter s))
      = ∑ j : Fin (i + 2), ((-1 : ℤ) ^ (j : ℕ)) •
          (V.presheaf.map (homOfLE (K.inter_le_inter_face s j)).op).hom (f (K.face s j))

theorem

pullOpen_d_apply'

L68 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact.AlgebraicGeometry.OModulePresheaf.Leray.pullOpen_d_apply'

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')

Lean source · statement

theorem pullOpen_d_apply' (W : V'.Opens) (a : ℕ) (f : (pullOpen p πZ W).cochain K a) (σ : K.Idx (a
    + 1)) :
    ((pullOpen p πZ W).d K a f σ : Γ(V', W ⊓ (Opens.map p.base).obj (K.inter σ)))
      = ∑ j : Fin (a + 2), ((-1 : ℤ) ^ (j : ℕ)) •
          (V'.presheaf.map (homOfLE (inf_le_inf_left W
            ((Opens.map p.base).monotone (K.inter_le_inter_face σ j)))).op).hom (f (K.face σ j))

def

rowC_equiv

L84 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact.AlgebraicGeometry.OModulePresheaf.Leray.rowC_equiv

Documentation

Identify a row of the Leray bicomplex with the cochains of its induced affine cover.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
section Rows
variable [IsSeparated πZ] [IsSeparated (p ≫ πZ)]

Lean source · full declaration

def rowC_equiv {b : ℕ} (τ : K'.Idx b) (a : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    (pullOpen p πZ (K'.inter τ)).cochain K a ≃ₗ[R] (rowCoverOf p πZ K K' τ).cochain a :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  { toFun := fun f σ => (V'.presheaf.map (homOfLE (inter_rowCoverOf p πZ K K' τ σ).le).op).hom (f σ)
    invFun := fun g σ => (V'.presheaf.map (homOfLE (inter_rowCoverOf p πZ K K' τ σ).ge).op).hom (g
      σ)
    left_inv := fun f => funext fun σ => by
      change (V'.presheaf.map _).hom ((V'.presheaf.map _).hom (f σ)) = f σ
      erw [Scheme.TwoAffineOpenCover.res_res]; exact res_self' _ _
    right_inv := fun g => funext fun σ => by
      change (V'.presheaf.map _).hom ((V'.presheaf.map _).hom (g σ)) = g σ
      erw [Scheme.TwoAffineOpenCover.res_res]; exact res_self' _ _
    map_add' := fun _ _ => funext fun σ => map_add _ _ _
    map_smul' := fun r f => funext fun σ =>
      (Scheme.OrderedAffineCoverOf.res (p ≫ πZ) (inter_rowCoverOf p πZ K K' τ σ).le).map_smul r (f
        σ) }

theorem

rowC_equiv_apply

L102 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact.AlgebraicGeometry.OModulePresheaf.Leray.rowC_equiv_apply

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
section Rows
variable [IsSeparated πZ] [IsSeparated (p ≫ πZ)]

Lean source · full declaration

theorem rowC_equiv_apply {b : ℕ} (τ : K'.Idx b) (a : ℕ) (f) (σ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    rowC_equiv p πZ K K' τ a f σ = (V'.presheaf.map (homOfLE (inter_rowCoverOf p πZ K K' τ
      σ).le).op).hom (f σ) :=
  rfl

theorem

rowC_comm

L108 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact.AlgebraicGeometry.OModulePresheaf.Leray.rowC_comm

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
section Rows
variable [IsSeparated πZ] [IsSeparated (p ≫ πZ)]

Lean source · full declaration

theorem rowC_comm {b : ℕ} (τ : K'.Idx b) (a : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    ∀ f, rowC_equiv p πZ K K' τ (a + 1) ((pullOpen p πZ (K'.inter τ)).d K a f)
      = (rowCoverOf p πZ K K' τ).d (p ≫ πZ) a (rowC_equiv p πZ K K' τ a f) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  intro f; funext σ
  erw [rowC_equiv_apply, pullOpen_d_apply', Scheme.OrderedAffineCoverOf.d_apply]
  refine (map_sum ((V'.presheaf.map _).hom) _ _).trans (Finset.sum_congr rfl fun j _ => ?_)
  change (V'.presheaf.map _).hom (((-1 : ℤ) ^ (j : ℕ)) • (V'.presheaf.map _).hom (f (K.face σ j)))
    = ((-1 : ℤ) ^ (j : ℕ)) • (V'.presheaf.map _).hom ((V'.presheaf.map _).hom (f (K.face σ j)))
  erw [map_zsmul, Scheme.TwoAffineOpenCover.res_res]
  exact (congrArg (((-1 : ℤ) ^ (j : ℕ)) • ·) (Scheme.TwoAffineOpenCover.res_res _ _ _)).symm

theorem

ker_dH_succ_le_range_dH

L121 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact.AlgebraicGeometry.OModulePresheaf.Leray.ker_dH_succ_le_range_dH

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
section Rows
variable [IsSeparated πZ] [IsSeparated (p ≫ πZ)]

Lean source · statement

theorem ker_dH_succ_le_range_dH (a b : ℕ) :
    LinearMap.ker ((LerayDblCpx p πZ K K').dH (a + 1) b) ≤ LinearMap.range ((LerayDblCpx p πZ K
      K').dH a b)

theorem

ker_dH_zero_eq_range_biAug

L146 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact.AlgebraicGeometry.OModulePresheaf.Leray.ker_dH_zero_eq_range_biAug

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
section Rows
variable [IsSeparated πZ] [IsSeparated (p ≫ πZ)]

Lean source · statement

theorem ker_dH_zero_eq_range_biAug (b : ℕ) :
    LinearMap.ker ((LerayDblCpx p πZ K K').dH 0 b) = LinearMap.range (biAug p πZ K K' b)

theorem

biAug_injective

L179 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact.AlgebraicGeometry.OModulePresheaf.Leray.biAug_injective

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
section Rows
variable [IsSeparated πZ] [IsSeparated (p ≫ πZ)]

Lean source · statement

theorem biAug_injective (b : ℕ) : Function.Injective (biAug p πZ K K' b)

theorem

rows_exact

L199 ↗

AlgebraicGeometry.OModulePresheaf.Leray.rows_exact

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_rows_exact
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.AlgebraicCurves.Cohomology.Sheaves.Proofs in
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
  OModulePresheaf_Leray_rows_exact.AlgebraicGeometry.OModulePresheaf.Leray in

Lean source · statement

theorem _root_.AlgebraicGeometry.OModulePresheaf.Leray.rows_exact
    {R : Type u} [CommRing R] {V' Z : Scheme.{u}} (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R))
    [IsSeparated πZ] [IsSeparated (p ≫ πZ)] (K : Z.OrderedAffineCover) (K' :
      V'.OrderedAffineCover) :
    (∀ a b : ℕ, LinearMap.ker ((OModulePresheaf.Leray.LerayDblCpx p πZ K K').dH (a + 1) b)
        ≤ LinearMap.range ((OModulePresheaf.Leray.LerayDblCpx p πZ K K').dH a b)) ∧
      (∀ b : ℕ, LinearMap.ker ((OModulePresheaf.Leray.LerayDblCpx p πZ K K').dH 0 b)
        = LinearMap.range (OModulePresheaf.Leray.biAug p πZ K K' b)) ∧
      ∀ b : ℕ, Function.Injective (OModulePresheaf.Leray.biAug p πZ K K' b)

Module documentation

Declarations