AlgebraicGeometry.OModulePresheaf.cechFinite_of_affSES_right
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_affSES_right
universe u
open AlgebraicGeometry _root_.AlgebraicGeometry.OModulePresheaf inLean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cechFinite_of_affSES_right {R : Type u} [CommRing
R] [IsNoetherianRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
[IsSeparated π] {F₁ F₂ F₃ : OModulePresheaf π} (S : OModulePresheaf.AffSES F₁ F₂ F₃) (K :
V.OrderedAffineCover)
(h₁ : F₁.CechFinite K) (h₂ : F₂.CechFinite K) : F₃.CechFinite K