Module

AffineFiniteSubmodule.lean

Nyll.SchemeTheory.Modules.AffineFiniteSubmodule

7 declarations indexed from sourceView source ↗

Module documentation

Actual affine subsheaves generated by module sections

A submodule of the affine global-section module gives an actual morphism from its tilde sheaf to the ambient module by the native tilde--Gamma adjunction. Its native image is a sheaf submodule. The unit identity proves that it contains the specified actual sections; finite module generators give a finite-type subsheaf through the actual epimorphism onto the image.

Imports6

Nyll.SchemeTheory.Modules.ImageSubmodule
Nyll.SchemeTheory.Modules.FiniteTypeTilde
Nyll.SchemeTheory.Modules.QuasicoherentLocal
Nyll.SchemeTheory.Modules.QuasicoherentImage
Mathlib.AlgebraicGeometry.Modules.Tilde
Mathlib.CategoryTheory.Adjunction.Basic

Imported by2

def

affineSubmoduleInclusion

L36 ↗

AlgebraicGeometry.Scheme.Modules.affineSubmoduleInclusion

Documentation

The bundled inclusion retains the actual affine global-section module and its existing scalar structure.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {R : CommRingCat.{u}} (F : (Spec R).Modules)

Lean source · statement

def affineSubmoduleInclusion
    (K : Submodule R ((moduleSpecΓFunctor (R := R)).obj F)) :
    ModuleCat.of R K ⟶ (moduleSpecΓFunctor (R := R)).obj F

def

affineSubmoduleMap

L42 ↗

AlgebraicGeometry.Scheme.Modules.affineSubmoduleMap

Documentation

The actual morphism determined by inclusion of a submodule of global sections.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {R : CommRingCat.{u}} (F : (Spec R).Modules)

Lean source · statement

def affineSubmoduleMap
    (K : Submodule R ((moduleSpecΓFunctor (R := R)).obj F)) :
    (tilde.functor R).obj (ModuleCat.of R K) ⟶ F

theorem

affineSubmoduleMap_globalSections

L50 ↗

AlgebraicGeometry.Scheme.Modules.affineSubmoduleMap_globalSections

Documentation

The global-section component of the constructed map is the actual inclusion, under the canonical tilde global-section isomorphism.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {R : CommRingCat.{u}} (F : (Spec R).Modules)

Lean source · statement

theorem affineSubmoduleMap_globalSections
    (K : Submodule R ((moduleSpecΓFunctor (R := R)).obj F)) :
    (tilde.isoTop (ModuleCat.of R K)).hom ≫
        (moduleSpecΓFunctor (R := R)).map (affineSubmoduleMap F K) =
      affineSubmoduleInclusion F K

def

affineSubmodule

L61 ↗

AlgebraicGeometry.Scheme.Modules.affineSubmodule

Documentation

The native image of the actual affine morphism generated by K.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {R : CommRingCat.{u}} (F : (Spec R).Modules)

Lean source · statement

def affineSubmodule
    (K : Submodule R ((moduleSpecΓFunctor (R := R)).obj F)) : F.Submodule

theorem

mem_affineSubmodule_globalSections

L67 ↗

AlgebraicGeometry.Scheme.Modules.mem_affineSubmodule_globalSections

Documentation

Every specified global section belongs to the actual generated subsheaf.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {R : CommRingCat.{u}} (F : (Spec R).Modules)

Lean source · statement

theorem mem_affineSubmodule_globalSections
    (K : Submodule R ((moduleSpecΓFunctor (R := R)).obj F))
    (s : (moduleSpecΓFunctor (R := R)).obj F) (hs : s ∈ K) :
    s ∈ (affineSubmodule F K).toSubmodule.obj (op ⊤)

theorem

isFiniteType_affineSubmodule

L83 ↗

AlgebraicGeometry.Scheme.Modules.isFiniteType_affineSubmodule

Documentation

Finite module generators produce an actual native submodule of finite type.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {R : CommRingCat.{u}} (F : (Spec R).Modules)

Lean source · statement

theorem isFiniteType_affineSubmodule
    (K : Submodule R ((moduleSpecΓFunctor (R := R)).obj F)) (hK : K.FG) :
    (affineSubmodule F K).toSheafOfModules.IsFiniteType

theorem

isQuasicoherent_affineSubmodule

L95 ↗

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_affineSubmodule

Documentation

In a quasicoherent ambient module, the actual affine generated submodule is quasicoherent.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
variable {R : CommRingCat.{u}} (F : (Spec R).Modules)

Lean source · statement

theorem isQuasicoherent_affineSubmodule [F.IsQuasicoherent]
    (K : Submodule R ((moduleSpecΓFunctor (R := R)).obj F)) :
    (affineSubmodule F K).toSheafOfModules.IsQuasicoherent

Module documentation

Actual affine subsheaves generated by module sections

Declarations

affineSubmoduleInclusion

affineSubmoduleMap

affineSubmoduleMap_globalSections

affineSubmodule

mem_affineSubmodule_globalSections

isFiniteType_affineSubmodule

isQuasicoherent_affineSubmodule