Category instances for Mul, Add, Semigroup and AddSemigroup

We introduce the bundled categories:

• MagmaCat
• AddMagmaCat
• Semigrp
• AddSemigrp along with the relevant forgetful functors between them.

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

TODO

• Limits in these categories
• free/forgetful adjunctions

structure AddMagmaCat : Type (u + 1)

The category of additive magmas and additive magma morphisms.

• carrier : Type u

  The underlying additive magma.

• str : Add ↑self

structure MagmaCat : Type (u + 1)

The category of magmas and magma morphisms.

• carrier : Type u

  The underlying magma.

• str : Mul ↑self

instance MagmaCat.instCoeSortType : CoeSort MagmaCat (Type u)

Equations

• MagmaCat.instCoeSortType = { coe := MagmaCat.carrier }

instance AddMagmaCat.instCoeSortType : CoeSort AddMagmaCat (Type u)

Equations

• AddMagmaCat.instCoeSortType = { coe := AddMagmaCat.carrier }

@[reducible, inline]

abbrev MagmaCat.of (M : Type u) [Mul M] : MagmaCat

Construct a bundled MagmaCat from the underlying type and typeclass.

Equations

• MagmaCat.of M = MagmaCat.mk M

@[reducible, inline]

abbrev AddMagmaCat.of (M : Type u) [Add M] : AddMagmaCat

Construct a bundled AddMagmaCat from the underlying type and typeclass.

Equations

• AddMagmaCat.of M = AddMagmaCat.mk M

structure AddMagmaCat.Hom (A B : AddMagmaCat) : Type u

The type of morphisms in AddMagmaCat R.

• hom' : ↑A →ₙ+ ↑B

  The underlying AddHom.

theorem AddMagmaCat.Hom.ext {A B : AddMagmaCat} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

structure MagmaCat.Hom (A B : MagmaCat) : Type u

The type of morphisms in MagmaCat R.

• hom' : ↑A →ₙ* ↑B

  The underlying MulHom.

theorem MagmaCat.Hom.ext {A B : MagmaCat} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

instance MagmaCat.instCategory : CategoryTheory.Category.{u, u + 1} MagmaCat

Equations

• MagmaCat.instCategory = CategoryTheory.Category.mk @MagmaCat.instCategory.proof_1 @MagmaCat.instCategory.proof_2 @MagmaCat.instCategory.proof_3

instance AddMagmaCat.instCategory : CategoryTheory.Category.{u, u + 1} AddMagmaCat

Equations

• AddMagmaCat.instCategory = CategoryTheory.Category.mk @AddMagmaCat.instCategory.proof_1 @AddMagmaCat.instCategory.proof_2 @AddMagmaCat.instCategory.proof_3

instance MagmaCat.instConcreteCategoryMulHomCarrier : CategoryTheory.ConcreteCategory MagmaCat fun (x1 x2 : MagmaCat) => ↑x1 →ₙ* ↑x2

Equations

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

instance AddMagmaCat.instConcreteCategoryAddHomCarrier : CategoryTheory.ConcreteCategory AddMagmaCat fun (x1 x2 : AddMagmaCat) => ↑x1 →ₙ+ ↑x2

Equations

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

@[reducible, inline]

abbrev MagmaCat.Hom.hom {X Y : MagmaCat} (f : X.Hom Y) : ↑X →ₙ* ↑Y

Turn a morphism in MagmaCat back into a MulHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev AddMagmaCat.Hom.hom {X Y : AddMagmaCat} (f : X.Hom Y) : ↑X →ₙ+ ↑Y

Turn a morphism in AddMagmaCat back into an AddHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev MagmaCat.ofHom {X Y : Type u} [Mul X] [Mul Y] (f : X →ₙ* Y) : of X ⟶ of Y

Typecheck a MulHom as a morphism in MagmaCat.

Equations

• MagmaCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

@[reducible, inline]

abbrev AddMagmaCat.ofHom {X Y : Type u} [Add X] [Add Y] (f : X →ₙ+ Y) : of X ⟶ of Y

Typecheck an AddHom as a morphism in AddMagmaCat.

Equations

• AddMagmaCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def MagmaCat.Hom.Simps.hom (X Y : MagmaCat) (f : X.Hom Y) : ↑X →ₙ* ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• MagmaCat.Hom.Simps.hom X Y f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem MagmaCat.coe_id {X : MagmaCat} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem AddMagmaCat.coe_id {X : AddMagmaCat} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem MagmaCat.coe_comp {X Y Z : MagmaCat} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem AddMagmaCat.coe_comp {X Y Z : AddMagmaCat} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem MagmaCat.forget_map {X Y : MagmaCat} (f : X ⟶ Y) : (CategoryTheory.forget MagmaCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem AddMagmaCat.forget_map {X Y : AddMagmaCat} (f : X ⟶ Y) : (CategoryTheory.forget AddMagmaCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem AddMagmaCat.ext {X Y : AddMagmaCat} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem MagmaCat.ext {X Y : MagmaCat} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem MagmaCat.coe_of (M : Type u) [Mul M] : ↑(of M) = M

theorem AddMagmaCat.coe_of (M : Type u) [Add M] : ↑(of M) = M

@[simp]

theorem MagmaCat.hom_id {M : MagmaCat} : Hom.hom (CategoryTheory.CategoryStruct.id M) = MulHom.id ↑M

@[simp]

theorem AddMagmaCat.hom_id {M : AddMagmaCat} : Hom.hom (CategoryTheory.CategoryStruct.id M) = AddHom.id ↑M

theorem MagmaCat.id_apply (M : MagmaCat) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x

theorem AddMagmaCat.id_apply (M : AddMagmaCat) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x

@[simp]

theorem MagmaCat.hom_comp {M N T : MagmaCat} (f : M ⟶ N) (g : N ⟶ T) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

@[simp]

theorem AddMagmaCat.hom_comp {M N T : AddMagmaCat} (f : M ⟶ N) (g : N ⟶ T) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem MagmaCat.comp_apply {M N T : MagmaCat} (f : M ⟶ N) (g : N ⟶ T) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem AddMagmaCat.comp_apply {M N T : AddMagmaCat} (f : M ⟶ N) (g : N ⟶ T) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem AddMagmaCat.hom_ext {M N : AddMagmaCat} {f g : M ⟶ N} (hf : Hom.hom f = Hom.hom g) : f = g

theorem MagmaCat.hom_ext {M N : MagmaCat} {f g : M ⟶ N} (hf : Hom.hom f = Hom.hom g) : f = g

@[simp]

theorem MagmaCat.hom_ofHom {M N : Type u} [Mul M] [Mul N] (f : M →ₙ* N) : Hom.hom (ofHom f) = f

@[simp]

theorem AddMagmaCat.hom_ofHom {M N : Type u} [Add M] [Add N] (f : M →ₙ+ N) : Hom.hom (ofHom f) = f

@[simp]

theorem MagmaCat.ofHom_hom {M N : MagmaCat} (f : M ⟶ N) : ofHom (Hom.hom f) = f

@[simp]

theorem AddMagmaCat.ofHom_hom {M N : AddMagmaCat} (f : M ⟶ N) : ofHom (Hom.hom f) = f

@[simp]

theorem MagmaCat.ofHom_id {M : Type u} [Mul M] : ofHom (MulHom.id M) = CategoryTheory.CategoryStruct.id (of M)

@[simp]

theorem AddMagmaCat.ofHom_id {M : Type u} [Add M] : ofHom (AddHom.id M) = CategoryTheory.CategoryStruct.id (of M)

@[simp]

theorem MagmaCat.ofHom_comp {M N P : Type u} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : N →ₙ* P) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

@[simp]

theorem AddMagmaCat.ofHom_comp {M N P : Type u} [Add M] [Add N] [Add P] (f : M →ₙ+ N) (g : N →ₙ+ P) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem MagmaCat.ofHom_apply {X Y : Type u} [Mul X] [Mul Y] (f : X →ₙ* Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem AddMagmaCat.ofHom_apply {X Y : Type u} [Add X] [Add Y] (f : X →ₙ+ Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem MagmaCat.inv_hom_apply {M N : MagmaCat} (e : M ≅ N) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem AddMagmaCat.neg_hom_apply {M N : AddMagmaCat} (e : M ≅ N) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem MagmaCat.hom_inv_apply {M N : MagmaCat} (e : M ≅ N) (s : ↑N) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

theorem AddMagmaCat.hom_neg_apply {M N : AddMagmaCat} (e : M ≅ N) (s : ↑N) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

@[simp]

theorem MagmaCat.mulEquiv_coe_eq {X Y : Type u_1} [Mul X] [Mul Y] (e : X ≃* Y) : Hom.hom (ofHom ↑e) = ↑e

@[simp]

theorem AddMagmaCat.addEquiv_coe_eq {X Y : Type u_1} [Add X] [Add Y] (e : X ≃+ Y) : Hom.hom (ofHom ↑e) = ↑e

instance MagmaCat.instInhabited : Inhabited MagmaCat

Equations

• MagmaCat.instInhabited = { default := MagmaCat.of PEmpty.{?u.1 + 1} }

instance AddMagmaCat.instInhabited : Inhabited AddMagmaCat

Equations

• AddMagmaCat.instInhabited = { default := AddMagmaCat.of PEmpty.{?u.1 + 1} }

structure AddSemigrp : Type (u + 1)

The category of additive semigroups and semigroup morphisms.

• carrier : Type u

  The underlying type.

• str : AddSemigroup ↑self

structure Semigrp : Type (u + 1)

The category of semigroups and semigroup morphisms.

• carrier : Type u

  The underlying type.

• str : Semigroup ↑self

instance Semigrp.instCoeSortType : CoeSort Semigrp (Type u)

Equations

• Semigrp.instCoeSortType = { coe := Semigrp.carrier }

instance AddSemigrp.instCoeSortType : CoeSort AddSemigrp (Type u)

Equations

• AddSemigrp.instCoeSortType = { coe := AddSemigrp.carrier }

@[reducible, inline]

abbrev Semigrp.of (M : Type u) [Semigroup M] : Semigrp

Construct a bundled Semigrp from the underlying type and typeclass.

Equations

• Semigrp.of M = Semigrp.mk M

@[reducible, inline]

abbrev AddSemigrp.of (M : Type u) [AddSemigroup M] : AddSemigrp

Construct a bundled AddSemigrp from the underlying type and typeclass.

Equations

• AddSemigrp.of M = AddSemigrp.mk M

structure AddSemigrp.Hom (A B : AddSemigrp) : Type u

The type of morphisms in AddSemigrp R.

• hom' : ↑A →ₙ+ ↑B

  The underlying AddHom.

theorem AddSemigrp.Hom.ext {A B : AddSemigrp} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

structure Semigrp.Hom (A B : Semigrp) : Type u

The type of morphisms in Semigrp R.

• hom' : ↑A →ₙ* ↑B

  The underlying MulHom.

theorem Semigrp.Hom.ext {A B : Semigrp} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

instance Semigrp.instCategory : CategoryTheory.Category.{u, u + 1} Semigrp

Equations

• Semigrp.instCategory = CategoryTheory.Category.mk @Semigrp.instCategory.proof_1 @Semigrp.instCategory.proof_2 @Semigrp.instCategory.proof_3

instance AddSemigrp.instCategory : CategoryTheory.Category.{u, u + 1} AddSemigrp

Equations

• AddSemigrp.instCategory = CategoryTheory.Category.mk @AddSemigrp.instCategory.proof_1 @AddSemigrp.instCategory.proof_2 @AddSemigrp.instCategory.proof_3

instance Semigrp.instConcreteCategoryMulHomCarrier : CategoryTheory.ConcreteCategory Semigrp fun (x1 x2 : Semigrp) => ↑x1 →ₙ* ↑x2

Equations

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

instance AddSemigrp.instConcreteCategoryAddHomCarrier : CategoryTheory.ConcreteCategory AddSemigrp fun (x1 x2 : AddSemigrp) => ↑x1 →ₙ+ ↑x2

Equations

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

@[reducible, inline]

abbrev Semigrp.Hom.hom {X Y : Semigrp} (f : X.Hom Y) : ↑X →ₙ* ↑Y

Turn a morphism in Semigrp back into a MulHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev AddSemigrp.Hom.hom {X Y : AddSemigrp} (f : X.Hom Y) : ↑X →ₙ+ ↑Y

Turn a morphism in AddSemigrp back into an AddHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev Semigrp.ofHom {X Y : Type u} [Semigroup X] [Semigroup Y] (f : X →ₙ* Y) : of X ⟶ of Y

Typecheck a MulHom as a morphism in Semigrp.

Equations

• Semigrp.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

@[reducible, inline]

abbrev AddSemigrp.ofHom {X Y : Type u} [AddSemigroup X] [AddSemigroup Y] (f : X →ₙ+ Y) : of X ⟶ of Y

Typecheck an AddHom as a morphism in AddSemigrp.

Equations

• AddSemigrp.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def Semigrp.Hom.Simps.hom (X Y : Semigrp) (f : X.Hom Y) : ↑X →ₙ* ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• Semigrp.Hom.Simps.hom X Y f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem Semigrp.coe_id {X : Semigrp} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem AddSemigrp.coe_id {X : AddSemigrp} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem Semigrp.coe_comp {X Y Z : Semigrp} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem AddSemigrp.coe_comp {X Y Z : AddSemigrp} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[deprecated "Use hom_comp instead" (since := "2025-01-28")]

theorem Semigrp.comp_def {X Y Z : Semigrp} {f : X ⟶ Y} {g : Y ⟶ Z} : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

@[deprecated "Use hom_comp instead" (since := "2025-01-28")]

theorem AddSemigrp.comp_def {X Y Z : AddSemigrp} {f : X ⟶ Y} {g : Y ⟶ Z} : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

@[simp]

theorem Semigrp.forget_map {X Y : Semigrp} (f : X ⟶ Y) : (CategoryTheory.forget Semigrp).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem AddSemigrp.ext {X Y : AddSemigrp} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem Semigrp.ext {X Y : Semigrp} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem Semigrp.coe_of (R : Type u) [Semigroup R] : ↑(of R) = R

theorem AddSemigrp.coe_of (R : Type u) [AddSemigroup R] : ↑(of R) = R

@[simp]

theorem Semigrp.hom_id {X : Semigrp} : Hom.hom (CategoryTheory.CategoryStruct.id X) = MulHom.id ↑X

@[simp]

theorem AddSemigrp.hom_id {X : AddSemigrp} : Hom.hom (CategoryTheory.CategoryStruct.id X) = AddHom.id ↑X

theorem Semigrp.id_apply (X : Semigrp) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

theorem AddSemigrp.id_apply (X : AddSemigrp) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

@[simp]

theorem Semigrp.hom_comp {X Y T : Semigrp} (f : X ⟶ Y) (g : Y ⟶ T) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

@[simp]

theorem AddSemigrp.hom_comp {X Y T : AddSemigrp} (f : X ⟶ Y) (g : Y ⟶ T) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem Semigrp.comp_apply {X Y T : Semigrp} (f : X ⟶ Y) (g : Y ⟶ T) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem AddSemigrp.comp_apply {X Y T : AddSemigrp} (f : X ⟶ Y) (g : Y ⟶ T) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem AddSemigrp.hom_ext {X Y : AddSemigrp} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

theorem Semigrp.hom_ext {X Y : Semigrp} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

@[simp]

theorem Semigrp.hom_ofHom {X Y : Type u} [Semigroup X] [Semigroup Y] (f : X →ₙ* Y) : Hom.hom (ofHom f) = f

@[simp]

theorem AddSemigrp.hom_ofHom {X Y : Type u} [AddSemigroup X] [AddSemigroup Y] (f : X →ₙ+ Y) : Hom.hom (ofHom f) = f

@[simp]

theorem Semigrp.ofHom_hom {X Y : Semigrp} (f : X ⟶ Y) : ofHom (Hom.hom f) = f

@[simp]

theorem AddSemigrp.ofHom_hom {X Y : AddSemigrp} (f : X ⟶ Y) : ofHom (Hom.hom f) = f

@[simp]

theorem Semigrp.ofHom_id {X : Type u} [Semigroup X] : ofHom (MulHom.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem AddSemigrp.ofHom_id {X : Type u} [AddSemigroup X] : ofHom (AddHom.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem Semigrp.ofHom_comp {X Y Z : Type u} [Semigroup X] [Semigroup Y] [Semigroup Z] (f : X →ₙ* Y) (g : Y →ₙ* Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

@[simp]

theorem AddSemigrp.ofHom_comp {X Y Z : Type u} [AddSemigroup X] [AddSemigroup Y] [AddSemigroup Z] (f : X →ₙ+ Y) (g : Y →ₙ+ Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem Semigrp.ofHom_apply {X Y : Type u} [Semigroup X] [Semigroup Y] (f : X →ₙ* Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem AddSemigrp.ofHom_apply {X Y : Type u} [AddSemigroup X] [AddSemigroup Y] (f : X →ₙ+ Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem Semigrp.inv_hom_apply {X Y : Semigrp} (e : X ≅ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem AddSemigrp.neg_hom_apply {X Y : AddSemigrp} (e : X ≅ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem Semigrp.hom_inv_apply {X Y : Semigrp} (e : X ≅ Y) (s : ↑Y) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

theorem AddSemigrp.hom_neg_apply {X Y : AddSemigrp} (e : X ≅ Y) (s : ↑Y) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

@[simp]

theorem Semigrp.mulEquiv_coe_eq {X Y : Type u_1} [Semigroup X] [Semigroup Y] (e : X ≃* Y) : Hom.hom (ofHom ↑e) = ↑e

@[simp]

theorem AddSemigrp.addEquiv_coe_eq {X Y : Type u_1} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) : Hom.hom (ofHom ↑e) = ↑e

instance Semigrp.instInhabited : Inhabited Semigrp

Equations

• Semigrp.instInhabited = { default := Semigrp.of PEmpty.{?u.1 + 1} }

instance AddSemigrp.instInhabited : Inhabited AddSemigrp

Equations

• AddSemigrp.instInhabited = { default := AddSemigrp.of PEmpty.{?u.1 + 1} }

instance Semigrp.hasForgetToMagmaCat : CategoryTheory.HasForget₂ Semigrp MagmaCat

Equations

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

instance AddSemigrp.hasForgetToAddMagmaCat : CategoryTheory.HasForget₂ AddSemigrp AddMagmaCat

Equations

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

def MulEquiv.toMagmaCatIso {X Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) : MagmaCat.of X ≅ MagmaCat.of Y

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

Equations

• e.toMagmaCatIso = { hom := MagmaCat.ofHom e.toMulHom, inv := MagmaCat.ofHom e.symm.toMulHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def AddEquiv.toAddMagmaCatIso {X Y : Type u} [Add X] [Add Y] (e : X ≃+ Y) : AddMagmaCat.of X ≅ AddMagmaCat.of Y

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

Equations

• e.toAddMagmaCatIso = { hom := AddMagmaCat.ofHom e.toAddHom, inv := AddMagmaCat.ofHom e.symm.toAddHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem MulEquiv.toMagmaCatIso_hom {X Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) : e.toMagmaCatIso.hom = MagmaCat.ofHom e.toMulHom

@[simp]

theorem AddEquiv.toAddMagmaCatIso_inv {X Y : Type u} [Add X] [Add Y] (e : X ≃+ Y) : e.toAddMagmaCatIso.inv = AddMagmaCat.ofHom e.symm.toAddHom

@[simp]

theorem MulEquiv.toMagmaCatIso_inv {X Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) : e.toMagmaCatIso.inv = MagmaCat.ofHom e.symm.toMulHom

@[simp]

theorem AddEquiv.toAddMagmaCatIso_hom {X Y : Type u} [Add X] [Add Y] (e : X ≃+ Y) : e.toAddMagmaCatIso.hom = AddMagmaCat.ofHom e.toAddHom

def MulEquiv.toSemigrpIso {X Y : Type u} [Semigroup X] [Semigroup Y] (e : X ≃* Y) : Semigrp.of X ≅ Semigrp.of Y

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

Equations

• e.toSemigrpIso = { hom := Semigrp.ofHom e.toMulHom, inv := Semigrp.ofHom e.symm.toMulHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def AddEquiv.toAddSemigrpIso {X Y : Type u} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) : AddSemigrp.of X ≅ AddSemigrp.of Y

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

Equations

• e.toAddSemigrpIso = { hom := AddSemigrp.ofHom e.toAddHom, inv := AddSemigrp.ofHom e.symm.toAddHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem AddEquiv.toAddSemigrpIso_inv {X Y : Type u} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) : e.toAddSemigrpIso.inv = AddSemigrp.ofHom e.symm.toAddHom

@[simp]

theorem AddEquiv.toAddSemigrpIso_hom {X Y : Type u} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) : e.toAddSemigrpIso.hom = AddSemigrp.ofHom e.toAddHom

@[simp]

theorem MulEquiv.toSemigrpIso_inv {X Y : Type u} [Semigroup X] [Semigroup Y] (e : X ≃* Y) : e.toSemigrpIso.inv = Semigrp.ofHom e.symm.toMulHom

@[simp]

theorem MulEquiv.toSemigrpIso_hom {X Y : Type u} [Semigroup X] [Semigroup Y] (e : X ≃* Y) : e.toSemigrpIso.hom = Semigrp.ofHom e.toMulHom

def CategoryTheory.Iso.magmaCatIsoToMulEquiv {X Y : MagmaCat} (i : X ≅ Y) : ↑X ≃* ↑Y

Build a MulEquiv from an isomorphism in the category MagmaCat.

Equations

• i.magmaCatIsoToMulEquiv = (MagmaCat.Hom.hom i.hom).toMulEquiv (MagmaCat.Hom.hom i.inv) ⋯ ⋯

def CategoryTheory.Iso.addMagmaCatIsoToAddEquiv {X Y : AddMagmaCat} (i : X ≅ Y) : ↑X ≃+ ↑Y

Build an AddEquiv from an isomorphism in the category AddMagmaCat.

Equations

• i.addMagmaCatIsoToAddEquiv = (AddMagmaCat.Hom.hom i.hom).toAddEquiv (AddMagmaCat.Hom.hom i.inv) ⋯ ⋯

def CategoryTheory.Iso.semigrpIsoToMulEquiv {X Y : Semigrp} (i : X ≅ Y) : ↑X ≃* ↑Y

Build a MulEquiv from an isomorphism in the category Semigroup.

Equations

• i.semigrpIsoToMulEquiv = (Semigrp.Hom.hom i.hom).toMulEquiv (Semigrp.Hom.hom i.inv) ⋯ ⋯

def CategoryTheory.Iso.addSemigrpIsoToAddEquiv {X Y : AddSemigrp} (i : X ≅ Y) : ↑X ≃+ ↑Y

Build an AddEquiv from an isomorphism in the category AddSemigroup.

Equations

• i.addSemigrpIsoToAddEquiv = (AddSemigrp.Hom.hom i.hom).toAddEquiv (AddSemigrp.Hom.hom i.inv) ⋯ ⋯

def mulEquivIsoMagmaIso {X Y : Type u} [Mul X] [Mul Y] : X ≃* Y ≅ MagmaCat.of X ≅ MagmaCat.of Y

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

Equations

• mulEquivIsoMagmaIso = { hom := fun (e : X ≃* Y) => e.toMagmaCatIso, inv := fun (i : MagmaCat.of X ≅ MagmaCat.of Y) => i.magmaCatIsoToMulEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def addEquivIsoAddMagmaIso {X Y : Type u} [Add X] [Add Y] : X ≃+ Y ≅ AddMagmaCat.of X ≅ AddMagmaCat.of Y

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

Equations

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

def mulEquivIsoSemigrpIso {X Y : Type u} [Semigroup X] [Semigroup Y] : X ≃* Y ≅ Semigrp.of X ≅ Semigrp.of Y

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

Equations

• mulEquivIsoSemigrpIso = { hom := fun (e : X ≃* Y) => e.toSemigrpIso, inv := fun (i : Semigrp.of X ≅ Semigrp.of Y) => i.semigrpIsoToMulEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def addEquivIsoAddSemigrpIso {X Y : Type u} [AddSemigroup X] [AddSemigroup Y] : X ≃+ Y ≅ AddSemigrp.of X ≅ AddSemigrp.of Y

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

Equations

• addEquivIsoAddSemigrpIso = { hom := fun (e : X ≃+ Y) => e.toAddSemigrpIso, inv := fun (i : AddSemigrp.of X ≅ AddSemigrp.of Y) => i.addSemigrpIsoToAddEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

instance MagmaCat.forgetReflectsIsos : (CategoryTheory.forget MagmaCat).ReflectsIsomorphisms

instance AddMagmaCat.forgetReflectsIsos : (CategoryTheory.forget AddMagmaCat).ReflectsIsomorphisms

instance Semigrp.forgetReflectsIsos : (CategoryTheory.forget Semigrp).ReflectsIsomorphisms

instance AddSemigrp.forgetReflectsIsos : (CategoryTheory.forget AddSemigrp).ReflectsIsomorphisms

instance Semigrp.forget₂_full : (CategoryTheory.forget₂ Semigrp MagmaCat).Full

Ensure that forget₂ CommMonCat MonCat automatically reflects isomorphisms. We could have used CategoryTheory.HasForget.ReflectsIso alternatively.

instance AddSemigrp.forget₂_full : (CategoryTheory.forget₂ AddSemigrp AddMagmaCat).Full

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.