AlgebraicGeometry.OModulePresheaf.Leray.exists_levelwise_equiv_transpose_id
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_exists_levelwise_equiv_transpose_id
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
open AlgebraicGeometry.OModulePresheaf AlgebraicGeometry.OModulePresheaf.LerayLean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.Leray.exists_levelwise_equiv_transpose_id
{R : Type u} [CommRing R] {X : Scheme.{u}} (π : X ⟶ Spec (CommRingCat.of R))
(𝔓 𝒲 : X.OrderedAffineCover) :
∃ e : ∀ p q : ℕ, (OModulePresheaf.Leray.LerayDblCpx (𝟙 X) π 𝒲 𝔓).C p q ≃ₗ[R]
(DoubleComplex.transpose (OModulePresheaf.Leray.LerayDblCpx (𝟙 X) π 𝔓 𝒲)).C p q,
(∀ (p q : ℕ) (x : (OModulePresheaf.Leray.LerayDblCpx (𝟙 X) π 𝒲 𝔓).C p q),
e (p + 1) q ((OModulePresheaf.Leray.LerayDblCpx (𝟙 X) π 𝒲 𝔓).dH p q x) =
(DoubleComplex.transpose (OModulePresheaf.Leray.LerayDblCpx (𝟙 X) π 𝔓 𝒲)).dH p q
(e p q x)) ∧
(∀ (p q : ℕ) (x : (OModulePresheaf.Leray.LerayDblCpx (𝟙 X) π 𝒲 𝔓).C p q),
e p (q + 1) ((OModulePresheaf.Leray.LerayDblCpx (𝟙 X) π 𝒲 𝔓).dV p q x) =
(DoubleComplex.transpose (OModulePresheaf.Leray.LerayDblCpx (𝟙 X) π 𝔓 𝒲)).dV p q
(e p q x)) ∧
∀ (p q : ℕ) (x : (OModulePresheaf.Leray.LerayDblCpx (𝟙 X) π 𝒲 𝔓).C p q)
(σ : 𝔓.Idx q) (τ : 𝒲.Idx p),
(e p q x : OModulePresheaf.Leray.biC (𝟙 X) π 𝔓 𝒲 q p) (σ, τ) =
(X.presheaf.map (homOfLE (le_inf
(inf_le_right.trans (Scheme.Hom.id_preimage (𝔓.inter σ)).le)
((Scheme.Hom.id_preimage (𝒲.inter τ)).ge.trans' inf_le_left) :
OModulePresheaf.Leray.biOpen (𝟙 X) 𝔓 𝒲 q p σ τ ≤
OModulePresheaf.Leray.biOpen (𝟙 X) 𝒲 𝔓 p q τ σ)).op).hom
(x (τ, σ))