# Documentation

Mathlib.Algebra.Category.SemigroupCat.Basic

# Category instances for Mul, Add, Semigroup and AddSemigroup#

We introduce the bundled categories:

• MagmaCat
• AddMagmaCat
• SemigroupCat
• AddSemigroupCat along with the relevant forgetful functors between them.

This closely follows Mathlib.Algebra.Category.MonCat.Basic.

## TODO #

• Limits in these categories
Type (u + 1)

Instances For
def MagmaCat :
Type (u + 1)

The category of magmas and magma morphisms.

Instances For
theorem AddMagmaCat.bundledHom.proof_3 {α : Type u_1} {β : Type u_1} {γ : Type u_1} (Iα : Add α) (Iβ : Add β) (Iγ : Add γ) (f : AddHom α β) (g : AddHom β γ) :
g f = g f
().toFun = id
∀ {α β : Type u_1} ( : Add α) ( : Add β), Function.Injective fun f => f
Instances For
instance MagmaCat.instMulHomClass (X : MagmaCat) (Y : MagmaCat) :
MulHomClass (X Y) X Y

Construct a bundled AddMagmaCat from the underlying type and typeclass.

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

Construct a bundled MagmaCat from the underlying type and typeclass.

Instances For
@[simp]
↑() = R
@[simp]
theorem MagmaCat.coe_of (R : Type u) [Mul R] :
↑() = R
@[simp]
e = e
@[simp]
theorem MagmaCat.mulEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [Mul X] [Mul Y] (e : X ≃* Y) :
e = e

Typecheck an AddHom as a morphism in AddMagmaCat.

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

Typecheck a MulHom as a morphism in MagmaCat.

Instances For
theorem AddMagmaCat.ofHom_apply {X : Type u} {Y : Type u} [Add X] [Add Y] (f : AddHom X Y) (x : X) :
↑() x = f x
theorem MagmaCat.ofHom_apply {X : Type u} {Y : Type u} [Mul X] [Mul Y] (f : X →ₙ* Y) (x : X) :
↑() x = f x
Type (u + 1)

The category of additive semigroups and semigroup morphisms.

Instances For
def SemigroupCat :
Type (u + 1)

The category of semigroups and semigroup morphisms.

Instances For
Instances For
Instances For

Construct a bundled AddSemigroupCat from the underlying type and typeclass.

Instances For

Construct a bundled SemigroupCat from the underlying type and typeclass.

Instances For
@[simp]
theorem AddSemigroupCat.coe_of (R : Type u) [] :
↑() = R
@[simp]
theorem SemigroupCat.coe_of (R : Type u) [] :
↑() = R
@[simp]
theorem AddSemigroupCat.addEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+ Y) :
e = e
@[simp]
theorem SemigroupCat.mulEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃* Y) :
e = e
def AddSemigroupCat.ofHom {X : Type u} {Y : Type u} [] [] (f : AddHom X Y) :

Typecheck an AddHom as a morphism in AddSemigroupCat.

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

Typecheck a MulHom as a morphism in SemigroupCat.

Instances For
theorem AddSemigroupCat.ofHom_apply {X : Type u} {Y : Type u} [] [] (f : AddHom X Y) (x : X) :
↑() x = f x
theorem SemigroupCat.ofHom_apply {X : Type u} {Y : Type u} [] [] (f : X →ₙ* Y) (x : X) :
↑() x = f x

Build an isomorphism in the category AddMagmaCat from an AddEquiv between Adds.

Instances For
@[simp]
theorem MulEquiv.toMagmaCatIso_inv_apply {X : Type u} {Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) :
∀ (a : Y), ().inv a = Equiv.toFun ().toEquiv a
@[simp]
theorem MulEquiv.toMagmaCatIso_hom_apply {X : Type u} {Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) :
∀ (a : X), ().hom a = Equiv.toFun e.toEquiv a
@[simp]
∀ (a : Y), ().inv a = Equiv.toFun ().toEquiv a
@[simp]
∀ (a : X), ().hom a = Equiv.toFun e.toEquiv a
def MulEquiv.toMagmaCatIso {X : Type u} {Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) :

Build an isomorphism in the category MagmaCat from a MulEquiv between Muls.

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

Build an isomorphism in the category AddSemigroup from an AddEquiv between AddSemigroups.

Instances For
theorem AddEquiv.toAddSemigroupCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+ Y) :
@[simp]
theorem MulEquiv.toSemigroupCatIso_inv_apply {X : Type u} {Y : Type u} [] [] (e : X ≃* Y) :
∀ (a : Y), ().inv a = Equiv.toFun ().toEquiv a
@[simp]
theorem AddEquiv.toAddSemigroupCatIso_inv_apply {X : Type u} {Y : Type u} [] [] (e : X ≃+ Y) :
∀ (a : Y), ().inv a = Equiv.toFun ().toEquiv a
@[simp]
theorem MulEquiv.toSemigroupCatIso_hom_apply {X : Type u} {Y : Type u} [] [] (e : X ≃* Y) :
∀ (a : X), ().hom a = Equiv.toFun e.toEquiv a
@[simp]
theorem AddEquiv.toAddSemigroupCatIso_hom_apply {X : Type u} {Y : Type u} [] [] (e : X ≃+ Y) :
∀ (a : X), ().hom a = Equiv.toFun e.toEquiv a
def MulEquiv.toSemigroupCatIso {X : Type u} {Y : Type u} [] [] (e : X ≃* Y) :

Build an isomorphism in the category Semigroup from a MulEquiv between Semigroups.

Instances For

Build an AddEquiv from an isomorphism in the category AddMagma.

Instances For

Build a MulEquiv from an isomorphism in the category Magma.

Instances For

Build an AddEquiv from an isomorphism in the category AddSemigroup.

Instances For

Build a MulEquiv from an isomorphism in the category Semigroup.

Instances For
X ≃+ Y

additive equivalences between Adds are the same as (isomorphic to) isomorphisms in AddMagma

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

multiplicative equivalences between Muls are the same as (isomorphic to) isomorphisms in Magma

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

additive equivalences between AddSemigroups are the same as (isomorphic to) isomorphisms in AddSemigroup

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

multiplicative equivalences between Semigroups are the same as (isomorphic to) isomorphisms in Semigroup

Instances For
Once we've shown that the forgetful functors to type reflect isomorphisms, we automatically obtain that the forget₂ functors between our concrete categories reflect isomorphisms.