NYLL
Module

OModulePresheaf_ores_ounitPullback_oext.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_ores_ounitPullback_oext
7 declarations indexed from sourceView source ↗

Module documentation

Ordered Čech restriction, extension, and pullback identities.

Imports7
Imported by2

Declarations

theorem

ores_od

L36 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ores_ounitPullback_oext.DORDProofs.ores_od
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ores_ounitPullback_oext
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace DORDProofs
open AlgebraicGeometry.OModulePresheaf AlgebraicGeometry.Scheme.OrderedAffineCover
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem ores_od (F : OModulePresheaf π) (K : V.OrderedAffineCover) (n : ℕ) (c : F.ocochain K n) :
    F.ores K (n + 1) (F.od K n c) = F.d K n (F.ores K n c)
theorem

ores_oext

L42 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ores_ounitPullback_oext.DORDProofs.ores_oext
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ores_ounitPullback_oext
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace DORDProofs
open AlgebraicGeometry.OModulePresheaf AlgebraicGeometry.Scheme.OrderedAffineCover
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem ores_oext (F : OModulePresheaf π) (K : V.OrderedAffineCover) (n : ℕ) (z : F.cochain K n) :
    F.ores K n (F.oext K n z) = z
theorem

ores_ocup

L55 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ores_ounitPullback_oext.DORDProofs.ores_ocup
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ores_ounitPullback_oext
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace DORDProofs
open AlgebraicGeometry.OModulePresheaf AlgebraicGeometry.Scheme.OrderedAffineCover
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem ores_ocup (F : OModulePresheaf π) (K : V.OrderedAffineCover) (a b n : ℕ) (hn : a + b = n)
    (α : (OModulePresheaf.unit π).ocochain K a) (β : F.ocochain K b) :
    F.ores K n (F.ocup K a b n hn α β) =
      F.cup K a b n hn ((OModulePresheaf.unit π).ores K a α) (F.ores K b β)
theorem

ores_ounitPullback_oext

L64 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ores_ounitPullback_oext.DORDProofs.ores_ounitPullback_oext
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ores_ounitPullback_oext
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace DORDProofs
open AlgebraicGeometry.OModulePresheaf AlgebraicGeometry.Scheme.OrderedAffineCover
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)}
variable {R' : Type u} [CommRing R'] {X Y : Scheme.{u}}
Lean source · statement
theorem ores_ounitPullback_oext
    (πX : X ⟶ Spec (CommRingCat.of R')) (πY : Y ⟶ Spec (CommRingCat.of R))
    (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover) (𝒦 : Y.OrderedAffineCover) (lam : 𝒲.ι → 𝒦.ι)
    (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w)) (n : ℕ) (z : (OModulePresheaf.unit πY).cochain 𝒦 n) :
    (OModulePresheaf.unit πX).ores 𝒲 n
        (OModulePresheaf.ounitPullback (πX := πX) h 𝒲 𝒦 lam hlam n
          ((OModulePresheaf.unit πY).oext 𝒦 n z)) =
      OModulePresheaf.unitPullback (πX := πX) h 𝒲 𝒦 lam hlam n z
theorem

od_ounitPullback

L101 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ores_ounitPullback_oext.DORDProofs.od_ounitPullback
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ores_ounitPullback_oext
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace DORDProofs
open AlgebraicGeometry.OModulePresheaf AlgebraicGeometry.Scheme.OrderedAffineCover
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)}
variable {R' : Type u} [CommRing R'] {X Y : Scheme.{u}}
Lean source · statement
theorem od_ounitPullback
    (πX : X ⟶ Spec (CommRingCat.of R')) (πY : Y ⟶ Spec (CommRingCat.of R))
    (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover) (𝒦 : Y.OrderedAffineCover) (lam : 𝒲.ι → 𝒦.ι)
    (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w)) (n : ℕ) (c : (OModulePresheaf.unit πY).ocochain 𝒦 n) :
    (OModulePresheaf.unit πX).od 𝒲 n (OModulePresheaf.ounitPullback (πX := πX) h 𝒲 𝒦 lam hlam n c) =
      OModulePresheaf.ounitPullback (πX := πX) h 𝒲 𝒦 lam hlam (n + 1)
        ((OModulePresheaf.unit πY).od 𝒦 n c)
theorem

ounitPullback_ocup

L125 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ores_ounitPullback_oext.DORDProofs.ounitPullback_ocup
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ores_ounitPullback_oext
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace DORDProofs
open AlgebraicGeometry.OModulePresheaf AlgebraicGeometry.Scheme.OrderedAffineCover
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)}
variable {R' : Type u} [CommRing R'] {X Y : Scheme.{u}}
Lean source · statement
theorem ounitPullback_ocup
    (πX : X ⟶ Spec (CommRingCat.of R')) (πY : Y ⟶ Spec (CommRingCat.of R))
    (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover) (𝒦 : Y.OrderedAffineCover) (lam : 𝒲.ι → 𝒦.ι)
    (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w)) (a b n : ℕ) (hn : a + b = n)
    (α : (OModulePresheaf.unit πY).ocochain 𝒦 a) (β : (OModulePresheaf.unit πY).ocochain 𝒦 b) :
    OModulePresheaf.ounitPullback (πX := πX) h 𝒲 𝒦 lam hlam n
        ((OModulePresheaf.unit πY).ocup 𝒦 a b n hn α β) =
      (OModulePresheaf.unit πX).ocup 𝒲 a b n hn
        (OModulePresheaf.ounitPullback (πX := πX) h 𝒲 𝒦 lam hlam a α)
        (OModulePresheaf.ounitPullback (πX := πX) h 𝒲 𝒦 lam hlam b β)
theorem

ores_ounitPullback_oext

L161 ↗
AlgebraicGeometry.OModulePresheaf.ores_ounitPullback_oext
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ores_ounitPullback_oext
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.ores_ounitPullback_oext
    {R R' : Type u} [CommRing R] [CommRing R'] {X Y : Scheme.{u}}
    (πX : X ⟶ Spec (CommRingCat.of R')) (πY : Y ⟶ Spec (CommRingCat.of R))
    (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover) (𝒦 : Y.OrderedAffineCover) (lam : 𝒲.ι → 𝒦.ι)
    (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w)) (n : ℕ) (z : (OModulePresheaf.unit πY).cochain 𝒦 n) :
    (OModulePresheaf.unit πX).ores 𝒲 n
        (OModulePresheaf.ounitPullback (πX := πX) h 𝒲 𝒦 lam hlam n
          ((OModulePresheaf.unit πY).oext 𝒦 n z)) =
      OModulePresheaf.unitPullback (πX := πX) h 𝒲 𝒦 lam hlam n z

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