Modules over a monoid object form an abelian category

Mathlib's CategoryTheory.Mod D A carries no additive structure. This file supplies it, for A a monoid object in a monoidally preadditive category D, and upgrades it to an abelian structure when D is abelian and tensoring on the left is right exact.

Everything is computed in D and transported along the forgetful functor:

• hom-groups are the subgroups of D's hom-groups cut out by the intertwining condition — closed under addition because A ◁ − is additive;
• the zero module is the zero object of D with the zero action, and the biproduct of RS.modBiprod exhibits binary biproducts;
• the kernel of a module map is the kernel of its underlying morphism, with the action restricted by the universal property of the kernel: no exactness hypothesis is needed, since the restricted action is produced by kernel.lift;
• the cokernel is the cokernel of the underlying morphism, with the action descended along A ◁ cokernel.π; here right exactness of Z ◁ − is what makes the descent possible, and the module laws are checked after cancelling the epimorphisms 𝟙_ D ◁ cokernel.π and (A ⊗ A) ◁ cokernel.π;
• a module map is a monomorphism exactly when its underlying morphism is, and likewise for epimorphisms, so normality in D transports: the route to CategoryTheory.Abelian is the normality route, as for super modules in RS/Classical/Deligne/SuperModAbelian.lean.

The second half of the file is independent of module theory: in any abelian category, a subobject of a finite direct sum of simple objects is the direct sum of a sublist of them, and dually for quotients. The engine is RS.idxSum, the direct sum of a list of indices into a family of objects, and the two theorems RS.exists_sublist_iso_of_mono/RS.exists_sublist_iso_of_epi are proved by induction on the list from the two splitting lemmas RS.isoBiprodOfRetraction/RS.isoBiprodOfSection: at each step the intersection with the leading summand is a subobject of a simple object, hence zero or the whole of it, and in either case the inclusion of the kernel is split. The specialisations to a Fin n-indexed biproduct (RS.exists_sublist_iso_biproduct_of_mono and its epimorphism companion) and to a sum of copies of two simple objects (RS.exists_mixSum_iso_of_mono and its companion) follow.

The additive structure on module maps

theorem RS.zero_lin {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} : CategoryTheory.CategoryStruct.comp (actLeft A M.X) 0 = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A 0) (actLeft A N.X)

The zero morphism of carriers intertwines the actions.

theorem RS.add_lin {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f g : M ⟶ N) : CategoryTheory.CategoryStruct.comp (actLeft A M.X) (f.hom + g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (f.hom + g.hom)) (actLeft A N.X)

A sum of module maps intertwines the actions.

theorem RS.neg_lin {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (actLeft A M.X) (-f.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (-f.hom)) (actLeft A N.X)

The negative of a module map intertwines the actions.

def RS.homAdd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f g : M ⟶ N) : M ⟶ N

The sum of two module maps.

Equations

• RS.homAdd f g = CategoryTheory.Mod.Hom.mk' (f.hom + g.hom) ⋯

def RS.homZero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} : M ⟶ N

The zero module map.

Equations

• RS.homZero = CategoryTheory.Mod.Hom.mk' 0 ⋯

def RS.homNeg {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : M ⟶ N

The negative of a module map.

Equations

• RS.homNeg f = CategoryTheory.Mod.Hom.mk' (-f.hom) ⋯

@[instance_reducible]

instance RS.instAddHomMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} : Add (M ⟶ N)

Equations

• RS.instAddHomMod = { add := RS.homAdd }

@[instance_reducible]

instance RS.instZeroHomMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} : Zero (M ⟶ N)

Equations

• RS.instZeroHomMod = { zero := RS.homZero }

@[instance_reducible]

instance RS.instNegHomMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} : Neg (M ⟶ N)

Equations

• RS.instNegHomMod = { neg := RS.homNeg }

@[instance_reducible]

instance RS.instAddCommGroupHomMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} : AddCommGroup (M ⟶ N)

The hom-groups of the category of modules.

Equations

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

@[instance_reducible]

instance RS.instPreadditiveMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] : CategoryTheory.Preadditive (CategoryTheory.Mod D A)

Modules over a monoid object are preadditive, with hom-groups the intertwining subgroups of the ambient hom-groups.

Equations

• RS.instPreadditiveMod = { homGroup := fun (x x_1 : CategoryTheory.Mod D A) => RS.instAddCommGroupHomMod, add_comp := ⋯, comp_add := ⋯ }

@[simp]

theorem RS.mod_add_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f g : M ⟶ N) : (f + g).hom = f.hom + g.hom

@[simp]

theorem RS.mod_zero_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} : CategoryTheory.Mod.Hom.hom 0 = 0

@[simp]

theorem RS.mod_neg_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : (-f).hom = -f.hom

instance RS.instForgetAdditive {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {A : D} [CategoryTheory.MonObj A] : (CategoryTheory.Mod.forget A).Additive

The forgetful functor is additive.

instance RS.instForgetFaithful {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A : D} [CategoryTheory.MonObj A] : (CategoryTheory.Mod.forget A).Faithful

The forgetful functor is faithful.

theorem RS.mono_of_mono_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) (h : CategoryTheory.Mono f.hom) : CategoryTheory.Mono f

A module map whose underlying morphism is a monomorphism is a monomorphism.

theorem RS.epi_of_epi_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A : D} [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) (h : CategoryTheory.Epi f.hom) : CategoryTheory.Epi f

A module map whose underlying morphism is an epimorphism is an epimorphism.

The zero module

@[implicit_reducible]

noncomputable def RS.zeroModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] (A : D) [CategoryTheory.MonObj A] : CategoryTheory.ModObj A 0

The zero object of D is a module, with the zero action.

Equations

• RS.zeroModObj A = { smul := 0, one_smul := ⋯, mul_smul := ⋯ }

noncomputable def RS.zeroMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] (A : D) [CategoryTheory.MonObj A] : CategoryTheory.Mod D A

The zero module.

Equations

• RS.zeroMod A = { X := 0, mod := RS.zeroModObj A }

theorem RS.isZero_zeroMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasZeroObject D] (A : D) [CategoryTheory.MonObj A] : CategoryTheory.Limits.IsZero (zeroMod A)

The zero module is a zero object.

instance RS.instHasZeroObjectMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasZeroObject D] (A : D) [CategoryTheory.MonObj A] : CategoryTheory.Limits.HasZeroObject (CategoryTheory.Mod D A)

Modules over a monoid object have a zero object.

Binary biproducts

noncomputable def RS.modBinaryBicone {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.Limits.BinaryBicone M N

The binary bicone carried by the biproduct of two modules.

Equations

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

theorem RS.modBinaryBicone_total {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modBinaryBicone A M N).fst (modBinaryBicone A M N).inl + CategoryTheory.CategoryStruct.comp (modBinaryBicone A M N).snd (modBinaryBicone A M N).inr = CategoryTheory.CategoryStruct.id (modBinaryBicone A M N).pt

The bicone of the module biproduct is total.

noncomputable def RS.modBinaryBiconeIsBilimit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : (modBinaryBicone A M N).IsBilimit

The bicone of the module biproduct is a bilimit.

Equations

• RS.modBinaryBiconeIsBilimit A M N = CategoryTheory.Limits.isBinaryBilimitOfTotal (RS.modBinaryBicone A M N) ⋯

instance RS.instHasBinaryBiproductsMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] : CategoryTheory.Limits.HasBinaryBiproducts (CategoryTheory.Mod D A)

Modules over a monoid object have binary biproducts.

Finite biproducts

noncomputable def RS.modBiproductAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (A : D) [CategoryTheory.MonObj A] {K : Type} [Fintype K] (M : K → CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (⨁ fun (j : K) => (M j).X) ⟶ ⨁ fun (j : K) => (M j).X

The componentwise action on a finite biproduct of carriers.

Equations

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

@[simp]

theorem RS.modBiproductAct_π {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (A : D) [CategoryTheory.MonObj A] {K : Type} [Fintype K] (M : K → CategoryTheory.Mod D A) (j : K) : CategoryTheory.CategoryStruct.comp (modBiproductAct A M) (CategoryTheory.Limits.biproduct.π (fun (j : K) => (M j).X) j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.Limits.biproduct.π (fun (j : K) => (M j).X) j)) (actLeft A (M j).X)

@[simp]

theorem RS.modBiproductAct_π_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (A : D) [CategoryTheory.MonObj A] {K : Type} [Fintype K] (M : K → CategoryTheory.Mod D A) (j : K) {Z : D} (h : (M j).X ⟶ Z) : CategoryTheory.CategoryStruct.comp (modBiproductAct A M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (j : K) => (M j).X) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.Limits.biproduct.π (fun (j : K) => (M j).X) j)) (CategoryTheory.CategoryStruct.comp (actLeft A (M j).X) h)

theorem RS.modBiproductAct_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (A : D) [CategoryTheory.MonObj A] {K : Type} [Fintype K] (M : K → CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (⨁ fun (j : K) => (M j).X)) (modBiproductAct A M) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (⨁ fun (j : K) => (M j).X)).hom

Unitality of the componentwise action.

theorem RS.modBiproductAct_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (A : D) [CategoryTheory.MonObj A] {K : Type} [Fintype K] (M : K → CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (⨁ fun (j : K) => (M j).X)) (modBiproductAct A M) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (⨁ fun (j : K) => (M j).X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modBiproductAct A M)) (modBiproductAct A M))

Associativity of the componentwise action.

@[implicit_reducible]

noncomputable def RS.modBiproductModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (A : D) [CategoryTheory.MonObj A] {K : Type} [Fintype K] (M : K → CategoryTheory.Mod D A) : CategoryTheory.ModObj A (⨁ fun (j : K) => (M j).X)

The module structure on a finite biproduct of carriers.

Equations

• RS.modBiproductModObj A M = { smul := RS.modBiproductAct A M, one_smul := ⋯, mul_smul := ⋯ }

noncomputable def RS.modBiproduct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (A : D) [CategoryTheory.MonObj A] {K : Type} [Fintype K] (M : K → CategoryTheory.Mod D A) : CategoryTheory.Mod D A

The finite biproduct of modules, bundled.

Equations

• RS.modBiproduct A M = { X := ⨁ fun (j : K) => (M j).X, mod := RS.modBiproductModObj A M }

noncomputable def RS.modBiproductπ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (A : D) [CategoryTheory.MonObj A] {K : Type} [Fintype K] (M : K → CategoryTheory.Mod D A) (j : K) : modBiproduct A M ⟶ M j

The projections of the biproduct are module maps.

Equations

• RS.modBiproductπ A M j = CategoryTheory.Mod.Hom.mk' (CategoryTheory.Limits.biproduct.π (fun (j : K) => (M j).X) j) ⋯

theorem RS.modBiproductAct_ι {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (A : D) [CategoryTheory.MonObj A] {K : Type} [Fintype K] (M : K → CategoryTheory.Mod D A) (j : K) : CategoryTheory.CategoryStruct.comp (actLeft A (M j).X) (CategoryTheory.Limits.biproduct.ι (fun (j : K) => (M j).X) j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.Limits.biproduct.ι (fun (j : K) => (M j).X) j)) (modBiproductAct A M)

The injections intertwine the actions.

noncomputable def RS.modBiproductInj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (A : D) [CategoryTheory.MonObj A] {K : Type} [Fintype K] (M : K → CategoryTheory.Mod D A) (j : K) : M j ⟶ modBiproduct A M

The injections of the biproduct are module maps.

Equations

• RS.modBiproductInj A M j = CategoryTheory.Mod.Hom.mk' (CategoryTheory.Limits.biproduct.ι (fun (j : K) => (M j).X) j) ⋯

noncomputable def RS.modBicone {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (A : D) [CategoryTheory.MonObj A] {K : Type} [Fintype K] (M : K → CategoryTheory.Mod D A) : CategoryTheory.Limits.Bicone M

The bicone carried by the finite biproduct of modules.

Equations

• RS.modBicone A M = { pt := RS.modBiproduct A M, π := RS.modBiproductπ A M, ι := RS.modBiproductInj A M, ι_π := ⋯ }

def RS.modHomAddHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (A : D) [CategoryTheory.MonObj A] (P Q : CategoryTheory.Mod D A) : (P ⟶ Q) →+ (P.X ⟶ Q.X)

Taking the underlying morphism of a module map is additive.

Equations

• RS.modHomAddHom A P Q = { toFun := fun (f : P ⟶ Q) => f.hom, map_zero' := ⋯, map_add' := ⋯ }

theorem RS.modBicone_total {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (A : D) [CategoryTheory.MonObj A] {K : Type} [Fintype K] (M : K → CategoryTheory.Mod D A) : ∑ j : K, CategoryTheory.CategoryStruct.comp ((modBicone A M).π j) ((modBicone A M).ι j) = CategoryTheory.CategoryStruct.id (modBicone A M).pt

The bicone of the finite biproduct of modules is total.

instance RS.instHasFiniteBiproductsMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (A : D) [CategoryTheory.MonObj A] : CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Mod D A)

Modules over a monoid object have finite biproducts, computed in the ambient category.

Finite products

instance RS.instHasFiniteProductsMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteProducts D] (A : D) [CategoryTheory.MonObj A] : CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Mod D A)

Modules over a monoid object have finite products.

Kernels

theorem RS.kerAct_aux {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.Limits.kernel.ι f.hom)) (actLeft A M.X)) f.hom = 0

The action carried by the kernel lands in the kernel.

noncomputable def RS.kerAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (CategoryTheory.Limits.kernel f.hom) ⟶ CategoryTheory.Limits.kernel f.hom

The action on the kernel of the underlying morphism.

Equations

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

@[simp]

theorem RS.kerAct_ι {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (kerAct A f) (CategoryTheory.Limits.kernel.ι f.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.Limits.kernel.ι f.hom)) (actLeft A M.X)

@[simp]

theorem RS.kerAct_ι_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) {Z : D} (h : M.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (kerAct A f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f.hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.Limits.kernel.ι f.hom)) (CategoryTheory.CategoryStruct.comp (actLeft A M.X) h)

theorem RS.kerAct_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (CategoryTheory.Limits.kernel f.hom)) (kerAct A f) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.Limits.kernel f.hom)).hom

Unitality of the action on the kernel.

theorem RS.kerAct_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.Limits.kernel f.hom)) (kerAct A f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (CategoryTheory.Limits.kernel f.hom)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (kerAct A f)) (kerAct A f))

Associativity of the action on the kernel.

@[implicit_reducible]

noncomputable def RS.kerModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.ModObj A (CategoryTheory.Limits.kernel f.hom)

The module structure on the kernel of the underlying morphism.

Equations

• RS.kerModObj A f = { smul := RS.kerAct A f, one_smul := ⋯, mul_smul := ⋯ }

noncomputable def RS.kerMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.Mod D A

The kernel of a module map, bundled.

Equations

• RS.kerMod A f = { X := CategoryTheory.Limits.kernel f.hom, mod := RS.kerModObj A f }

noncomputable def RS.kerIncl {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : kerMod A f ⟶ M

The inclusion of the kernel of a module map.

Equations

• RS.kerIncl A f = CategoryTheory.Mod.Hom.mk' (CategoryTheory.Limits.kernel.ι f.hom) ⋯

@[simp]

theorem RS.kerIncl_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : (kerIncl A f).hom = CategoryTheory.Limits.kernel.ι f.hom

theorem RS.kerIncl_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (kerIncl A f) f = 0

The inclusion of the kernel is annihilated by the map.

theorem RS.mono_kerIncl {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.Mono (kerIncl A f)

The inclusion of the kernel is a monomorphism.

noncomputable def RS.kerLift {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) {W : CategoryTheory.Mod D A} (k : W ⟶ M) (hk : CategoryTheory.CategoryStruct.comp k f = 0) : W ⟶ kerMod A f

The lift of a module map annihilated by f through the inclusion of the kernel.

Equations

• RS.kerLift A f k hk = CategoryTheory.Mod.Hom.mk' (CategoryTheory.Limits.kernel.lift f.hom k.hom ⋯) ⋯

theorem RS.kerLift_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) {W : CategoryTheory.Mod D A} (k : W ⟶ M) (hk : CategoryTheory.CategoryStruct.comp k f = 0) : CategoryTheory.CategoryStruct.comp (kerLift A f k hk) (kerIncl A f) = k

The lift through the kernel recovers the given map.

noncomputable def RS.kernelForkMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.Limits.KernelFork f

The kernel fork of a module map.

Equations

• RS.kernelForkMod A f = CategoryTheory.Limits.KernelFork.ofι (RS.kerIncl A f) ⋯

noncomputable def RS.kernelForkModIsLimit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.Limits.IsLimit (kernelForkMod A f)

The kernel fork of a module map is limiting.

Equations

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

instance RS.instHasKernelsMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasKernels D] (A : D) [CategoryTheory.MonObj A] : CategoryTheory.Limits.HasKernels (CategoryTheory.Mod D A)

Modules over a monoid object have kernels, computed in the ambient category.

Cokernels

theorem RS.epi_whiskerLeft_cokernelπ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (Z : D) {X Y : D} (g : X ⟶ Y) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.cokernel.π g))

Whiskering a cokernel projection leaves an epimorphism.

noncomputable def RS.whiskerCokernelDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (Z : D) {X Y W : D} (g : X ⟶ Y) (k : CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y ⟶ W) (hk : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) k = 0) : CategoryTheory.MonoidalCategoryStruct.tensorObj Z (CategoryTheory.Limits.cokernel g) ⟶ W

Descent along a whiskered cokernel projection.

Equations

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

@[simp]

theorem RS.whiskerCokernel_π_desc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (Z : D) {X Y W : D} (g : X ⟶ Y) (k : CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y ⟶ W) (hk : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) k = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.cokernel.π g)) (whiskerCokernelDesc Z g k hk) = k

@[simp]

theorem RS.whiskerCokernel_π_desc_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (Z : D) {X Y W : D} (g : X ⟶ Y) (k : CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y ⟶ W) (hk : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) k = 0) {Z✝ : D} (h : W ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.cokernel.π g)) (CategoryTheory.CategoryStruct.comp (whiskerCokernelDesc Z g k hk) h) = CategoryTheory.CategoryStruct.comp k h

theorem RS.cokerAct_aux {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCokernels D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f.hom) (CategoryTheory.CategoryStruct.comp (actLeft A N.X) (CategoryTheory.Limits.cokernel.π f.hom)) = 0

The descended action is well defined.

noncomputable def RS.cokerAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (CategoryTheory.Limits.cokernel f.hom) ⟶ CategoryTheory.Limits.cokernel f.hom

The action on the cokernel of the underlying morphism.

Equations

• RS.cokerAct A f = RS.whiskerCokernelDesc A f.hom (CategoryTheory.CategoryStruct.comp (RS.actLeft A N.X) (CategoryTheory.Limits.cokernel.π f.hom)) ⋯

@[simp]

theorem RS.π_cokerAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.Limits.cokernel.π f.hom)) (cokerAct A f) = CategoryTheory.CategoryStruct.comp (actLeft A N.X) (CategoryTheory.Limits.cokernel.π f.hom)

@[simp]

theorem RS.π_cokerAct_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) {Z : D} (h : CategoryTheory.Limits.cokernel f.hom ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.Limits.cokernel.π f.hom)) (CategoryTheory.CategoryStruct.comp (cokerAct A f) h) = CategoryTheory.CategoryStruct.comp (actLeft A N.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f.hom) h)

theorem RS.cokerAct_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (CategoryTheory.Limits.cokernel f.hom)) (cokerAct A f) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.Limits.cokernel f.hom)).hom

Unitality of the action on the cokernel.

theorem RS.cokerAct_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.Limits.cokernel f.hom)) (cokerAct A f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (CategoryTheory.Limits.cokernel f.hom)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (cokerAct A f)) (cokerAct A f))

Associativity of the action on the cokernel.

@[implicit_reducible]

noncomputable def RS.cokerModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.ModObj A (CategoryTheory.Limits.cokernel f.hom)

The module structure on the cokernel of the underlying morphism.

Equations

• RS.cokerModObj A f = { smul := RS.cokerAct A f, one_smul := ⋯, mul_smul := ⋯ }

noncomputable def RS.cokerMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.Mod D A

The cokernel of a module map, bundled.

Equations

• RS.cokerMod A f = { X := CategoryTheory.Limits.cokernel f.hom, mod := RS.cokerModObj A f }

noncomputable def RS.cokerProj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : N ⟶ cokerMod A f

The projection onto the cokernel of a module map.

Equations

• RS.cokerProj A f = CategoryTheory.Mod.Hom.mk' (CategoryTheory.Limits.cokernel.π f.hom) ⋯

@[simp]

theorem RS.cokerProj_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : (cokerProj A f).hom = CategoryTheory.Limits.cokernel.π f.hom

theorem RS.comp_cokerProj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp f (cokerProj A f) = 0

The projection onto the cokernel annihilates the map.

theorem RS.epi_cokerProj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.Epi (cokerProj A f)

The projection onto the cokernel is an epimorphism.

noncomputable def RS.cokerDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) {W : CategoryTheory.Mod D A} (k : N ⟶ W) (hk : CategoryTheory.CategoryStruct.comp f k = 0) : cokerMod A f ⟶ W

The descent of a module map annihilating f through the projection onto the cokernel.

Equations

• RS.cokerDesc A f k hk = CategoryTheory.Mod.Hom.mk' (CategoryTheory.Limits.cokernel.desc f.hom k.hom ⋯) ⋯

theorem RS.cokerProj_desc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) {W : CategoryTheory.Mod D A} (k : N ⟶ W) (hk : CategoryTheory.CategoryStruct.comp f k = 0) : CategoryTheory.CategoryStruct.comp (cokerProj A f) (cokerDesc A f k hk) = k

The descent through the cokernel recovers the given map.

noncomputable def RS.cokernelCoforkMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.Limits.CokernelCofork f

The cokernel cofork of a module map.

Equations

• RS.cokernelCoforkMod A f = CategoryTheory.Limits.CokernelCofork.ofπ (RS.cokerProj A f) ⋯

noncomputable def RS.cokernelCoforkModIsColimit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.Limits.IsColimit (cokernelCoforkMod A f)

The cokernel cofork of a module map is colimiting.

Equations

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

instance RS.instHasCokernelsMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCokernels D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] : CategoryTheory.Limits.HasCokernels (CategoryTheory.Mod D A)

Modules over a monoid object have cokernels, computed in the ambient category.

The monomorphism and epimorphism bridges

theorem RS.mono_iff_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.Mono f ↔ CategoryTheory.Mono f.hom

A module map is a monomorphism exactly when its underlying morphism is.

theorem RS.epi_whiskerLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (Z : D) {X Y : D} (e : X ⟶ Y) [CategoryTheory.Epi e] : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z e)

Whiskering preserves epimorphisms: an epimorphism of an abelian category is the cokernel of its kernel, and tensoring on the left preserves that cokernel.

theorem RS.epi_iff_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.Epi f ↔ CategoryTheory.Epi f.hom

A module map is an epimorphism exactly when its underlying morphism is.

Normality and abelianness

theorem RS.monoLift_aux {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) {W : CategoryTheory.Mod D A} (k : W ⟶ N) (hk : CategoryTheory.CategoryStruct.comp k (cokerProj A φ) = 0) : CategoryTheory.CategoryStruct.comp k.hom (CategoryTheory.Limits.cokernel.π φ.hom) = 0

A module map annihilated by the projection onto the cokernel is annihilated by the underlying cokernel projection.

noncomputable def RS.monoLiftHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Mono φ.hom] {W : CategoryTheory.Mod D A} (k : W ⟶ N) (hk : CategoryTheory.CategoryStruct.comp k (cokerProj A φ) = 0) : W.X ⟶ M.X

The underlying factorisation through a monomorphic module map.

Equations

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

theorem RS.monoLiftHom_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Mono φ.hom] {W : CategoryTheory.Mod D A} (k : W ⟶ N) (hk : CategoryTheory.CategoryStruct.comp k (cokerProj A φ) = 0) : CategoryTheory.CategoryStruct.comp (monoLiftHom A φ k hk) φ.hom = k.hom

theorem RS.monoLiftHom_comp_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Mono φ.hom] {W : CategoryTheory.Mod D A} (k : W ⟶ N) (hk : CategoryTheory.CategoryStruct.comp k (cokerProj A φ) = 0) {Z : D} (h : N.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (monoLiftHom A φ k hk) (CategoryTheory.CategoryStruct.comp φ.hom h) = CategoryTheory.CategoryStruct.comp k.hom h

theorem RS.monoLiftHom_lin {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Mono φ.hom] {W : CategoryTheory.Mod D A} (k : W ⟶ N) (hk : CategoryTheory.CategoryStruct.comp k (cokerProj A φ) = 0) : CategoryTheory.CategoryStruct.comp (actLeft A W.X) (monoLiftHom A φ k hk) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (monoLiftHom A φ k hk)) (actLeft A M.X)

The underlying factorisation intertwines the actions.

noncomputable def RS.monoLift {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Mono φ.hom] {W : CategoryTheory.Mod D A} (k : W ⟶ N) (hk : CategoryTheory.CategoryStruct.comp k (cokerProj A φ) = 0) : W ⟶ M

The factorisation through a monomorphism of a module map annihilated by the projection onto its cokernel.

Equations

• RS.monoLift A φ k hk = CategoryTheory.Mod.Hom.mk' (RS.monoLiftHom A φ k hk) ⋯

theorem RS.monoLift_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Mono φ.hom] {W : CategoryTheory.Mod D A} (k : W ⟶ N) (hk : CategoryTheory.CategoryStruct.comp k (cokerProj A φ) = 0) : CategoryTheory.CategoryStruct.comp (monoLift A φ k hk) φ = k

The factorisation through a monomorphism recovers the given map.

@[implicit_reducible]

noncomputable def RS.normalMonoOfMonoHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Mono φ.hom] : CategoryTheory.NormalMono φ

A module map with monomorphic underlying morphism is the kernel of its cokernel.

Equations

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

theorem RS.epiDesc_aux {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) {W : CategoryTheory.Mod D A} (k : M ⟶ W) (hk : CategoryTheory.CategoryStruct.comp (kerIncl A φ) k = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι φ.hom) k.hom = 0

A module map annihilating the inclusion of the kernel is annihilated by the underlying kernel inclusion.

noncomputable def RS.epiDescHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Epi φ.hom] {W : CategoryTheory.Mod D A} (k : M ⟶ W) (hk : CategoryTheory.CategoryStruct.comp (kerIncl A φ) k = 0) : N.X ⟶ W.X

The underlying factorisation through an epimorphic module map.

Equations

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

theorem RS.comp_epiDescHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Epi φ.hom] {W : CategoryTheory.Mod D A} (k : M ⟶ W) (hk : CategoryTheory.CategoryStruct.comp (kerIncl A φ) k = 0) : CategoryTheory.CategoryStruct.comp φ.hom (epiDescHom A φ k hk) = k.hom

The underlying factorisation recovers the given map.

theorem RS.comp_epiDescHom_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Epi φ.hom] {W : CategoryTheory.Mod D A} (k : M ⟶ W) (hk : CategoryTheory.CategoryStruct.comp (kerIncl A φ) k = 0) {Z : D} (h : W.X ⟶ Z) : CategoryTheory.CategoryStruct.comp φ.hom (CategoryTheory.CategoryStruct.comp (epiDescHom A φ k hk) h) = CategoryTheory.CategoryStruct.comp k.hom h

The underlying factorisation recovers the given map.

theorem RS.epiDescHom_lin {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Epi φ.hom] {W : CategoryTheory.Mod D A} (k : M ⟶ W) (hk : CategoryTheory.CategoryStruct.comp (kerIncl A φ) k = 0) : CategoryTheory.CategoryStruct.comp (actLeft A N.X) (epiDescHom A φ k hk) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (epiDescHom A φ k hk)) (actLeft A W.X)

The underlying factorisation intertwines the actions.

noncomputable def RS.epiDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Epi φ.hom] {W : CategoryTheory.Mod D A} (k : M ⟶ W) (hk : CategoryTheory.CategoryStruct.comp (kerIncl A φ) k = 0) : N ⟶ W

The factorisation through an epimorphism of a module map annihilating the inclusion of its kernel.

Equations

• RS.epiDesc A φ k hk = CategoryTheory.Mod.Hom.mk' (RS.epiDescHom A φ k hk) ⋯

theorem RS.comp_epiDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Epi φ.hom] {W : CategoryTheory.Mod D A} (k : M ⟶ W) (hk : CategoryTheory.CategoryStruct.comp (kerIncl A φ) k = 0) : CategoryTheory.CategoryStruct.comp φ (epiDesc A φ k hk) = k

The factorisation through an epimorphism recovers the given map.

@[implicit_reducible]

noncomputable def RS.normalEpiOfEpiHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (φ : M ⟶ N) [CategoryTheory.Epi φ.hom] : CategoryTheory.NormalEpi φ

A module map with epimorphic underlying morphism is the cokernel of its kernel.

Equations

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

instance RS.instIsNormalMonoCategoryMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] : CategoryTheory.IsNormalMonoCategory (CategoryTheory.Mod D A)

Every monomorphism of modules is a kernel.

instance RS.instIsNormalEpiCategoryMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] : CategoryTheory.IsNormalEpiCategory (CategoryTheory.Mod D A)

Every epimorphism of modules is a cokernel.

@[instance_reducible]

noncomputable instance RS.instAbelianMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] : CategoryTheory.Abelian (CategoryTheory.Mod D A)

Modules over a monoid object in an abelian monoidally preadditive category with right-exact tensor form an abelian category.

Equations

• RS.instAbelianMod A = { toPreadditive := RS.instPreadditiveMod, toIsNormalMonoCategory := ⋯, toIsNormalEpiCategory := ⋯, has_finite_products := ⋯, has_kernels := ⋯, has_cokernels := ⋯ }

instance RS.instForgetPreservesMono {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (A : D) [CategoryTheory.MonObj A] : (CategoryTheory.Mod.forget A).PreservesMonomorphisms

The forgetful functor preserves monomorphisms.

instance RS.instForgetReflectsMono {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (A : D) [CategoryTheory.MonObj A] : (CategoryTheory.Mod.forget A).ReflectsMonomorphisms

The forgetful functor reflects monomorphisms.

instance RS.instForgetPreservesEpi {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] : (CategoryTheory.Mod.forget A).PreservesEpimorphisms

The forgetful functor preserves epimorphisms.

instance RS.instForgetReflectsEpi {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] : (CategoryTheory.Mod.forget A).ReflectsEpimorphisms

The forgetful functor reflects epimorphisms.

Splitting off a retraction or a section

noncomputable def RS.retractionSection {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {K N : E} (k : K ⟶ N) (r : N ⟶ K) (hr : CategoryTheory.CategoryStruct.comp k r = CategoryTheory.CategoryStruct.id K) : CategoryTheory.Limits.cokernel k ⟶ N

The section of the cokernel projection determined by a retraction.

Equations

• RS.retractionSection k r hr = CategoryTheory.Limits.cokernel.desc k (CategoryTheory.CategoryStruct.id N - CategoryTheory.CategoryStruct.comp r k) ⋯

theorem RS.π_retractionSection {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {K N : E} (k : K ⟶ N) (r : N ⟶ K) (hr : CategoryTheory.CategoryStruct.comp k r = CategoryTheory.CategoryStruct.id K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π k) (retractionSection k r hr) = CategoryTheory.CategoryStruct.id N - CategoryTheory.CategoryStruct.comp r k

theorem RS.π_retractionSection_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {K N : E} (k : K ⟶ N) (r : N ⟶ K) (hr : CategoryTheory.CategoryStruct.comp k r = CategoryTheory.CategoryStruct.id K) {Z : E} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π k) (CategoryTheory.CategoryStruct.comp (retractionSection k r hr) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id N - CategoryTheory.CategoryStruct.comp r k) h

theorem RS.retractionSection_π {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {K N : E} (k : K ⟶ N) (r : N ⟶ K) (hr : CategoryTheory.CategoryStruct.comp k r = CategoryTheory.CategoryStruct.id K) : CategoryTheory.CategoryStruct.comp (retractionSection k r hr) (CategoryTheory.Limits.cokernel.π k) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.cokernel k)

The section is a section of the cokernel projection.

theorem RS.retractionSection_comp {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {K N : E} (k : K ⟶ N) (r : N ⟶ K) (hr : CategoryTheory.CategoryStruct.comp k r = CategoryTheory.CategoryStruct.id K) : CategoryTheory.CategoryStruct.comp (retractionSection k r hr) r = 0

The section is annihilated by the retraction.

noncomputable def RS.retractionBicone {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {K N : E} (k : K ⟶ N) (r : N ⟶ K) (hr : CategoryTheory.CategoryStruct.comp k r = CategoryTheory.CategoryStruct.id K) : CategoryTheory.Limits.BinaryBicone K (CategoryTheory.Limits.cokernel k)

The bicone exhibiting the ambient object as the biproduct of a split monomorphism and its cokernel.

Equations

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

theorem RS.retractionBicone_total {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {K N : E} (k : K ⟶ N) (r : N ⟶ K) (hr : CategoryTheory.CategoryStruct.comp k r = CategoryTheory.CategoryStruct.id K) : CategoryTheory.CategoryStruct.comp (retractionBicone k r hr).fst (retractionBicone k r hr).inl + CategoryTheory.CategoryStruct.comp (retractionBicone k r hr).snd (retractionBicone k r hr).inr = CategoryTheory.CategoryStruct.id (retractionBicone k r hr).pt

The bicone determined by a retraction is total.

noncomputable def RS.isoBiprodOfRetraction {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {K N : E} (k : K ⟶ N) (r : N ⟶ K) (hr : CategoryTheory.CategoryStruct.comp k r = CategoryTheory.CategoryStruct.id K) : N ≅ K ⊞ CategoryTheory.Limits.cokernel k

A retraction splits off the cokernel: if k : K ⟶ N has a retraction then N is the biproduct of K and the cokernel of k.

Equations

• RS.isoBiprodOfRetraction k r hr = CategoryTheory.Limits.biprod.uniqueUpToIso K (CategoryTheory.Limits.cokernel k) (CategoryTheory.Limits.isBinaryBilimitOfTotal (RS.retractionBicone k r hr) ⋯)

noncomputable def RS.sectionRetraction {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {C N : E} (c : N ⟶ C) (s : C ⟶ N) (hs : CategoryTheory.CategoryStruct.comp s c = CategoryTheory.CategoryStruct.id C) : N ⟶ CategoryTheory.Limits.kernel c

The retraction of the kernel inclusion determined by a section.

Equations

• RS.sectionRetraction c s hs = CategoryTheory.Limits.kernel.lift c (CategoryTheory.CategoryStruct.id N - CategoryTheory.CategoryStruct.comp c s) ⋯

theorem RS.sectionRetraction_ι {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {C N : E} (c : N ⟶ C) (s : C ⟶ N) (hs : CategoryTheory.CategoryStruct.comp s c = CategoryTheory.CategoryStruct.id C) : CategoryTheory.CategoryStruct.comp (sectionRetraction c s hs) (CategoryTheory.Limits.kernel.ι c) = CategoryTheory.CategoryStruct.id N - CategoryTheory.CategoryStruct.comp c s

theorem RS.sectionRetraction_ι_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {C N : E} (c : N ⟶ C) (s : C ⟶ N) (hs : CategoryTheory.CategoryStruct.comp s c = CategoryTheory.CategoryStruct.id C) {Z : E} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (sectionRetraction c s hs) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι c) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id N - CategoryTheory.CategoryStruct.comp c s) h

theorem RS.ι_sectionRetraction {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {C N : E} (c : N ⟶ C) (s : C ⟶ N) (hs : CategoryTheory.CategoryStruct.comp s c = CategoryTheory.CategoryStruct.id C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι c) (sectionRetraction c s hs) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.kernel c)

The retraction is a retraction of the kernel inclusion.

theorem RS.comp_sectionRetraction {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {C N : E} (c : N ⟶ C) (s : C ⟶ N) (hs : CategoryTheory.CategoryStruct.comp s c = CategoryTheory.CategoryStruct.id C) : CategoryTheory.CategoryStruct.comp s (sectionRetraction c s hs) = 0

The section is annihilated by the retraction.

noncomputable def RS.sectionBicone {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {C N : E} (c : N ⟶ C) (s : C ⟶ N) (hs : CategoryTheory.CategoryStruct.comp s c = CategoryTheory.CategoryStruct.id C) : CategoryTheory.Limits.BinaryBicone (CategoryTheory.Limits.kernel c) C

The bicone exhibiting the ambient object as the biproduct of the kernel of a split epimorphism and its target.

Equations

• RS.sectionBicone c s hs = { pt := N, fst := RS.sectionRetraction c s hs, snd := c, inl := CategoryTheory.Limits.kernel.ι c, inr := s, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := hs }

theorem RS.sectionBicone_total {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {C N : E} (c : N ⟶ C) (s : C ⟶ N) (hs : CategoryTheory.CategoryStruct.comp s c = CategoryTheory.CategoryStruct.id C) : CategoryTheory.CategoryStruct.comp (sectionBicone c s hs).fst (sectionBicone c s hs).inl + CategoryTheory.CategoryStruct.comp (sectionBicone c s hs).snd (sectionBicone c s hs).inr = CategoryTheory.CategoryStruct.id (sectionBicone c s hs).pt

The bicone determined by a section is total.

noncomputable def RS.isoBiprodOfSection {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {C N : E} (c : N ⟶ C) (s : C ⟶ N) (hs : CategoryTheory.CategoryStruct.comp s c = CategoryTheory.CategoryStruct.id C) : N ≅ CategoryTheory.Limits.kernel c ⊞ C

A section splits off the kernel: if c : N ⟶ C has a section then N is the biproduct of the kernel of c and C.

Equations

• RS.isoBiprodOfSection c s hs = CategoryTheory.Limits.biprod.uniqueUpToIso (CategoryTheory.Limits.kernel c) C (CategoryTheory.Limits.isBinaryBilimitOfTotal (RS.sectionBicone c s hs) ⋯)

Subobjects and quotients of a finite sum of simples

theorem RS.exists_subobject_of_mono_biprod {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {X T N : E} [CategoryTheory.Simple X] (f : N ⟶ X ⊞ T) [CategoryTheory.Mono f] : ∃ (C : E) (m : C ⟶ T), CategoryTheory.Mono m ∧ (Nonempty (N ≅ C) ∨ Nonempty (N ≅ X ⊞ C))

The inductive step for subobjects: a subobject of X ⊞ T with X simple is either a subobject of T, or the sum of X with one.

theorem RS.exists_quotient_of_epi_biprod {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {X T N : E} [CategoryTheory.Simple X] (f : X ⊞ T ⟶ N) [CategoryTheory.Epi f] : ∃ (C : E) (m : T ⟶ C), CategoryTheory.Epi m ∧ (Nonempty (N ≅ C) ∨ Nonempty (N ≅ X ⊞ C))

The inductive step for quotients: a quotient of X ⊞ T with X simple is either a quotient of T, or the sum of X with one.

noncomputable def RS.idxSum {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {J : Type w} (S : J → E) : List J → E

The direct sum of a list of indices, formed by iterated binary biproducts from a family of objects.

Equations

• RS.idxSum S [] = 0
• RS.idxSum S (i :: L) = (S i ⊞ RS.idxSum S L)

@[simp]

theorem RS.idxSum_nil {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {J : Type w} (S : J → E) : idxSum S [] = 0

@[simp]

theorem RS.idxSum_cons {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {J : Type w} (S : J → E) (i : J) (L : List J) : idxSum S (i :: L) = (S i ⊞ idxSum S L)

theorem RS.exists_sublist_iso_of_mono {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {J : Type w} (S : J → E) (L : List J) : (∀ j ∈ L, CategoryTheory.Simple (S j)) → ∀ {N : E} (f : N ⟶ idxSum S L), CategoryTheory.Mono f → ∃ (L' : List J), L'.Sublist L ∧ Nonempty (N ≅ idxSum S L')

A subobject of a finite direct sum of simple objects is the direct sum of a sublist of them.

theorem RS.exists_sublist_iso_of_epi {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {J : Type w} (S : J → E) (L : List J) : (∀ j ∈ L, CategoryTheory.Simple (S j)) → ∀ {N : E} (f : idxSum S L ⟶ N), CategoryTheory.Epi f → ∃ (L' : List J), L'.Sublist L ∧ Nonempty (N ≅ idxSum S L')

A quotient of a finite direct sum of simple objects is the direct sum of a sublist of them.

Sums of copies of two simple objects

noncomputable def RS.mixSum {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] (X Y : E) (p q : ℕ) : E

The direct sum of p copies of X and q copies of Y.

Equations

• RS.mixSum X Y p q = RS.idxSum id (List.replicate p X ++ List.replicate q Y)

theorem RS.simple_of_mem_mix {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] (X Y : E) [CategoryTheory.Simple X] [CategoryTheory.Simple Y] (p q : ℕ) (Z : E) : Z ∈ List.replicate p X ++ List.replicate q Y → CategoryTheory.Simple (id Z)

Every entry of a mixed replicate list is one of the two given objects.

theorem RS.exists_mixSum_iso_of_mono {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] (X Y : E) [CategoryTheory.Simple X] [CategoryTheory.Simple Y] (p q : ℕ) {N : E} (f : N ⟶ mixSum X Y p q) (hf : CategoryTheory.Mono f) : ∃ (p' : ℕ) (q' : ℕ), p' ≤ p ∧ q' ≤ q ∧ Nonempty (N ≅ mixSum X Y p' q')

A subobject of a sum of p copies of a simple object and q copies of another is a sum of p' ≤ p copies of the first and q' ≤ q copies of the second.

theorem RS.exists_mixSum_iso_of_epi {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] (X Y : E) [CategoryTheory.Simple X] [CategoryTheory.Simple Y] (p q : ℕ) {N : E} (f : mixSum X Y p q ⟶ N) (hf : CategoryTheory.Epi f) : ∃ (p' : ℕ) (q' : ℕ), p' ≤ p ∧ q' ≤ q ∧ Nonempty (N ≅ mixSum X Y p' q')

A quotient of a sum of p copies of a simple object and q copies of another is a sum of p' ≤ p copies of the first and q' ≤ q copies of the second.

Biproducts indexed by Fin n

noncomputable def RS.finSuccBicone {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {n : ℕ} (S : Fin (n + 1) → E) : CategoryTheory.Limits.BinaryBicone (S 0) (⨁ fun (i : Fin n) => S i.succ)

The bicone splitting off the zeroth summand of a biproduct indexed by Fin (n + 1).

Equations

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

noncomputable def RS.biproductFinSuccIso {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {n : ℕ} (S : Fin (n + 1) → E) : ⨁ S ≅ S 0 ⊞ ⨁ fun (i : Fin n) => S i.succ

A biproduct indexed by Fin (n + 1) splits off its zeroth summand.

Equations

• RS.biproductFinSuccIso S = CategoryTheory.Limits.biprod.uniqueUpToIso (S 0) (⨁ fun (i : Fin n) => S i.succ) (CategoryTheory.Limits.isBinaryBilimitOfTotal (RS.finSuccBicone S) ⋯)

theorem RS.idxSum_map {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {J K : Type w} (S : K → E) (g : J → K) (L : List J) : idxSum S (List.map g L) = idxSum (S ∘ g) L

Reindexing a list sum along a map of indices.

theorem RS.nonempty_biproduct_iso_idxSum {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] (n : ℕ) (S : Fin n → E) : Nonempty (⨁ S ≅ idxSum S (List.finRange n))

A biproduct indexed by Fin n is the sum over the list of its indices.

theorem RS.exists_sublist_iso_biproduct_of_mono {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.Abelian E] {n : ℕ} (S : Fin n → E) (hS : ∀ (i : Fin n), CategoryTheory.Simple (S i)) {N : E} (f : N ⟶ ⨁ S) (hf : CategoryTheory.Mono f) : ∃ (L : List (Fin n)), L.Sublist (List.finRange n) ∧ Nonempty (N ≅ idxSum S L)

A subobject of a finite biproduct of simple objects is the sum over a sublist of the indices.