Module

Scheme_Modules_hom_ext_of_isIso_fromTildeGamma.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_hom_ext_of_isIso_fromTildeGamma

1 declaration indexed from sourceView source ↗

Module documentation

Module morphisms determined by global sections

Detects equality of module morphisms from global sections when the affine comparison is invertible.

Imports2

Mathlib.AlgebraicGeometry.Modules.Tilde
Mathlib.Tactic.Ext

Imported by2

theorem

hom_ext_of_isIso_fromTildeGamma

L31 ↗

AlgebraicGeometry.Scheme.Modules.hom_ext_of_isIso_fromTildeGamma

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_hom_ext_of_isIso_fromTildeGamma
universe u
open CategoryTheory AlgebraicGeometry Opposite

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.hom_ext_of_isIso_fromTildeGamma {R :
  CommRingCat.{u}}
    {M N : (Spec (.of R)).Modules} [IsIso (Scheme.Modules.fromTildeΓ M)] (φ ψ : M ⟶ N)
    (h : ∀ m : Γ(M, ⊤), φ.app ⊤ m = ψ.app ⊤ m) : φ = ψ

Module documentation

Module morphisms determined by global sections

Declarations

hom_ext_of_isIso_fromTildeGamma