AlgebraicGeometry.OModulePresheaf.exists_linearMap_apply_eq_unitPullback
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_exists_linearMap_apply_eq_unitPullback
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe uLean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.exists_linearMap_apply_eq_unitPullback
{R : Type u} [CommRing R] {X Y : Scheme.{u}}
(πX : X ⟶ Spec (CommRingCat.of R)) (πY : Y ⟶ Spec (CommRingCat.of R))
(h : X ⟶ Y) (hh : h ≫ πY = πX)
(𝒲 : X.OrderedAffineCover) (𝒦 : Y.OrderedAffineCover) (lam : 𝒲.ι → 𝒦.ι)
(hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w)) (n : ℕ) :
∃ L : (OModulePresheaf.unit πY).cochain 𝒦 n →ₗ[R] (OModulePresheaf.unit πX).cochain 𝒲 n,
∀ z, L z = OModulePresheaf.unitPullback (πX := πX) h 𝒲 𝒦 lam hlam n z