NYLL
Module

ImageSubmodule.lean

Nyll.SchemeTheory.Modules.ImageSubmodule
8 declarations indexed from sourceView source ↗

Module documentation

Actual image subsheaves

The image is the native kernel submodule of the actual cokernel projection. Its comparison with the abelian image gives an epimorphic corestriction, and the categorical image universal property gives its least-submodule property.

Imports5
Imported by4

Declarations

def

imageSubmodule

L34 ↗
SheafOfModules.imageSubmodule
Documentation

The actual image subsheaf, including its local membership condition.

Source context 5 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
Lean source · statement
def imageSubmodule {M N : SheafOfModules.{u} R} (f : M ⟶ N) : N.Submodule
def

imageSubmoduleIso

L38 ↗
SheafOfModules.imageSubmoduleIso
Documentation

The actual image subsheaf agrees with the abelian image.

Source context 5 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
Lean source · statement
def imageSubmoduleIso {M N : SheafOfModules.{u} R} (f : M ⟶ N) :
    (imageSubmodule f).toSheafOfModules ≅ Abelian.image f
theorem

imageSubmoduleIso_hom_ι

L43 ↗
SheafOfModules.imageSubmoduleIso_hom_ι
Documentation

The abelian-image comparison respects the actual inclusion into the target.

Source context 5 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
Lean source · statement
theorem imageSubmoduleIso_hom_ι {M N : SheafOfModules.{u} R} (f : M ⟶ N) :
    (imageSubmoduleIso f).hom ≫ Abelian.image.ι f = (imageSubmodule f).ι
def

toImageSubmodule

L48 ↗
SheafOfModules.toImageSubmodule
Documentation

The actual epimorphism from the source onto its native image subsheaf.

Source context 5 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
Lean source · statement
def toImageSubmodule {M N : SheafOfModules.{u} R} (f : M ⟶ N) :
    M ⟶ (imageSubmodule f).toSheafOfModules
instance

(anonymous instance)

L52 ↗
Source context 5 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
Lean source · statement
instance {M N : SheafOfModules.{u} R} (f : M ⟶ N) :
    Epi (toImageSubmodule f)
theorem

toImageSubmodule_ι

L57 ↗
SheafOfModules.toImageSubmodule_ι
Documentation

The corestriction retains the original map into the ambient sheaf.

Source context 5 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
Lean source · statement
theorem toImageSubmodule_ι {M N : SheafOfModules.{u} R} (f : M ⟶ N) :
    toImageSubmodule f ≫ (imageSubmodule f).ι = f
theorem

imageSubmodule_le

L63 ↗
SheafOfModules.imageSubmodule_le
Documentation

Every actual factorization through a native submodule contains the image.

Source context 5 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
Lean source · statement
theorem imageSubmodule_le {M N : SheafOfModules.{u} R} (f : M ⟶ N)
    (P : N.Submodule) (g : M ⟶ P.toSheafOfModules) (hg : g ≫ P.ι = f) :
    imageSubmodule f ≤ P
theorem

isFiniteType_imageSubmodule

L78 ↗
SheafOfModules.isFiniteType_imageSubmodule
Documentation

An actual image of a finite-type sheaf is finite type.

Source context 6 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
variable [HasBinaryProducts C]
  [∀ X : C, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X : C, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
Lean source · statement
theorem isFiniteType_imageSubmodule {M N : SheafOfModules.{u} R}
    (f : M ⟶ N) [M.IsFiniteType] : (imageSubmodule f).toSheafOfModules.IsFiniteType

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