Module

Scheme_Modules_Hom_mono_iff_injective.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_Hom_mono_iff_injective

1 declaration indexed from sourceView source ↗

Module documentation

Monomorphisms of module sheaves

Characterizes monomorphisms of scheme modules by injectivity on sections.

Imports4

Mathlib.Algebra.Category.Grp.EpiMono
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.Tactic.Ext
Mathlib.Tactic.TermCongr

Imported by7

theorem

mono_iff_injective

L33 ↗

AlgebraicGeometry.Scheme.Modules.Hom.mono_iff_injective

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_Hom_mono_iff_injective
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.Hom.mono_iff_injective
    {X : Scheme.{u}} {M N : X.Modules} (φ : M ⟶ N) :
    Mono φ ↔ ∀ U : X.Opens, Function.Injective (φ.app U)

Module documentation

Monomorphisms of module sheaves

Declarations

mono_iff_injective