# Documentation

Mathlib.Algebra.Category.MonCat.Basic

We introduce the bundled categories:

• MonCat
• AddMonCat
• CommMonCat
• AddCommMonCat along with the relevant forgetful functors between them.
Type (u + 1)

The category of additive monoids and monoid morphisms.

Instances For
def MonCat :
Type (u + 1)

The category of monoids and monoid morphisms.

Instances For
abbrev AddMonCat.AssocAddMonoidHom (M : Type u_1) (N : Type u_2) [] [] :
Type (max u_2 u_1)

AddMonoidHom doesn't actually assume associativity. This alias is needed to make the category theory machinery work.

Instances For
@[inline, reducible]
abbrev MonCat.AssocMonoidHom (M : Type u_1) (N : Type u_2) [] [] :
Type (max u_2 u_1)

MonoidHom doesn't actually assume associativity. This alias is needed to make the category theory machinery work.

Instances For
theorem AddMonCat.bundledHom.proof_2 {α : Type u_1} (I : ) :
(fun {X Y} x x_1 f => f) I I ((fun {α} x => ) I) = id
theorem AddMonCat.bundledHom.proof_3 {α : Type u_1} {β : Type u_1} {γ : Type u_1} (Iα : ) (Iβ : ) (Iγ : ) (f : ) (g : ) :
g f = g f
theorem AddMonCat.bundledHom.proof_1 {α : Type u_1} {β : Type u_1} (Iα : ) (Iβ : ) ⦃a₁ : ⦃a₂ : (a : (fun {X Y} x x_1 f => f) a₁ = (fun {X Y} x x_1 f => f) a₂) :
a₁ = a₂
FunLike (X Y) X fun x => Y
instance MonCat.Hom_FunLike (X : MonCat) (Y : MonCat) :
FunLike (X Y) X fun x => Y
@[simp]
@[simp]
theorem MonCat.coe_id {X : MonCat} :
@[simp]
= g f
@[simp]
theorem MonCat.coe_comp {X : MonCat} {Y : MonCat} {Z : MonCat} {f : X Y} {g : Y Z} :
= g f
@[simp]
().map f = f
@[simp]
theorem MonCat.forget_map {X : MonCat} {Y : MonCat} (f : X Y) :
().map f = f
theorem AddMonCat.ext {X : AddMonCat} {Y : AddMonCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
f = g
theorem MonCat.ext {X : MonCat} {Y : MonCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
f = g
def AddMonCat.of (M : Type u) [] :

Construct a bundled AddMonCat from the underlying type and typeclass.

Instances For
def MonCat.of (M : Type u) [] :

Construct a bundled MonCat from the underlying type and typeclass.

Instances For
theorem AddMonCat.coe_of (R : Type u) [] :
↑() = R
theorem MonCat.coe_of (R : Type u) [] :
↑() = R
def AddMonCat.ofHom {X : Type u} {Y : Type u} [] [] (f : X →+ Y) :

Typecheck an AddMonoidHom as a morphism in AddMonCat.

Instances For
def MonCat.ofHom {X : Type u} {Y : Type u} [] [] (f : X →* Y) :

Typecheck a MonoidHom as a morphism in MonCat.

Instances For
@[simp]
theorem AddMonCat.ofHom_apply {X : Type u} {Y : Type u} [] [] (f : X →+ Y) (x : X) :
↑() x = f x
@[simp]
theorem MonCat.ofHom_apply {X : Type u} {Y : Type u} [] [] (f : X →* Y) (x : X) :
↑() x = f x
@[simp]
0 x = 0
@[simp]
theorem MonCat.oneHom_apply (X : MonCat) (Y : MonCat) (x : X) :
1 x = 1
@[simp]
theorem AddMonCat.zero_of {A : Type u_1} [] :
0 = 0
@[simp]
theorem MonCat.one_of {A : Type u_1} [] :
1 = 1
@[simp]
theorem AddMonCat.add_of {A : Type u_1} [] (a : A) (b : A) :
a + b = a + b
@[simp]
theorem MonCat.mul_of {A : Type u_1} [] (a : A) (b : A) :
a * b = a * b
Type (u + 1)

The category of additive commutative monoids and monoid morphisms.

Instances For
def CommMonCat :
Type (u + 1)

The category of commutative monoids and monoid morphisms.

Instances For
FunLike (X Y) X fun x => Y
instance CommMonCat.Hom_FunLike (X : CommMonCat) (Y : CommMonCat) :
FunLike (X Y) X fun x => Y
@[simp]
@[simp]
= g f
@[simp]
theorem CommMonCat.coe_comp {X : CommMonCat} {Y : CommMonCat} {Z : CommMonCat} {f : X Y} {g : Y Z} :
= g f
@[simp]
= f
@[simp]
theorem CommMonCat.forget_map {X : CommMonCat} {Y : CommMonCat} (f : X Y) :
().map f = f
theorem AddCommMonCat.ext {X : AddCommMonCat} {Y : AddCommMonCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
f = g
theorem CommMonCat.ext {X : CommMonCat} {Y : CommMonCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
f = g

Construct a bundled AddCommMon from the underlying type and typeclass.

Instances For
def CommMonCat.of (M : Type u) [] :

Construct a bundled CommMonCat from the underlying type and typeclass.

Instances For
theorem AddCommMonCat.coe_of (R : Type u) [] :
↑() = R
theorem CommMonCat.coe_of (R : Type u) [] :
↑() = R
def AddCommMonCat.ofHom {X : Type u} {Y : Type u} [] [] (f : X →+ Y) :

Typecheck an AddMonoidHom as a morphism in AddCommMonCat.

Instances For
def CommMonCat.ofHom {X : Type u} {Y : Type u} [] [] (f : X →* Y) :

Typecheck a MonoidHom as a morphism in CommMonCat.

Instances For
@[simp]
theorem AddCommMonCat.ofHom_apply {X : Type u} {Y : Type u} [] [] (f : X →+ Y) (x : X) :
↑() x = f x
@[simp]
theorem CommMonCat.ofHom_apply {X : Type u} {Y : Type u} [] [] (f : X →* Y) (x : X) :
↑() x = f x
theorem AddEquiv.toAddMonCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+ Y) :
def AddEquiv.toAddMonCatIso {X : Type u} {Y : Type u} [] [] (e : X ≃+ Y) :

Build an isomorphism in the category AddMonCat from an AddEquiv between AddMonoids.

Instances For
theorem AddEquiv.toAddMonCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+ Y) :
@[simp]
theorem MulEquiv.toMonCatIso_hom {X : Type u} {Y : Type u} [] [] (e : X ≃* Y) :
@[simp]
theorem AddEquiv.toAddMonCatIso_inv {X : Type u} {Y : Type u} [] [] (e : X ≃+ Y) :
@[simp]
theorem AddEquiv.toAddMonCatIso_hom {X : Type u} {Y : Type u} [] [] (e : X ≃+ Y) :
@[simp]
theorem MulEquiv.toMonCatIso_inv {X : Type u} {Y : Type u} [] [] (e : X ≃* Y) :
def MulEquiv.toMonCatIso {X : Type u} {Y : Type u} [] [] (e : X ≃* Y) :

Build an isomorphism in the category MonCat from a MulEquiv between Monoids.

Instances For
theorem AddEquiv.toAddCommMonCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+ Y) :
def AddEquiv.toAddCommMonCatIso {X : Type u} {Y : Type u} [] [] (e : X ≃+ Y) :

Build an isomorphism in the category AddCommMonCat from an AddEquiv between AddCommMonoids.

Instances For
theorem AddEquiv.toAddCommMonCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+ Y) :
@[simp]
theorem MulEquiv.toCommMonCatIso_inv {X : Type u} {Y : Type u} [] [] (e : X ≃* Y) :
@[simp]
theorem AddEquiv.toAddCommMonCatIso_inv {X : Type u} {Y : Type u} [] [] (e : X ≃+ Y) :
@[simp]
theorem MulEquiv.toCommMonCatIso_hom {X : Type u} {Y : Type u} [] [] (e : X ≃* Y) :
@[simp]
theorem AddEquiv.toAddCommMonCatIso_hom {X : Type u} {Y : Type u} [] [] (e : X ≃+ Y) :
def MulEquiv.toCommMonCatIso {X : Type u} {Y : Type u} [] [] (e : X ≃* Y) :

Build an isomorphism in the category CommMonCat from a MulEquiv between CommMonoids.

Instances For

Build an AddEquiv from an isomorphism in the category AddMonCat.

Instances For
def CategoryTheory.Iso.monCatIsoToMulEquiv {X : MonCat} {Y : MonCat} (i : X Y) :
X ≃* Y

Build a MulEquiv from an isomorphism in the category MonCat.

Instances For

Build an AddEquiv from an isomorphism in the category AddCommMonCat.

Instances For

Build a MulEquiv from an isomorphism in the category CommMonCat.

Instances For
def addEquivIsoAddMonCatIso {X : Type u} {Y : Type u} [] [] :
X ≃+ Y

additive equivalences between AddMonoids are the same as (isomorphic to) isomorphisms in AddMonCat

Instances For
def mulEquivIsoMonCatIso {X : Type u} {Y : Type u} [] [] :
X ≃* Y

multiplicative equivalences between Monoids are the same as (isomorphic to) isomorphisms in MonCat

Instances For
def addEquivIsoAddCommMonCatIso {X : Type u} {Y : Type u} [] [] :
X ≃+ Y

additive equivalences between AddCommMonoids are the same as (isomorphic to) isomorphisms in AddCommMonCat

Instances For
def mulEquivIsoCommMonCatIso {X : Type u} {Y : Type u} [] [] :
X ≃* Y

multiplicative equivalences between CommMonoids are the same as (isomorphic to) isomorphisms in CommMonCat

Instances For