theorem
L47 ↗isQuasicoherent_ker
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_ker.AlgebraicGeometry.OModulePresheaf.G4T.isQuasicoherent_ker
Source context 18 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_ker
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 isQuasicoherent_ker (hF : OModulePresheaf.IsQuasicoherent F)
(hG : OModulePresheaf.IsQuasicoherent G) :
OModulePresheaf.IsQuasicoherent (OModulePresheaf.ker φ)