NYLL
Module

OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen
6 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf exists box zigzag of d eq zero of is Affine Open

Imports44
Imported by2

Declarations

abbrev

rr

L76 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen.G1SlabZigzagAux.rr
Documentation

Restriction of regular sections to a smaller open.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
universe u
namespace G1SlabZigzagAux
variable {P : Scheme.{u}}
Lean source · statement
abbrev rr {O O' : P.Opens} (h : O ≤ O') : Γ(P, O') →+* Γ(P, O)
theorem

rr_rr

L79 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen.G1SlabZigzagAux.rr_rr
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
universe u
namespace G1SlabZigzagAux
variable {P : Scheme.{u}}
Lean source · statement
theorem rr_rr {O O' O'' : P.Opens} (h : O ≤ O') (h' : O' ≤ O'') (x : Γ(P, O'')) :
    rr h (rr h' x) = rr (h.trans h') x
theorem

isSeparated_fst

L94 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen.G1SlabZigzagAux.isSeparated_fst
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
universe u
namespace G1SlabZigzagAux
variable {P : Scheme.{u}}
section Main
variable {k : Type u} [Field k] {X Y : Scheme.{u}}
  (fX : X ⟶ Spec (CommRingCat.of k)) (fY : Y ⟶ Spec (CommRingCat.of k))
  [IsSeparated fX] [IsSeparated fY]
  (p₁ : P ⟶ X) (p₂ : P ⟶ Y)
  (𝒲 : P.OrderedAffineCover) (𝒱 : Y.OrderedAffineCover) (U : X.Opens)
omit [IsSeparated fX] in
Lean source · statement
theorem isSeparated_fst (hP : IsPullback p₁ p₂ fX fY) : IsSeparated p₁
theorem

isAffineOpen_strip

L98 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen.G1SlabZigzagAux.isAffineOpen_strip
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
universe u
namespace G1SlabZigzagAux
variable {P : Scheme.{u}}
section Main
variable {k : Type u} [Field k] {X Y : Scheme.{u}}
  (fX : X ⟶ Spec (CommRingCat.of k)) (fY : Y ⟶ Spec (CommRingCat.of k))
  [IsSeparated fX] [IsSeparated fY]
  (p₁ : P ⟶ X) (p₂ : P ⟶ Y)
  (𝒲 : P.OrderedAffineCover) (𝒱 : Y.OrderedAffineCover) (U : X.Opens)
omit [IsSeparated fX] in
Lean source · statement
theorem isAffineOpen_strip (hP : IsPullback p₁ p₂ fX fY) (hU : IsAffineOpen U) {a : ℕ} (σ : 𝒱.Idx
  a) :
    IsAffineOpen (p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ 𝒱.inter σ)
theorem

restrict_inter

L109 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen.G1SlabZigzagAux.restrict_inter
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
universe u
namespace G1SlabZigzagAux
variable {P : Scheme.{u}}
section Main
variable {k : Type u} [Field k] {X Y : Scheme.{u}}
  (fX : X ⟶ Spec (CommRingCat.of k)) (fY : Y ⟶ Spec (CommRingCat.of k))
  [IsSeparated fX] [IsSeparated fY]
  (p₁ : P ⟶ X) (p₂ : P ⟶ Y)
  (𝒲 : P.OrderedAffineCover) (𝒱 : Y.OrderedAffineCover) (U : X.Opens)
Lean source · statement
theorem restrict_inter {R : Type u} [CommRing R] (π : P ⟶ Spec (.of R)) [IsSeparated π]
    {W : P.Opens} (hW : IsAffineOpen W) {b : ℕ} (t : (𝒲.restrict π hW).Idx b) :
    (𝒲.restrict π hW).inter t = 𝒲.inter t ⊓ W
theorem

exists_box_zigzag_of_d_eq_zero_of_isAffineOpen

L131 ↗
AlgebraicGeometry.OModulePresheaf.exists_box_zigzag_of_d_eq_zero_of_isAffineOpen
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory CategoryTheory.Limits TopologicalSpace
universe u
open AlgebraicCurves.Cohomology.Sheaves.Proofs in
open OModulePresheaf_exists_box_zigzag_of_d_eq_zero_of_isAffineOpen.G1SlabZigzagAux in
Lean source · statement
theorem exists_box_zigzag_of_d_eq_zero_of_isAffineOpen
    {k : Type u} [Field k] {X Y P : Scheme.{u}}
    (fX : X ⟶ Spec (CommRingCat.of k)) (fY : Y ⟶ Spec (CommRingCat.of k))
    [QuasiCompact fX] [IsSeparated fX] [QuasiCompact fY] [IsSeparated fY]
    (p₁ : P ⟶ X) (p₂ : P ⟶ Y) (hP : IsPullback p₁ p₂ fX fY)
    (𝒲 : P.OrderedAffineCover) (𝒱 : Y.OrderedAffineCover)
    (c : (OModulePresheaf.unit (p₁ ≫ fX)).cochain 𝒲 1)
    (hc : (OModulePresheaf.unit (p₁ ≫ fX)).d 𝒲 1 c = 0)
    (U : X.Opens) (hU : IsAffineOpen U) :
    ∃ (γ : ∀ (σ : 𝒱.Idx 0) (t : 𝒲.Idx 0), Γ(P, 𝒲.inter t ⊓ p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ 𝒱.inter σ))
      (e : ∀ σ : 𝒱.Idx 1, Γ(P, p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ 𝒱.inter σ)),
      (∀ (σ : 𝒱.Idx 0) (t : 𝒲.Idx (0 + 1)),
        (P.presheaf.map (homOfLE (inf_le_left.trans inf_le_left :
            𝒲.inter t ⊓ p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ 𝒱.inter σ ≤ 𝒲.inter t)).op).hom (c t)
          = ∑ j : Fin (0 + 2), ((-1 : ℤ) ^ (j : ℕ)) •
              (P.presheaf.map (homOfLE (inf_le_inf_right (p₂ ⁻¹ᵁ 𝒱.inter σ)
                (inf_le_inf_right (p₁ ⁻¹ᵁ U) (𝒲.inter_le_inter_face t j)))).op).hom (γ σ (𝒲.face t
                  j))) ∧
      (∀ (σ : 𝒱.Idx (0 + 1)) (t : 𝒲.Idx 0),
        (P.presheaf.map (homOfLE (inf_le_inf_right (p₂ ⁻¹ᵁ 𝒱.inter σ) inf_le_right :
            𝒲.inter t ⊓ p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ 𝒱.inter σ ≤ p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ 𝒱.inter σ)).op).hom (e σ)
          = ∑ j : Fin (0 + 2), ((-1 : ℤ) ^ (j : ℕ)) •
              (P.presheaf.map (homOfLE (inf_le_inf_left (𝒲.inter t ⊓ p₁ ⁻¹ᵁ U)
                (p₂.preimage_mono (𝒱.inter_le_inter_face σ j)))).op).hom (γ (𝒱.face σ j) t)) ∧
      (∀ ρ : 𝒱.Idx (1 + 1),
        ∑ j : Fin (1 + 2), ((-1 : ℤ) ^ (j : ℕ)) •
            (P.presheaf.map (homOfLE (inf_le_inf_left (p₁ ⁻¹ᵁ U)
              (p₂.preimage_mono (𝒱.inter_le_inter_face ρ j)))).op).hom (e (𝒱.face ρ j)) = 0)

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