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

def MagmaCat : Type (u + 1)

The category of magmas and magma morphisms.

Equations

• MagmaCat = CategoryTheory.Bundled Mul

def AddMagmaCat : Type (u + 1)

The category of additive magmas and additive magma morphisms.

Equations

• AddMagmaCat = CategoryTheory.Bundled Add

instance MagmaCat.bundledHom : CategoryTheory.BundledHom MulHom

Equations

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

instance AddMagmaCat.bundledHom : CategoryTheory.BundledHom AddHom

Equations

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

instance instMagmaCatLargeCategory : CategoryTheory.LargeCategory MagmaCat

Equations

• instMagmaCatLargeCategory = CategoryTheory.BundledHom.category MulHom

instance MagmaCat.instConcreteCategory : CategoryTheory.ConcreteCategory MagmaCat

Equations

• MagmaCat.instConcreteCategory = CategoryTheory.BundledHom.concreteCategory MulHom

instance instAddMagmaCatLargeCategory : CategoryTheory.LargeCategory AddMagmaCat

Equations

• instAddMagmaCatLargeCategory = CategoryTheory.BundledHom.category AddHom

instance AddMagmaCat.instConcreteCategory : CategoryTheory.ConcreteCategory AddMagmaCat

Equations

• AddMagmaCat.instConcreteCategory = CategoryTheory.BundledHom.concreteCategory AddHom

instance MagmaCat.instCoeSortType : CoeSort MagmaCat (Type u_1)

Equations

• MagmaCat.instCoeSortType = { coe := fun (X : MagmaCat) => ↑X }

instance AddMagmaCat.instCoeSortType : CoeSort AddMagmaCat (Type u_1)

Equations

• AddMagmaCat.instCoeSortType = { coe := fun (X : AddMagmaCat) => ↑X }

def MagmaCat.forget_obj_eq_coe (R : MagmaCat) : Prop

Equations

• R.forget_obj_eq_coe = ((CategoryTheory.forget MagmaCat).obj R = ↑R)

def AddMagmaCat.forget_obj_eq_coe (R : AddMagmaCat) : Prop

Equations

• R.forget_obj_eq_coe = ((CategoryTheory.forget AddMagmaCat).obj R = ↑R)

instance MagmaCat.instMulα (X : MagmaCat) : Mul ↑X

Equations

• X.instMulα = X.str

instance AddMagmaCat.instMulα (X : AddMagmaCat) : Add ↑X

Equations

• X.instMulα = X.str

instance MagmaCat.instFunLike (X : MagmaCat) (Y : MagmaCat) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• X.instFunLike Y = inferInstanceAs (FunLike (↑X →ₙ* ↑Y) ↑X ↑Y)

instance AddMagmaCat.instFunLike (X : AddMagmaCat) (Y : AddMagmaCat) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• X.instFunLike Y = inferInstanceAs (FunLike (AddHom ↑X ↑Y) ↑X ↑Y)

instance MagmaCat.instMulHomClass (X : MagmaCat) (Y : MagmaCat) : MulHomClass (X ⟶ Y) ↑X ↑Y

Equations

• ⋯ = ⋯

instance AddMagmaCat.instAddHomClass (X : AddMagmaCat) (Y : AddMagmaCat) : AddHomClass (X ⟶ Y) ↑X ↑Y

Equations

• ⋯ = ⋯

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

Construct a bundled MagmaCat from the underlying type and typeclass.

Equations

• MagmaCat.of M = CategoryTheory.Bundled.of M

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

Construct a bundled AddMagmaCat from the underlying type and typeclass.

Equations

• AddMagmaCat.of M = CategoryTheory.Bundled.of M

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Typecheck a MulHom as a morphism in MagmaCat.

Equations

• MagmaCat.ofHom f = f

def AddMagmaCat.ofHom {X : Type u} {Y : Type u} [Add X] [Add Y] (f : AddHom X Y) : AddMagmaCat.of X ⟶ AddMagmaCat.of Y

Typecheck an AddHom as a morphism in AddMagmaCat.

Equations

• AddMagmaCat.ofHom f = f

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

theorem AddMagmaCat.ofHom_apply {X : Type u} {Y : Type u} [Add X] [Add Y] (f : AddHom X Y) (x : X) : (AddMagmaCat.ofHom f) x = f x

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} }

def Semigrp : Type (u + 1)

The category of semigroups and semigroup morphisms.

Equations

• Semigrp = CategoryTheory.Bundled Semigroup

def AddSemigrp : Type (u + 1)

The category of additive semigroups and semigroup morphisms.

Equations

• AddSemigrp = CategoryTheory.Bundled AddSemigroup

instance Semigrp.instParentProjectionMulSemigroupToMul : CategoryTheory.BundledHom.ParentProjection @Semigroup.toMul

Equations

• Semigrp.instParentProjectionMulSemigroupToMul = ⋯

instance AddSemigrp.instParentProjectionAddAddSemigroupToAdd : CategoryTheory.BundledHom.ParentProjection @AddSemigroup.toAdd

Equations

• AddSemigrp.instParentProjectionAddAddSemigroupToAdd = ⋯

instance instSemigrpLargeCategory : CategoryTheory.LargeCategory Semigrp

Equations

• instSemigrpLargeCategory = CategoryTheory.BundledHom.category (CategoryTheory.BundledHom.MapHom MulHom @Semigroup.toMul)

instance Semigrp.instConcreteCategory : CategoryTheory.ConcreteCategory Semigrp

Equations

• Semigrp.instConcreteCategory = CategoryTheory.BundledHom.concreteCategory fun (x x_1 : Type ?u.3) => CategoryTheory.BundledHom.MapHom MulHom @Semigroup.toMul

instance AddSemigrp.instConcreteCategory : CategoryTheory.ConcreteCategory AddSemigrp

Equations

• AddSemigrp.instConcreteCategory = CategoryTheory.BundledHom.concreteCategory fun (x x_1 : Type ?u.3) => CategoryTheory.BundledHom.MapHom AddHom @AddSemigroup.toAdd

instance instAddSemigrpLargeCategory : CategoryTheory.LargeCategory AddSemigrp

Equations

• instAddSemigrpLargeCategory = CategoryTheory.BundledHom.category (CategoryTheory.BundledHom.MapHom AddHom @AddSemigroup.toAdd)

instance Semigrp.instCoeSortType : CoeSort Semigrp (Type u_1)

Equations

• Semigrp.instCoeSortType = { coe := fun (X : Semigrp) => ↑X }

instance AddSemigrp.instCoeSortType : CoeSort AddSemigrp (Type u_1)

Equations

• AddSemigrp.instCoeSortType = { coe := fun (X : AddSemigrp) => ↑X }

def Semigrp.forget_obj_eq_coe (R : Semigrp) : Prop

Equations

• R.forget_obj_eq_coe = ((CategoryTheory.forget Semigrp).obj R = ↑R)

def AddSemigrp.forget_obj_eq_coe (R : AddSemigrp) : Prop

Equations

• R.forget_obj_eq_coe = ((CategoryTheory.forget AddSemigrp).obj R = ↑R)

instance Semigrp.instSemigroupα (X : Semigrp) : Semigroup ↑X

Equations

• X.instSemigroupα = X.str

instance AddSemigrp.instSemigroupα (X : AddSemigrp) : AddSemigroup ↑X

Equations

• X.instSemigroupα = X.str

instance Semigrp.instFunLike (X : Semigrp) (Y : Semigrp) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• X.instFunLike Y = inferInstanceAs (FunLike (↑X →ₙ* ↑Y) ↑X ↑Y)

instance AddSemigrp.instFunLike (X : AddSemigrp) (Y : AddSemigrp) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• X.instFunLike Y = inferInstanceAs (FunLike (AddHom ↑X ↑Y) ↑X ↑Y)

instance Semigrp.instMulHomClass (X : Semigrp) (Y : Semigrp) : MulHomClass (X ⟶ Y) ↑X ↑Y

Equations

• ⋯ = ⋯

instance AddSemigrp.instAddHomClass (X : AddSemigrp) (Y : AddSemigrp) : AddHomClass (X ⟶ Y) ↑X ↑Y

Equations

• ⋯ = ⋯

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

Construct a bundled Semigrp from the underlying type and typeclass.

Equations

• Semigrp.of M = CategoryTheory.Bundled.of M

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

Construct a bundled AddSemigrp from the underlying type and typeclass.

Equations

• AddSemigrp.of M = CategoryTheory.Bundled.of M

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Typecheck a MulHom as a morphism in Semigrp.

Equations

• Semigrp.ofHom f = f

def AddSemigrp.ofHom {X : Type u} {Y : Type u} [AddSemigroup X] [AddSemigroup Y] (f : AddHom X Y) : AddSemigrp.of X ⟶ AddSemigrp.of Y

Typecheck an AddHom as a morphism in AddSemigrp.

Equations

• AddSemigrp.ofHom f = f

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

theorem AddSemigrp.ofHom_apply {X : Type u} {Y : Type u} [AddSemigroup X] [AddSemigroup Y] (f : AddHom X Y) (x : X) : (AddSemigrp.ofHom f) x = f x

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

• Semigrp.hasForgetToMagmaCat = CategoryTheory.BundledHom.forget₂ MulHom @Semigroup.toMul

instance AddSemigrp.hasForgetToAddMagmaCat : CategoryTheory.HasForget₂ AddSemigrp AddMagmaCat

Equations

• AddSemigrp.hasForgetToAddMagmaCat = CategoryTheory.BundledHom.forget₂ AddHom @AddSemigroup.toAdd

def MulEquiv.toMagmaCatIso {X : Type u} {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 := e.toMulHom, inv := e.symm.toMulHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def AddEquiv.toAddMagmaCatIso {X : Type u} {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 := e.toAddHom, inv := e.symm.toAddHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem AddEquiv.toAddMagmaCatIso_inv_apply {X : Type u} {Y : Type u} [Add X] [Add Y] (e : X ≃+ Y) : ∀ (a : Y), e.toAddMagmaCatIso.inv a = e.symm.toFun a

@[simp]

theorem AddEquiv.toAddMagmaCatIso_hom_apply {X : Type u} {Y : Type u} [Add X] [Add Y] (e : X ≃+ Y) : ∀ (a : X), e.toAddMagmaCatIso.hom a = e.toFun a

@[simp]

theorem MulEquiv.toMagmaCatIso_hom_apply {X : Type u} {Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) : ∀ (a : X), e.toMagmaCatIso.hom a = e.toFun a

@[simp]

theorem MulEquiv.toMagmaCatIso_inv_apply {X : Type u} {Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) : ∀ (a : Y), e.toMagmaCatIso.inv a = e.symm.toFun a

def MulEquiv.toSemigrpIso {X : Type u} {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 := e.toMulHom, inv := e.symm.toMulHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def AddEquiv.toAddSemigrpIso {X : Type u} {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 := e.toAddHom, inv := e.symm.toAddHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem MulEquiv.toSemigrpIso_inv_apply {X : Type u} {Y : Type u} [Semigroup X] [Semigroup Y] (e : X ≃* Y) : ∀ (a : Y), e.toSemigrpIso.inv a = e.symm.toFun a

@[simp]

theorem AddEquiv.toAddSemigrpIso_hom_apply {X : Type u} {Y : Type u} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) : ∀ (a : X), e.toAddSemigrpIso.hom a = e.toFun a

@[simp]

theorem MulEquiv.toSemigrpIso_hom_apply {X : Type u} {Y : Type u} [Semigroup X] [Semigroup Y] (e : X ≃* Y) : ∀ (a : X), e.toSemigrpIso.hom a = e.toFun a

@[simp]

theorem AddEquiv.toAddSemigrpIso_inv_apply {X : Type u} {Y : Type u} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) : ∀ (a : Y), e.toAddSemigrpIso.inv a = e.symm.toFun a

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

Build a MulEquiv from an isomorphism in the category MagmaCat.

Equations

• i.magmaCatIsoToMulEquiv = MulHom.toMulEquiv i.hom i.inv ⋯ ⋯

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

Build an AddEquiv from an isomorphism in the category AddMagmaCat.

Equations

• i.addMagmaCatIsoToAddEquiv = AddHom.toAddEquiv i.hom i.inv ⋯ ⋯

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

Build a MulEquiv from an isomorphism in the category Semigroup.

Equations

• i.semigrpIsoToMulEquiv = MulHom.toMulEquiv i.hom i.inv ⋯ ⋯

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

Build an AddEquiv from an isomorphism in the category AddSemigroup.

Equations

• i.addSemigrpIsoToAddEquiv = AddHom.toAddEquiv i.hom i.inv ⋯ ⋯

def mulEquivIsoMagmaIso {X : Type u} {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 : Type u} {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 : Type u} {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 : Type u} {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

Equations

• MagmaCat.forgetReflectsIsos = ⋯

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

Equations

• AddMagmaCat.forgetReflectsIsos = ⋯

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

Equations

• Semigrp.forgetReflectsIsos = ⋯

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

Equations

• AddSemigrp.forgetReflectsIsos = ⋯

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

Equations

• Semigrp.forget₂_full = ⋯

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

Equations

• AddSemigrp.forget₂_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.