Module

SubmoduleTopRestriction.lean

Nyll.SchemeTheory.Modules.SubmoduleTopRestriction

5 declarations indexed from sourceView source ↗

Module documentation

Whole submodules and restrictions on which they generate

The module of the top submodule is canonically the ambient module. If an actual native submodule equals the whole module on a slice, the geometric restriction of its inclusion is an isomorphism: each actual section map is the bijective inclusion of the full section submodule.

Imports6

Nyll.SchemeTheory.Modules.SubmoduleRestrictionComparison
Nyll.SchemeTheory.Modules.SubmoduleOverEquality
Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian
Mathlib.Algebra.Module.Submodule.Lattice
Mathlib.CategoryTheory.Functor.ReflectsIso.Basic

Imported by2

theorem

top_obj

L35 ↗

SheafOfModules.Submodule.top_obj

Documentation

The top sheaf submodule has the full section submodule on every object.

Source context 5 commands

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

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

Lean source · statement

theorem top_obj (M : SheafOfModules.{v} R) (U : Cᵒᵖ) :
    (⊤ : M.Submodule).toSubmodule.obj U = ⊤

def

topSectionEquiv

L48 ↗

SheafOfModules.Submodule.topSectionEquiv

Source context 5 commands

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

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

Lean source · full declaration

def topSectionEquiv (M : SheafOfModules.{v} R) (U : Cᵒᵖ) :
    (⊤ : M.Submodule).toSubmodule.obj U ≃ₗ[R.obj.obj U] M.val.obj U where
  toFun := Subtype.val
  invFun s := ⟨s, by rw [top_obj]; exact _root_.Submodule.mem_top⟩
  left_inv s := Subtype.ext rfl
  right_inv _ := rfl
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

def

topIso

L58 ↗

SheafOfModules.Submodule.topIso

Documentation

The module of the actual top submodule is the ambient module.

Source context 5 commands

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

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

Lean source · statement

def topIso (M : SheafOfModules.{v} R) :
    (⊤ : M.Submodule).toSheafOfModules ≅ M

theorem

topIso_hom

L66 ↗

SheafOfModules.Submodule.topIso_hom

Documentation

The top-submodule comparison is its actual inclusion.

Source context 5 commands

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

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

Lean source · statement

theorem topIso_hom (M : SheafOfModules.{v} R) :
    (topIso M).hom = (⊤ : M.Submodule).ι

theorem

isIso_restrictSubmoduleInclusion_of_over_eq_top

L79 ↗

AlgebraicGeometry.Scheme.Modules.isIso_restrictSubmoduleInclusion_of_over_eq_top

Documentation

Equality with the whole native module on an open makes the actual geometrically restricted inclusion an isomorphism.

Source context 4 commands

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

noncomputable section
universe u v v₁ u₁
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem isIso_restrictSubmoduleInclusion_of_over_eq_top
    {X : Scheme.{u}} {F : SheafOfModules.{u} X.ringCatSheaf}
    (N : F.Submodule) (U : X.Opens)
    (hN : N.over U = (⊤ : F.Submodule).over U) :
    IsIso ((restrictFunctor U.ι).map
      (submoduleAsModuleInclusion (F := (sheafOfModulesEquivalence X).inverse.obj F) N))

Module documentation

Whole submodules and restrictions on which they generate

Declarations

top_obj

topSectionEquiv

topIso

topIso_hom

isIso_restrictSubmoduleInclusion_of_over_eq_top