# Category instances for Monoid, AddMonoid, CommMonoid, and AddCommMmonoid. #

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.

Equations
Instances For
def MonCat :
Type (u + 1)

The category of monoids and monoid morphisms.

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

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

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

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

Equations
Instances For
theorem AddMonCat.bundledHom.proof_2 {α : Type u_1} (I : ) :
(fun {X Y : Type u_1} (x : ) (x_1 : ) (f : ) => f) I I ((fun {α : Type u_1} (x : ) => ) I) = id
theorem AddMonCat.bundledHom.proof_1 {α : Type u_1} {β : Type u_1} (Iα : ) (Iβ : ) ⦃a₁ : ⦃a₂ : (a : (fun {X Y : Type u_1} (x : ) (x_1 : ) (f : ) => f) a₁ = (fun {X Y : Type u_1} (x : ) (x_1 : ) (f : ) => f) a₂) :
a₁ = a₂
Equations
• One or more equations did not get rendered due to their size.
theorem AddMonCat.bundledHom.proof_3 {α : Type u_1} {β : Type u_1} {γ : Type u_1} (Iα : ) (Iβ : ) (Iγ : ) (f : ) (g : ) :
g f = g f
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
• X.instMonoidα = X.str
instance MonCat.instMonoidα (X : MonCat) :
Monoid X
Equations
• X.instMonoidα = X.str
CoeFun (X Y) fun (x : X Y) => XY
Equations
• AddMonCat.instCoeFunHomForallαAddMonoid = { coe := fun (f : X →+ Y) => f }
instance MonCat.instCoeFunHomForallαMonoid {X : MonCat} {Y : MonCat} :
CoeFun (X Y) fun (x : X Y) => XY
Equations
• MonCat.instCoeFunHomForallαMonoid = { coe := fun (f : X →* Y) => f }
FunLike (X Y) X Y
Equations
instance MonCat.instFunLike (X : MonCat) (Y : MonCat) :
FunLike (X Y) X Y
Equations
Equations
• =
instance MonCat.instMonoidHomClass (X : MonCat) (Y : MonCat) :
MonoidHomClass (X Y) X Y
Equations
• =
@[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]
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.

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

Construct a bundled MonCat from the underlying type and typeclass.

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

Typecheck an AddMonoidHom as a morphism in AddMonCat.

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

Typecheck a MonoidHom as a morphism in MonCat.

Equations
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
Zero (X Y)
Equations
• X.instZeroHom Y = { zero := }
instance MonCat.instOneHom (X : MonCat) (Y : MonCat) :
One (X Y)
Equations
• X.instOneHom Y = { one := }
@[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
Equations
instance MonCat.instGroupαMonoidOf {G : Type u_1} [] :
Group ()
Equations
• MonCat.instGroupαMonoidOf = inst
Type (u + 1)

The category of additive commutative monoids and monoid morphisms.

Equations
Instances For
def CommMonCat :
Type (u + 1)

The category of commutative monoids and monoid morphisms.

Equations
Instances For
Equations
Equations
Equations
• X.instCommMonoidα = X.str
Equations
• X.instCommMonoidα = X.str
CoeFun (X Y) fun (x : X Y) => XY
Equations
• AddCommMonCat.instCoeFunHomForallαAddCommMonoid = { coe := fun (f : X →+ Y) => f }
instance CommMonCat.instCoeFunHomForallαCommMonoid {X : CommMonCat} {Y : CommMonCat} :
CoeFun (X Y) fun (x : X Y) => XY
Equations
• CommMonCat.instCoeFunHomForallαCommMonoid = { coe := fun (f : X →* Y) => f }
FunLike (X Y) X Y
Equations
• X.instFunLike Y = let_fun this := inferInstance; this
instance CommMonCat.instFunLike (X : CommMonCat) (Y : CommMonCat) :
FunLike (X Y) X Y
Equations
• X.instFunLike Y = let_fun this := inferInstance; this
@[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) :
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 AddCommMonCat from the underlying type and typeclass.

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

Construct a bundled CommMonCat from the underlying type and typeclass.

Equations
Instances For
Equations
Equations
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.

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

Typecheck a MonoidHom as a morphism in CommMonCat.

Equations
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) :
theorem AddEquiv.toAddMonCatIso.proof_1 {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.

Equations
Instances For
@[simp]
theorem MulEquiv.toMonCatIso_inv {X : Type u} {Y : Type u} [] [] (e : X ≃* Y) :
e.toMonCatIso.inv = MonCat.ofHom e.symm.toMonoidHom
@[simp]
theorem AddEquiv.toAddMonCatIso_hom {X : Type u} {Y : Type u} [] [] (e : X ≃+ Y) :
@[simp]
theorem MulEquiv.toMonCatIso_hom {X : Type u} {Y : Type u} [] [] (e : X ≃* Y) :
e.toMonCatIso.hom = MonCat.ofHom e.toMonoidHom
@[simp]
theorem AddEquiv.toAddMonCatIso_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.

Equations
• e.toMonCatIso = { hom := MonCat.ofHom e.toMonoidHom, inv := MonCat.ofHom e.symm.toMonoidHom, hom_inv_id := , inv_hom_id := }
Instances For
def AddEquiv.toAddCommMonCatIso {X : Type u} {Y : Type u} [] [] (e : X ≃+ Y) :

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

Equations
Instances For
theorem AddEquiv.toAddCommMonCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+ Y) :
theorem AddEquiv.toAddCommMonCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+ Y) :
@[simp]
theorem MulEquiv.toCommMonCatIso_hom {X : Type u} {Y : Type u} [] [] (e : X ≃* Y) :
e.toCommMonCatIso.hom = CommMonCat.ofHom e.toMonoidHom
@[simp]
theorem MulEquiv.toCommMonCatIso_inv {X : Type u} {Y : Type u} [] [] (e : X ≃* Y) :
e.toCommMonCatIso.inv = CommMonCat.ofHom e.symm.toMonoidHom
@[simp]
theorem AddEquiv.toAddCommMonCatIso_inv {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.

Equations
Instances For

Build an AddEquiv from an isomorphism in the category AddMonCat.

Equations
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.

Equations
Instances For

Build an AddEquiv from an isomorphism in the category AddCommMonCat.

Equations
Instances For

Build a MulEquiv from an isomorphism in the category CommMonCat.

Equations
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

Equations
• addEquivIsoAddMonCatIso = { hom := fun (e : X ≃+ Y) => e.toAddMonCatIso, inv := fun (i : ) => i.addMonCatIsoToAddEquiv, hom_inv_id := , inv_hom_id := }
Instances For
theorem addEquivIsoAddMonCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [] [] :
theorem addEquivIsoAddMonCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [] [] :
def mulEquivIsoMonCatIso {X : Type u} {Y : Type u} [] [] :
X ≃* Y

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

Equations
• mulEquivIsoMonCatIso = { hom := fun (e : X ≃* Y) => e.toMonCatIso, inv := fun (i : ) => i.monCatIsoToMulEquiv, hom_inv_id := , inv_hom_id := }
Instances For
theorem addEquivIsoAddCommMonCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [] [] :
(CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddCommMonCatIso) fun (i : ) => i.commMonCatIsoToAddEquiv) = CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddCommMonCatIso) fun (i : ) => i.commMonCatIsoToAddEquiv
theorem addEquivIsoAddCommMonCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [] [] :
(CategoryTheory.CategoryStruct.comp (fun (i : ) => i.commMonCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddCommMonCatIso) = CategoryTheory.CategoryStruct.comp (fun (i : ) => i.commMonCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddCommMonCatIso
def addEquivIsoAddCommMonCatIso {X : Type u} {Y : Type u} [] [] :
X ≃+ Y

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

Equations
• One or more equations did not get rendered due to their size.
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

Equations
• One or more equations did not get rendered due to their size.
Instances For
.ReflectsIsomorphisms
Equations
instance MonCat.forget_reflects_isos :
.ReflectsIsomorphisms
Equations
.ReflectsIsomorphisms
Equations
instance CommMonCat.forget_reflects_isos :
.ReflectsIsomorphisms
Equations

@[simp] lemmas for MonoidHom.comp and categorical identities.

@[simp]
theorem AddMonoidHom.comp_id_monCat {G : AddMonCat} {H : Type u} [] (f : G →+ H) :
f.comp = f
@[simp]
theorem MonoidHom.comp_id_monCat {G : MonCat} {H : Type u} [] (f : G →* H) :
f.comp = f
@[simp]
theorem AddMonoidHom.id_monCat_comp {G : Type u} [] {H : AddMonCat} (f : G →+ H) :
@[simp]
theorem MonoidHom.id_monCat_comp {G : Type u} [] {H : MonCat} (f : G →* H) :
@[simp]
theorem AddMonoidHom.comp_id_commMonCat {G : AddCommMonCat} {H : Type u} [] (f : G →+ H) :
f.comp = f
@[simp]
theorem MonoidHom.comp_id_commMonCat {G : CommMonCat} {H : Type u} [] (f : G →* H) :
f.comp = f
@[simp]
theorem AddMonoidHom.id_commMonCat_comp {G : Type u} [] {H : AddCommMonCat} (f : G →+ H) :
@[simp]
theorem MonoidHom.id_commMonCat_comp {G : Type u} [] {H : CommMonCat} (f : G →* H) :