NYLL
Module

SubmoduleRestrictedSections.lean

Nyll.SchemeTheory.Modules.SubmoduleRestrictedSections
2 declarations indexed from sourceView source ↗

Module documentation

Actual membership from a lifted section on an open subscheme

The top-section restriction comparison is natural in the actual module. A lift through the restricted inclusion therefore gives an element of the original native section submodule. This supplies the containment step after the geometric kernel extension has recovered its prescribed local module.

Imports2
Imported by2

Declarations

theorem

openTopSectionsIso_hom_naturality

L28 ↗
AlgebraicGeometry.Scheme.Modules.openTopSectionsIso_hom_naturality
Documentation

The actual top-section comparison respects module morphisms.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem openTopSectionsIso_hom_naturality
    {X : Scheme.{u}} {F G : X.Modules} (φ : F ⟶ G) (U : X.Opens) :
    (openTopSectionsIso F U).hom ≫ φ.app U =
      ((restrictFunctor U.ι).map φ).app ⊤ ≫ (openTopSectionsIso G U).hom
theorem

mem_submodule_of_restrict_lift

L41 ↗
AlgebraicGeometry.Scheme.Modules.mem_submodule_of_restrict_lift
Documentation

An actual lift on the open subscheme proves membership in the original native section submodule.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem mem_submodule_of_restrict_lift
    {X : Scheme.{u}} {F : X.Modules} (H : F.Submodule) (U : X.Opens)
    (x : F.val.obj (op U))
    (t : Γ((submoduleAsModule H).restrict U.ι, ⊤))
    (ht : (openTopSectionsIso F U).hom
      (((restrictFunctor U.ι).map (submoduleAsModuleInclusion H)).app ⊤ t) = x) :
    x ∈ H.toSubmodule.obj (op U)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.