def AlgebraicGeometry.TorsionSheaf.IsTorsionSection {X : Scheme} (F : X.Modules) (U : X.Opens) (s : ↑(F.presheaf.obj (Opposite.op U))) : Prop

A section s of a sheaf of O_X-modules F over U is a torsion section iff it is annihilated by some nonzero scalar in O_X(U).

def AlgebraicGeometry.TorsionSheaf.IsTorsionSheaf {X : Scheme} (F : X.Modules) : Prop

A sheaf of O_X-modules is torsion iff every section over every nonempty open is a torsion section.

def AlgebraicGeometry.TorsionSheaf.IsTorsionFreeSheaf {X : Scheme} (F : X.Modules) : Prop

A sheaf of O_X-modules is torsion-free iff its only torsion section over any nonempty open is the zero section.

theorem AlgebraicGeometry.TorsionSheaf.isTorsionSection_iff_mem_torsion {X : Scheme} [IsIntegral X] (F : X.Modules) (U : X.Opens) [Nonempty ↥↑U] (s : ↑(F.presheaf.obj (Opposite.op U))) : IsTorsionSection F U s ↔ s ∈ Submodule.torsion ↑(X.presheaf.obj (Opposite.op U)) ↑(F.presheaf.obj (Opposite.op U))

On an integral scheme, being a torsion section coincides with membership in the torsion submodule of the sections, since O_X(U) is a domain.

noncomputable def AlgebraicGeometry.TorsionSheaf.torsionSections {X : Scheme} (F : X.Modules) (U : X.Opens) : Submodule ↑(X.presheaf.obj (Opposite.op U)) ↑(F.presheaf.obj (Opposite.op U))

The submodule of torsion sections of F over U.

@[simp]

theorem AlgebraicGeometry.TorsionSheaf.mem_torsionSections_iff {X : Scheme} [IsIntegral X] (F : X.Modules) (U : X.Opens) [Nonempty ↥↑U] (s : ↑(F.presheaf.obj (Opposite.op U))) : s ∈ torsionSections F U ↔ IsTorsionSection F U s

Membership in torsionSections F U is the same as being a torsion section.

theorem AlgebraicGeometry.TorsionSheaf.isTorsionFreeSheaf_iff_torsionSections_eq_bot {X : Scheme} [IsIntegral X] (F : X.Modules) : IsTorsionFreeSheaf F ↔ ∀ (U : X.Opens) [Nonempty ↥↑U], torsionSections F U = ⊥

A sheaf is torsion-free iff the torsion submodule of its sections is zero on every nonempty open.

theorem AlgebraicGeometry.TorsionSheaf.torsionSubsheaf_isCoherent (X : Scheme) [IsNoetherian X] [IsIntegral X] (F : X.Modules) : ∃ (T : X.Modules) (ι : T ⟶ F), (∀ (U : X.Opens), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Modules.Hom.app ι U))) ∧ ∀ (U : X.Opens) [Nonempty ↥↑U] (s : ↑(F.presheaf.obj (Opposite.op U))), (∃ (t : ↑(T.presheaf.obj (Opposite.op U))), (CategoryTheory.ConcreteCategory.hom (Scheme.Modules.Hom.app ι U)) t = s) ↔ IsTorsionSection F U s

Torsion subsheaf (Def 39, Lec 22): on a Noetherian integral scheme, for any sheaf of O_X-modules F there exists a subsheaf T ↪ F whose sections over any nonempty open are exactly the torsion sections of F.