Module

KernelSubmodule.lean

Nyll.SchemeTheory.Modules.KernelSubmodule

6 declarations indexed from sourceView source ↗

Module documentation

Actual kernel subsheaves of modules

The kernel is the native submodule consisting, on each object, of the sections killed by the actual component morphism. Membership is local by separatedness of the target sheaf. Evaluation identifies its kernel fork with the ordinary linear-map kernel, giving the actual categorical comparison.

Imports5

Mathlib.Algebra.Category.ModuleCat.Sheaf.Submodule
Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
Mathlib.Algebra.Category.ModuleCat.Kernels
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Imported by3

def

kernelSubmodule

L34 ↗

PresheafOfModules.kernelSubmodule

Documentation

The actual sectionwise kernel submodule of a morphism of presheaves of modules. Its restriction compatibility is the naturality of the morphism.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Limits Opposite
namespace PresheafOfModules
variable {C : Type u} [Category.{v} C] {R : Cᵒᵖ ⥤ RingCat.{u}}

Lean source · full declaration

def kernelSubmodule {M N : PresheafOfModules.{u} R} (φ : M ⟶ N) : M.Submodule where
  obj X := (φ.app X).hom.ker
  map {X Y} i := by
    intro x hx
    change (φ.app X).hom x = 0 at hx
    change (φ.app Y).hom (M.map i x) = 0
    exact (PresheafOfModules.naturality_apply φ i x).trans
      ((congrArg (fun y : N.obj X => N.map i y) hx).trans
        (map_zero (N.map i).hom))

def

kernelSubmodule

L53 ↗

SheafOfModules.kernelSubmodule

Documentation

The native kernel subsheaf, constructed from local vanishing of the actual target section.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Limits Opposite
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}

Lean source · full declaration

def kernelSubmodule {M N : SheafOfModules.{u} R} (φ : M ⟶ N) : M.Submodule where
  toSubmodule := PresheafOfModules.kernelSubmodule φ.val
  isSheaf {X} s hs := by
    have hN : Presieve.IsSheaf J
        (N.val.presheaf ⋙ CategoryTheory.forget AddCommGrpCat.{u}) := by
      rw [← isSheaf_iff_isSheaf_of_type]
      exact GrothendieckTopology.HasSheafCompose.isSheaf _ N.isSheaf
    apply LinearMap.mem_ker.mpr
    apply (hN _ hs).isSeparatedFor.ext
    intro V i hi
    change (φ.val.app (op V)).hom (M.val.map i.op s) = 0 at hi
    change N.val.map i.op ((φ.val.app X).hom s) = N.val.map i.op (0 : N.val.obj X)
    exact (PresheafOfModules.naturality_apply φ.val i.op s).symm.trans
      (hi.trans (map_zero (N.val.map i.op).hom).symm)

theorem

kernelSubmodule_ι_comp

L68 ↗

SheafOfModules.kernelSubmodule_ι_comp

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Limits Opposite
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}

Lean source · statement

theorem kernelSubmodule_ι_comp
    {M N : SheafOfModules.{u} R} (φ : M ⟶ N) :
    (kernelSubmodule φ).ι ≫ φ = 0

def

kernelSubmoduleIsLimit

L80 ↗

SheafOfModules.kernelSubmoduleIsLimit

Documentation

The inclusion of the actual kernel subsheaf is a kernel fork.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Limits Opposite
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}

Lean source · statement

def kernelSubmoduleIsLimit
    {M N : SheafOfModules.{u} R} (φ : M ⟶ N) :
    IsLimit (KernelFork.ofι (kernelSubmodule φ).ι (kernelSubmodule_ι_comp φ))

def

kernelSubmoduleIso

L94 ↗

SheafOfModules.kernelSubmoduleIso

Documentation

The native sectionwise kernel subsheaf is the actual categorical kernel.

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Limits Opposite
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}

Lean source · statement

def kernelSubmoduleIso
    {M N : SheafOfModules.{u} R} (φ : M ⟶ N) :
    (kernelSubmodule φ).toSheafOfModules ≅ kernel φ

theorem

kernelSubmoduleIso_hom_ι

L99 ↗

SheafOfModules.kernelSubmoduleIso_hom_ι

Source context 5 commands

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

noncomputable section
universe v u
open CategoryTheory Limits Opposite
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}

Lean source · statement

theorem kernelSubmoduleIso_hom_ι
    {M N : SheafOfModules.{u} R} (φ : M ⟶ N) :
    (kernelSubmoduleIso φ).hom ≫ kernel.ι φ = (kernelSubmodule φ).ι

Module documentation

Actual kernel subsheaves of modules

Declarations

kernelSubmodule

kernelSubmodule

kernelSubmodule_ι_comp

kernelSubmoduleIsLimit

kernelSubmoduleIso

kernelSubmoduleIso_hom_ι