Module

OModulePresheaf_unitPullback_unitPullback_sub_mem_of_d_eq_zero.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_unitPullback_unitPullback_sub_mem_of_d_eq_zero

2 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf unit Pullback unit Pullback sub mem of d eq zero

Imports7

Mathlib.Data.Fin.Tuple.Sort
Mathlib.GroupTheory.Perm.Sign
Mathlib.AlgebraicGeometry.Scheme
Nyll.SchemeTheory.Cohomology.Cech.OrderedAffineCoverCech
Nyll.AlgebraicCurves.Cohomology.Cech.OrderedAffineCoverCechCup
Nyll.AlgebraicCurves.Cohomology.Sheaves.OrderedAffineCoverCochainPullback
Nyll.AlgebraicCurves.Cohomology.Cech.OrderedAffineCoverCechOrdered

Imported by3

theorem

comp_eq

L41 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_unitPullback_unitPullback_sub_mem_of_d_eq_zero.FHSOL.comp_eq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_unitPullback_unitPullback_sub_mem_of_d_eq_zero
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace FHSOL
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.Scheme

Lean source · statement

theorem comp_eq
    {R R' R'' : Type u} [CommRing R] [CommRing R'] [CommRing R''] {X Y Z : Scheme.{u}}
    (πX : X ⟶ Spec (CommRingCat.of R'')) (πY : Y ⟶ Spec (CommRingCat.of R')) (πZ : Z ⟶ Spec
      (CommRingCat.of R))
    (g : X ⟶ Y) (h : Y ⟶ Z)
    (𝒲 : X.OrderedAffineCover) (𝒱 : Y.OrderedAffineCover) (𝒦 : Z.OrderedAffineCover)
    (mu : 𝒲.ι → 𝒱.ι) (lam : 𝒱.ι → 𝒦.ι)
    (hmu : ∀ w, 𝒲.U w ≤ g ⁻¹ᵁ 𝒱.U (mu w)) (hlam : ∀ v, 𝒱.U v ≤ h ⁻¹ᵁ 𝒦.U (lam v))
    (hcomp : ∀ w, 𝒲.U w ≤ (g ≫ h) ⁻¹ᵁ 𝒦.U ((lam ∘ mu) w))
    (n : ℕ) (z : (OModulePresheaf.unit πZ).cochain 𝒦 n) :
    OModulePresheaf.unitPullback (πX := πX) g 𝒲 𝒱 mu hmu n
        (OModulePresheaf.unitPullback (πX := πY) h 𝒱 𝒦 lam hlam n z) =
      OModulePresheaf.unitPullback (πX := πX) (g ≫ h) 𝒲 𝒦 (lam ∘ mu) hcomp n z

theorem

unitPullback_unitPullback_sub_mem_of_d_eq_zero

L117 ↗

AlgebraicGeometry.OModulePresheaf.unitPullback_unitPullback_sub_mem_of_d_eq_zero

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_unitPullback_unitPullback_sub_mem_of_d_eq_zero
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u

Lean source · full declaration

theorem _root_.AlgebraicGeometry.OModulePresheaf.unitPullback_unitPullback_sub_mem_of_d_eq_zero
    {R R' R'' : Type u} [CommRing R] [CommRing R'] [CommRing R''] {X Y Z : Scheme.{u}}
    (πX : X ⟶ Spec (CommRingCat.of R'')) (πY : Y ⟶ Spec (CommRingCat.of R')) (πZ : Z ⟶ Spec
      (CommRingCat.of R))
    (h : X ⟶ Y) (h' : Y ⟶ Z) (h'' : X ⟶ Z) (hh : h'' = h ≫ h')
    (𝒲 : X.OrderedAffineCover) (𝒦 : Y.OrderedAffineCover) (𝒦' : Z.OrderedAffineCover)
    (lam : 𝒲.ι → 𝒦.ι) (lam' : 𝒦.ι → 𝒦'.ι) (lam'' : 𝒲.ι → 𝒦'.ι) (hlc : lam'' = lam' ∘ lam)
    (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w)) (hlam' : ∀ i, 𝒦.U i ≤ h' ⁻¹ᵁ 𝒦'.U (lam' i))
    (hlam'' : ∀ w, 𝒲.U w ≤ h'' ⁻¹ᵁ 𝒦'.U (lam'' w))
    (n : ℕ) (z : (OModulePresheaf.unit πZ).cochain 𝒦' n) (hz : (OModulePresheaf.unit πZ).d 𝒦' n z =
      0) :
    OModulePresheaf.unitPullback (πX := πX) h 𝒲 𝒦 lam hlam n (OModulePresheaf.unitPullback (πX :=
      πY) h' 𝒦 𝒦' lam' hlam' n z) -
        OModulePresheaf.unitPullback (πX := πX) h'' 𝒲 𝒦' lam'' hlam'' n z
      ∈ (show Submodule R'' ((OModulePresheaf.unit πX).cochain 𝒲 n) from
          match n with
          | 0 => ⊥
          | m + 1 => LinearMap.range ((OModulePresheaf.unit πX).d 𝒲 m)) := by
  subst hh hlc
  rw [FHSOL.comp_eq πX πY πZ h h' 𝒲 𝒦 𝒦' lam lam' hlam hlam' hlam'' n z, sub_self]
  exact Submodule.zero_mem _

Module documentation

OModule Presheaf unit Pullback unit Pullback sub mem of d eq zero

Declarations

comp_eq

unitPullback_unitPullback_sub_mem_of_d_eq_zero