Directed unions as colimits of modules

A monotone family of submodules over a directed preorder defines a diagram in ModuleCat, with the submodule inclusions as transition maps. If its supremum is a submodule T, the inclusions into T exhibit ModuleCat.of R T as the colimit of this diagram.

The universal map is the linear map TauCeti.Submodule.iSupLift glued from the legs of an arbitrary cocone.

Main declarations

• TauCeti.ModuleCat.submoduleFunctor: the diagram associated to a monotone family of submodules.
• TauCeti.ModuleCat.submoduleCocone: the inclusion cocone into the supremum submodule.
• TauCeti.ModuleCat.submoduleCoconeIsColimit: the inclusion cocone is a colimit.

noncomputable def TauCeti.ModuleCat.submoduleFunctor {R : Type u} {M : Type v} {ι : Type x} [Ring R] [AddCommGroup M] [Module R M] [Preorder ι] (K : ι → Submodule R M) (hK : Monotone K) : CategoryTheory.Functor ι (ModuleCat R)

A monotone family of submodules, regarded as a diagram in ModuleCat whose maps are the canonical inclusions.

Equations

• TauCeti.ModuleCat.submoduleFunctor K hK = { obj := fun (i : ι) => ↧↥(K i), map := fun {X Y : ι} (f : X ⟶ Y) => ModuleCat.ofHom (Submodule.inclusion ⋯), map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem TauCeti.ModuleCat.submoduleFunctor_obj {R : Type u} {M : Type v} {ι : Type x} [Ring R] [AddCommGroup M] [Module R M] [Preorder ι] (K : ι → Submodule R M) (hK : Monotone K) (i : ι) : (submoduleFunctor K hK).obj i = ↧↥(K i)

The object at an index of the submodule diagram is the corresponding submodule.

@[simp]

theorem TauCeti.ModuleCat.submoduleFunctor_map {R : Type u} {M : Type v} {ι : Type x} [Ring R] [AddCommGroup M] [Module R M] [Preorder ι] (K : ι → Submodule R M) (hK : Monotone K) {i j : ι} (f : i ⟶ j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((submoduleFunctor K hK).map f) (CategoryTheory.eqToHom ⋯)) = ModuleCat.ofHom (Submodule.inclusion ⋯)

A map in the submodule diagram is the canonical inclusion.

noncomputable def TauCeti.ModuleCat.submoduleCocone {R : Type u} {M : Type v} {ι : Type x} [Ring R] [AddCommGroup M] [Module R M] [Preorder ι] (K : ι → Submodule R M) (hK : Monotone K) (T : Submodule R M) (hT : ⨆ (i : ι), K i = T) : CategoryTheory.Limits.Cocone (submoduleFunctor K hK)

The cocone from a monotone family of submodules to a submodule equal to their supremum.

Equations

• TauCeti.ModuleCat.submoduleCocone K hK T hT = { pt := ↧↥T, ι := { app := fun (i : ι) => ModuleCat.ofHom (Submodule.inclusion ⋯), naturality := ⋯ } }

@[simp]

theorem TauCeti.ModuleCat.submoduleCocone_pt {R : Type u} {M : Type v} {ι : Type x} [Ring R] [AddCommGroup M] [Module R M] [Preorder ι] (K : ι → Submodule R M) (hK : Monotone K) (T : Submodule R M) (hT : ⨆ (i : ι), K i = T) : (submoduleCocone K hK T hT).pt = ↧↥T

The point of the directed-submodule cocone is the module carried by the supremum.

@[simp]

theorem TauCeti.ModuleCat.submoduleCocone_ι_app {R : Type u} {M : Type v} {ι : Type x} [Ring R] [AddCommGroup M] [Module R M] [Preorder ι] (K : ι → Submodule R M) (hK : Monotone K) (T : Submodule R M) (hT : ⨆ (i : ι), K i = T) (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((submoduleCocone K hK T hT).ι.app i) (CategoryTheory.eqToHom ⋯)) = ModuleCat.ofHom (Submodule.inclusion ⋯)

A leg of the directed-submodule cocone is the corresponding submodule inclusion.

noncomputable def TauCeti.ModuleCat.submoduleCoconeIsColimit {R : Type u} {M : Type v} {ι : Type x} [Ring R] [AddCommGroup M] [Module R M] [Preorder ι] [IsDirectedOrder ι] (K : ι → Submodule R M) (hK : Monotone K) (T : Submodule R M) (hT : ⨆ (i : ι), K i = T) : CategoryTheory.Limits.IsColimit (submoduleCocone K hK T hT)

A submodule equal to the supremum of a monotone family over a directed preorder is the colimit of that family in ModuleCat.

Equations

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