Module

Scheme_Modules_zeroSchemeIdeal_comp_eq_of_isIso.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_zeroSchemeIdeal_comp_eq_of_isIso

1 declaration indexed from sourceView source ↗

Module documentation

Zero ideals are invariant under isomorphism

Postcomposing a module section with an isomorphism preserves its zero-scheme ideal.

Imports2

Imported by14

theorem

zeroSchemeIdeal_comp_eq_of_isIso

L34 ↗

AlgebraicGeometry.Scheme.Modules.zeroSchemeIdeal_comp_eq_of_isIso

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_zeroSchemeIdeal_comp_eq_of_isIso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.zeroSchemeIdeal_comp_eq_of_isIso
    {X : Scheme.{u}} {M M' : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (f : M ⟶ M') [IsIso f] :
    Scheme.Modules.zeroSchemeIdeal (s ≫ f) = Scheme.Modules.zeroSchemeIdeal s

Module documentation

Zero ideals are invariant under isomorphism

Declarations

zeroSchemeIdeal_comp_eq_of_isIso