def CoherentSheaves.IsCoherentModule (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : Prop

An R-module M is coherent (in the textbook sense for affine schemes) iff it is finitely generated.

theorem CoherentSheaves.noetherian_coherent_iff_fp (R : Type u_1) [CommRing R] [IsNoetherianRing R] (M : Type u_2) [AddCommGroup M] [Module R M] : IsCoherentModule R M ↔ Module.FinitePresentation R M

Over a Noetherian ring, coherence is equivalent to finite presentation.

class CoherentSheaves.IsCoherentSheaf {X : AlgebraicGeometry.Scheme} (F : X.Modules) : Prop

A sheaf of modules F on a scheme X is coherent if it is quasi-coherent and of finite type.

• isQC : SheafOfModules.IsQuasicoherent F
• isFT : SheafOfModules.IsFiniteType F

@[implicit_reducible]

noncomputable instance CoherentSheaves.oX_modules_abelian (X : AlgebraicGeometry.Scheme) : CategoryTheory.Abelian X.Modules

The category of O_X-modules on a scheme X is abelian.

theorem CoherentSheaves.kernel_qc_of_qc {X : AlgebraicGeometry.Scheme} (F G : X.Modules) (hF : SheafOfModules.IsQuasicoherent F) (hG : SheafOfModules.IsQuasicoherent G) (φ : F ⟶ G) : SheafOfModules.IsQuasicoherent (CategoryTheory.Limits.kernel φ)

The kernel of a morphism between quasi-coherent sheaves is quasi-coherent.

theorem CoherentSheaves.affineCover_coversTop (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian X] : ∃ (I : Type u) (U : I → TopologicalSpace.Opens ↥X), (∀ (i : I), AlgebraicGeometry.IsAffineOpen (U i)) ∧ (Opens.grothendieckTopology ↥X).CoversTop U

A locally Noetherian scheme has an affine open cover that covers the topology.

theorem CoherentSheaves.kernel_over_affine_isFinitePresentation {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (F G : X.Modules) (hF_qc : SheafOfModules.IsQuasicoherent F) (hF_ft : SheafOfModules.IsFiniteType F) (hG_qc : SheafOfModules.IsQuasicoherent G) (φ : F ⟶ G) (U : TopologicalSpace.Opens ↥X) (hU : AlgebraicGeometry.IsAffineOpen U) : ((CategoryTheory.Limits.kernel φ).over U).IsFinitePresentation

Over an affine open of a locally Noetherian scheme, the kernel of a morphism of coherent sheaves is finitely presented.

theorem CoherentSheaves.kernel_ft_of_ft_locallyNoetherian {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (F G : X.Modules) (hF_qc : SheafOfModules.IsQuasicoherent F) (hF_ft : SheafOfModules.IsFiniteType F) (hG_qc : SheafOfModules.IsQuasicoherent G) (φ : F ⟶ G) : SheafOfModules.IsFiniteType (CategoryTheory.Limits.kernel φ)

On a locally Noetherian scheme, the kernel of a morphism from a finite-type quasi-coherent sheaf to another quasi-coherent sheaf is again of finite type.

theorem CoherentSheaves.kernel_coherent_sheaf (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian X] (F G : X.Modules) [IsCoherentSheaf F] [IsCoherentSheaf G] (φ : F ⟶ G) : IsCoherentSheaf (CategoryTheory.Limits.kernel φ)

The kernel of a morphism between coherent sheaves on a locally Noetherian scheme is coherent.

theorem CoherentSheaves.cokernel_isQuasicoherent (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian X] (F G : X.Modules) [IsCoherentSheaf F] [IsCoherentSheaf G] (φ : F ⟶ G) : (CategoryTheory.Limits.cokernel φ).IsQuasicoherent

The cokernel of a morphism between coherent sheaves on a locally Noetherian scheme is quasi-coherent.

theorem CoherentSheaves.cokernel_isFiniteType (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian X] (F G : X.Modules) [IsCoherentSheaf F] [IsCoherentSheaf G] (φ : F ⟶ G) : (CategoryTheory.Limits.cokernel φ).IsFiniteType

The cokernel of a morphism between coherent sheaves on a locally Noetherian scheme is of finite type.

theorem CoherentSheaves.cokernel_coherent_sheaf (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian X] (F G : X.Modules) [IsCoherentSheaf F] [IsCoherentSheaf G] (φ : F ⟶ G) : IsCoherentSheaf (CategoryTheory.Limits.cokernel φ)

The cokernel of a morphism between coherent sheaves on a locally Noetherian scheme is coherent.

theorem CoherentSheaves.ses_coherent_middle_sheaf (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian X] (F' F F'' : X.Modules) [IsCoherentSheaf F'] [IsCoherentSheaf F''] (i : F' ⟶ F) (p : F ⟶ F'') (hi : CategoryTheory.Mono i) (hp : CategoryTheory.Epi p) (hexact : CategoryTheory.CategoryStruct.comp i p = 0) : IsCoherentSheaf F

In a short exact sequence of O_X-modules where the outer terms are coherent, the middle term is coherent (the "two-out-of-three" property for coherent sheaves).

@[implicit_reducible]

instance CoherentSheaves.coherent_sheaves_abelian (R : Type u_1) [CommRing R] : CategoryTheory.Abelian (ModuleCat R)

The category of R-modules is abelian, for any commutative ring R.

theorem CoherentSheaves.lemma23_coherent_iff_fg_affine (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] : CoherentSpecFinitelyGenerated.IsLocallyFinitelyGenerated R M ↔ Module.Finite R M

Lemma 23 (Lec 12): on Spec A, the sheaf M̃ is coherent if and only if the module M is finitely generated, i.e. locally finitely generated equals finitely generated.

theorem CoherentSheaves.extension_of_sections {R : Type u_1} [CommRing R] (f : R) {M : Type u_2} [AddCommGroup M] [Module R M] (σ : LocalizedModule (Submonoid.powers f) M) : ∃ (m : M) (s : ↥(Submonoid.powers f)), σ = LocalizedModule.mk m s

Any element of the localized module M_f can be represented as m / f^n for some m ∈ M and n ∈ ℕ.