Module

Scheme_Modules_zeroSchemeIdeal_comp_le.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_zeroSchemeIdeal_comp_le

5 declarations indexed from sourceView source ↗

Module documentation

The zero ideal after postcomposition

The zero-scheme ideal of a postcomposed module section is contained in the zero-scheme ideal of the original section.

Imports1

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesSectionZeroScheme

Imported by2

theorem

restrictFunctor_map_app

L39 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_zeroSchemeIdeal_comp_le.ZSCompSol.restrictFunctor_map_app

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_zeroSchemeIdeal_comp_le
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace ZSCompSol
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M M' : X.Modules}

Lean source · statement

theorem restrictFunctor_map_app {U : Scheme.{u}} (i : U ⟶ X) [IsOpenImmersion i] (f : M ⟶ M')
    (W : U.Opens) : ((Scheme.Modules.restrictFunctor i).map f).app W = f.app (i ''ᵁ W)

theorem

restrictSection_comp

L42 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_zeroSchemeIdeal_comp_le.ZSCompSol.restrictSection_comp

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_zeroSchemeIdeal_comp_le
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace ZSCompSol
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M M' : X.Modules}

Lean source · statement

theorem restrictSection_comp (s : 𝟙_ X.Modules ⟶ M) (f : M ⟶ M') (U : X.Opens) :
    restrictSection (s ≫ f) U = ((Scheme.Modules.restrictFunctor U.ι).map f).app ⊤
        (restrictSection s U)

theorem

coeff_comp

L47 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_zeroSchemeIdeal_comp_le.ZSCompSol.coeff_comp

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_zeroSchemeIdeal_comp_le
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace ZSCompSol
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M M' : X.Modules}

Lean source · statement

theorem coeff_comp (s : 𝟙_ X.Modules ⟶ M) (f : M ⟶ M') (U : X.Opens)
    (φ : M'.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) :
    coeff (s ≫ f) U φ = coeff s U ((Scheme.Modules.restrictFunctor U.ι).map f ≫ φ)

theorem

coeffIdeal_comp_le

L52 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_zeroSchemeIdeal_comp_le.ZSCompSol.coeffIdeal_comp_le

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_zeroSchemeIdeal_comp_le
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
namespace ZSCompSol
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M M' : X.Modules}

Lean source · statement

theorem coeffIdeal_comp_le (s : 𝟙_ X.Modules ⟶ M) (f : M ⟶ M') (U : X.Opens) :
    coeffIdeal (s ≫ f) U ≤ coeffIdeal s U

theorem

zeroSchemeIdeal_comp_le

L60 ↗

AlgebraicGeometry.Scheme.Modules.zeroSchemeIdeal_comp_le

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_le
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_le
    {X : Scheme.{u}} {M M' : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (f : M ⟶ M') :
    Scheme.Modules.zeroSchemeIdeal (s ≫ f) ≤ Scheme.Modules.zeroSchemeIdeal s

Module documentation

The zero ideal after postcomposition

Declarations

restrictFunctor_map_app

restrictSection_comp

coeff_comp

coeffIdeal_comp_le

zeroSchemeIdeal_comp_le