Submodules of sheaves of modules

Given a sheaf of modules M, a SheafOfModules.Submodule M is a submodule N of its underlying presheaf of modules whose membership condition is local.

Main definitions

• SheafOfModules.Submodule: a submodule of (the underlying presheaf of modules of) a sheaf of modules whose membership is local.
• SheafOfModules.Submodule.toSheafOfModules: the associated sheaf of modules.

structure SheafOfModules.Submodule {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) extends M.val.Submodule : Type (max u₁ v)

A submodule of a sheaf of modules M: a submodule N of the underlying presheaf of modules whose membership condition is local.

• obj (X : Cᵒᵖ) : _root_.Submodule ↑(R.obj.obj X) ↑(M.val.obj X)
• map {X Y : Cᵒᵖ} (f : X ⟶ Y) : self.obj X ≤ Submodule.comap (M.val.restrictₛₗ f) (self.obj Y)
• isSheaf ⦃X : Cᵒᵖ⦄ (s : ↑(M.val.obj X)) : self.toSubfunctor.sieveOfSection s ∈ J (Opposite.unop X) → s ∈ self.obj X

theorem SheafOfModules.Submodule.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} {N₁ N₂ : M.Submodule} (h : N₁.toSubmodule = N₂.toSubmodule) : N₁ = N₂

theorem SheafOfModules.Submodule.ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} {N₁ N₂ : M.Submodule} : N₁ = N₂ ↔ N₁.toSubmodule = N₂.toSubmodule

noncomputable def SheafOfModules.Submodule.toSheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (N : M.Submodule) : SheafOfModules R

The sheaf of modules associated to a submodule of a sheaf of modules.

Equations

• N.toSheafOfModules = { val := N.toPresheafOfModules, isSheaf := ⋯ }

noncomputable def SheafOfModules.Submodule.ι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (N : M.Submodule) : N.toSheafOfModules ⟶ M

The inclusion of the sheaf of modules associated to a submodule N into M.

Equations

• N.ι = { val := N.ι }

@[simp]

theorem SheafOfModules.Submodule.ι_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (N : M.Submodule) : N.ι.val = N.ι

instance SheafOfModules.Submodule.instMonoι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (N : M.Submodule) : CategoryTheory.Mono N.ι

@[instance_reducible]

instance SheafOfModules.Submodule.instPartialOrder {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} : PartialOrder M.Submodule

Equations

• SheafOfModules.Submodule.instPartialOrder = PartialOrder.lift SheafOfModules.Submodule.toSubmodule ⋯

theorem SheafOfModules.Submodule.le_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} {N₁ N₂ : M.Submodule} : N₁ ≤ N₂ ↔ N₁.toSubmodule ≤ N₂.toSubmodule

@[instance_reducible]

instance SheafOfModules.Submodule.instInfSet {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} : InfSet M.Submodule

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance SheafOfModules.Submodule.instMin {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} : Min M.Submodule

Equations

• SheafOfModules.Submodule.instMin = { min := fun (N₁ N₂ : M.Submodule) => let __Submodule := N₁.toSubmodule ⊓ N₂.toSubmodule; { toSubmodule := __Submodule, isSheaf := ⋯ } }

@[instance_reducible]

noncomputable instance SheafOfModules.Submodule.instCompleteLattice {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} : CompleteLattice M.Submodule

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SheafOfModules.Submodule.toSubmodule_sInf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (s : Set M.Submodule) : (sInf s).toSubmodule = sInf ((fun (x : M.Submodule) => x.toSubmodule) '' s)

@[simp]

theorem SheafOfModules.Submodule.toSubmodule_iInf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} {ι : Sort u_1} (N : ι → M.Submodule) : (⨅ (i : ι), N i).toSubmodule = ⨅ (i : ι), (N i).toSubmodule

@[simp]

theorem SheafOfModules.Submodule.toSubmodule_inf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (N₁ N₂ : M.Submodule) : (N₁ ⊓ N₂).toSubmodule = N₁.toSubmodule ⊓ N₂.toSubmodule