AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eq_zero_of_forall_res_basicOpen_eq_zero.AlgebraicGeometry.OModulePresheaf.G4T.eq_zero_of_forall_res_basicOpen_eq_zero
Source context 19 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_eq_zero_of_forall_res_basicOpen_eq_zero
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G4T
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section PModQC
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable {F G : OModulePresheaf π} (φ : OModulePresheaf.Hom F G)Lean source · statement
theorem eq_zero_of_forall_res_basicOpen_eq_zero {F : OModulePresheaf π} (hF :
OModulePresheaf.IsQuasicoherent F)
(U : V.affineOpens) {ι : Type*} [Finite ι] (h : ι → Γ(V, U.1))
(hcov : U.1 ≤ ⨆ j, V.basicOpen (h j)) (x : F.obj U.1)
(hx : ∀ j, F.res (V.basicOpen_le (h j)) x = 0) : x = 0