Submodules of presheaves of modules

Given a presheaf of modules M over a presheaf of rings R and a family of submodules N X of M.obj X that is stable under the restriction maps of M, we construct the corresponding subobject of M in the category PresheafOfModules R.

Main definitions

• PresheafOfModules.Submodule M: a family of submodules of M, stable under restriction.
• PresheafOfModules.Submodule.toPresheafOfModules: the associated presheaf of modules.

The families of submodules of M form a CompleteLattice, with all the lattice operations computed pointwise.

structure PresheafOfModules.Submodule {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : Type (max u₁ v)

A family of submodules N X of M.obj X, for a presheaf of modules M, stable under the restriction maps of M. This defines a subobject of M in PresheafOfModules R.

• obj (X : Cᵒᵖ) : _root_.Submodule ↑(R.obj X) ↑(M.obj X)

  the submodule of M.obj X

• map {X Y : Cᵒᵖ} (f : X ⟶ Y) : self.obj X ≤ Submodule.comap (M.restrictₛₗ f) (self.obj Y)

  the family is stable under restriction

theorem PresheafOfModules.Submodule.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} {N₁ N₂ : M.Submodule} (h : ∀ (X : Cᵒᵖ), N₁.obj X = N₂.obj X) : N₁ = N₂

theorem PresheafOfModules.Submodule.ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} {N₁ N₂ : M.Submodule} : N₁ = N₂ ↔ ∀ (X : Cᵒᵖ), N₁.obj X = N₂.obj X

theorem PresheafOfModules.Submodule.map_mem {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (N : M.Submodule) {X Y : Cᵒᵖ} (f : X ⟶ Y) {x : ↑(M.obj X)} (hx : x ∈ N.obj X) : (CategoryTheory.ConcreteCategory.hom (M.map f)) x ∈ N.obj Y

noncomputable def PresheafOfModules.Submodule.toPresheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (N : M.Submodule) : PresheafOfModules R

The presheaf of modules associated to a submodule.

Equations

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

@[simp]

theorem PresheafOfModules.Submodule.toPresheafOfModules_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (N : M.Submodule) (X : Cᵒᵖ) : N.toPresheafOfModules.obj X = ModuleCat.of ↑(R.obj X) ↥(N.obj X)

@[simp]

theorem PresheafOfModules.Submodule.toPresheafOfModules_map_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (N : M.Submodule) {X Y : Cᵒᵖ} (f : X ⟶ Y) (m : ↥(N.obj X)) : ↑((CategoryTheory.ConcreteCategory.hom (N.toPresheafOfModules.map f)) m) = (CategoryTheory.ConcreteCategory.hom (M.map f)) ↑m

noncomputable def PresheafOfModules.Submodule.ι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (N : M.Submodule) : N.toPresheafOfModules ⟶ M

The inclusion of a submodule into the ambient presheaf of modules.

Equations

• N.ι = PresheafOfModules.homMk { app := fun (X : Cᵒᵖ) => AddCommGrpCat.ofHom (N.obj X).subtype.toAddMonoidHom, naturality := ⋯ } ⋯

@[simp]

theorem PresheafOfModules.Submodule.ι_app_hom_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (N : M.Submodule) (X : Cᵒᵖ) (a : ↑(N.toPresheafOfModules.presheaf.obj X)) : (ModuleCat.Hom.hom (N.ι.app X)) a = (CategoryTheory.ConcreteCategory.hom (AddCommGrpCat.ofHom (N.obj X).subtype.toAddMonoidHom)) a

instance PresheafOfModules.Submodule.instMonoι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (N : M.Submodule) : CategoryTheory.Mono N.ι

@[implicit_reducible]

instance PresheafOfModules.Submodule.instPartialOrder {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} : PartialOrder M.Submodule

Equations

• PresheafOfModules.Submodule.instPartialOrder = PartialOrder.lift PresheafOfModules.Submodule.obj ⋯

theorem PresheafOfModules.Submodule.le_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} {N₁ N₂ : M.Submodule} : N₁ ≤ N₂ ↔ ∀ (X : Cᵒᵖ), N₁.obj X ≤ N₂.obj X

noncomputable def PresheafOfModules.Submodule.homOfLE {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} {N₁ N₂ : M.Submodule} (hle : N₁ ≤ N₂) : N₁.toPresheafOfModules ⟶ N₂.toPresheafOfModules

If N₁ and N₂ are submodule with N₁ ≤ N₂, this is the associated inclusion of presheaves of modules.

Equations

• PresheafOfModules.Submodule.homOfLE hle = PresheafOfModules.homMk { app := fun (X : Cᵒᵖ) => AddCommGrpCat.ofHom (Submodule.inclusion ⋯).toAddMonoidHom, naturality := ⋯ } ⋯

@[simp]

theorem PresheafOfModules.Submodule.homOfLE_app_hom_apply_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} {N₁ N₂ : M.Submodule} (hle : N₁ ≤ N₂) (X : Cᵒᵖ) (a : ↑(N₁.toPresheafOfModules.presheaf.obj X)) : ↑((ModuleCat.Hom.hom ((homOfLE hle).app X)) a) = ↑a

instance PresheafOfModules.Submodule.instMonoHomOfLE {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (N₁ N₂ : M.Submodule) (hle : N₁ ≤ N₂) : CategoryTheory.Mono (homOfLE hle)

@[simp]

theorem PresheafOfModules.Submodule.homOfLE_ι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} {N₁ N₂ : M.Submodule} (hle : N₁ ≤ N₂) : CategoryTheory.CategoryStruct.comp (homOfLE hle) N₂.ι = N₁.ι

@[simp]

theorem PresheafOfModules.Submodule.homOfLE_ι_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} {N₁ N₂ : M.Submodule} (hle : N₁ ≤ N₂) {Z : PresheafOfModules R} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (homOfLE hle) (CategoryTheory.CategoryStruct.comp N₂.ι h) = CategoryTheory.CategoryStruct.comp N₁.ι h

@[implicit_reducible]

instance PresheafOfModules.Submodule.instCompleteLattice {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} : CompleteLattice M.Submodule

Equations

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

@[simp]

theorem PresheafOfModules.Submodule.bot_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (X : Cᵒᵖ) : ⊥.obj X = ⊥ X

@[simp]

theorem PresheafOfModules.Submodule.sSup_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s : Set M.Submodule) (X : Cᵒᵖ) : (sSup s).obj X = ⨆ N ∈ s, N.obj X

@[simp]

theorem PresheafOfModules.Submodule.sInf_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s : Set M.Submodule) (X : Cᵒᵖ) : (sInf s).obj X = ⨅ N ∈ s, N.obj X

@[simp]

theorem PresheafOfModules.Submodule.top_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (X : Cᵒᵖ) : ⊤.obj X = ⊤ X

@[simp]

theorem PresheafOfModules.Submodule.sup_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (F G : M.Submodule) (X : Cᵒᵖ) : (SemilatticeSup.sup F G).obj X = F.obj X ⊔ G.obj X

@[simp]

theorem PresheafOfModules.Submodule.inf_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (F G : M.Submodule) (X : Cᵒᵖ) : (Lattice.inf F G).obj X = F.obj X ⊓ G.obj X