NYLL
Module

OModulePresheaf_isQuasicoherent_coker.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_isQuasicoherent_coker
2 declarations indexed from sourceView source ↗

Module documentation

Quasicoherence of the cokernel of a morphism of quasicoherent module presheaves.

Imports4
Imported by2

Declarations

theorem

isQuasicoherent_coker

L47 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_coker.AlgebraicGeometry.OModulePresheaf.G4T.isQuasicoherent_coker
Source context 18 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_coker
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_coker (hG : OModulePresheaf.IsQuasicoherent G)
    (hF : OModulePresheaf.IsQuasicoherent F) :
    OModulePresheaf.IsQuasicoherent (OModulePresheaf.coker φ)
theorem

isQuasicoherent_coker

L74 ↗
AlgebraicGeometry.OModulePresheaf.isQuasicoherent_coker
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_coker
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
universe u
open _root_.AlgebraicCurves.Cohomology.Sheaves.Proofs in
open _root_.AlgebraicGeometry OModulePresheaf_isQuasicoherent_coker.AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.isQuasicoherent_coker {R : Type u} [CommRing R]
    {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} {F G : OModulePresheaf π} (φ : OModulePresheaf.Hom F
    G) (hG : G.IsQuasicoherent) (hF : F.IsQuasicoherent) : (OModulePresheaf.coker
    φ).IsQuasicoherent

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.