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
• free/forgetful adjunctions

def AddMagmaCat : Type (u + 1)

The category of additive magmas and additive magma morphisms.

Equations

• AddMagmaCat = CategoryTheory.Bundled Add

def MagmaCat : Type (u + 1)

The category of magmas and magma morphisms.

Equations

• MagmaCat = CategoryTheory.Bundled Mul

theorem AddMagmaCat.bundledHom.proof_1 : ∀ {α β : Type u_1} (Iα : Add α) (Iβ : Add β), Function.Injective fun (f : AddHom α β) => ⇑f

theorem AddMagmaCat.bundledHom.proof_2 {α : Type u_1} (I : Add α) : (AddHom.id α).toFun = id

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

instance AddMagmaCat.bundledHom : CategoryTheory.BundledHom AddHom

Equations

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

instance MagmaCat.bundledHom : CategoryTheory.BundledHom MulHom

Equations

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

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 AddMagmaCat.instCoeSortType : CoeSort AddMagmaCat (Type u_1)

Equations

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

instance MagmaCat.instCoeSortType : CoeSort MagmaCat (Type u_1)

Equations

• MagmaCat.instCoeSortType = { coe := fun (X : MagmaCat) => ↑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 AddMagmaCat.instMulα (X : AddMagmaCat) : Add ↑X

Equations

• X.instMulα = X.str

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

Equations

• X.instMulα = X.str

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.instFunLike (X : MagmaCat) (Y : MagmaCat) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem AddMagmaCat.addEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [Add X] [Add Y] (e : X ≃+ Y) : ⇑↑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

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

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

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

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

instance AddMagmaCat.instInhabited : Inhabited AddMagmaCat

Equations

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

instance MagmaCat.instInhabited : Inhabited MagmaCat

Equations

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

def AddSemigroupCat : Type (u + 1)

The category of additive semigroups and semigroup morphisms.

Equations

• AddSemigroupCat = CategoryTheory.Bundled AddSemigroup

def SemigroupCat : Type (u + 1)

The category of semigroups and semigroup morphisms.

Equations

• SemigroupCat = CategoryTheory.Bundled Semigroup

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

Equations

• AddSemigroupCat.instParentProjectionAddAddSemigroupToAdd = ⋯

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

Equations

• SemigroupCat.instParentProjectionMulSemigroupToMul = ⋯

instance SemigroupCat.instConcreteCategory : CategoryTheory.ConcreteCategory SemigroupCat

Equations

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

instance AddSemigroupCat.instConcreteCategory : CategoryTheory.ConcreteCategory AddSemigroupCat

Equations

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

instance instAddSemigroupCatLargeCategory : CategoryTheory.LargeCategory AddSemigroupCat

Equations

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

instance AddSemigroupCat.instCoeSortType : CoeSort AddSemigroupCat (Type u_1)

Equations

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

instance SemigroupCat.instCoeSortType : CoeSort SemigroupCat (Type u_1)

Equations

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

def SemigroupCat.forget_obj_eq_coe (R : SemigroupCat) : Prop

Equations

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

def AddSemigroupCat.forget_obj_eq_coe (R : AddSemigroupCat) : Prop

Equations

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

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

Equations

• X.instSemigroupα = X.str

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

Equations

• X.instSemigroupα = X.str

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

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Construct a bundled AddSemigroupCat from the underlying type and typeclass.

Equations

• AddSemigroupCat.of M = CategoryTheory.Bundled.of M

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

Construct a bundled SemigroupCat from the underlying type and typeclass.

Equations

• SemigroupCat.of M = CategoryTheory.Bundled.of M

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Typecheck an AddHom as a morphism in AddSemigroupCat.

Equations

• AddSemigroupCat.ofHom f = f

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

Typecheck a MulHom as a morphism in SemigroupCat.

Equations

• SemigroupCat.ofHom f = f

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

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

instance AddSemigroupCat.instInhabited : Inhabited AddSemigroupCat

Equations

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

instance SemigroupCat.instInhabited : Inhabited SemigroupCat

Equations

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

instance AddSemigroupCat.hasForgetToAddMagmaCat : CategoryTheory.HasForget₂ AddSemigroupCat AddMagmaCat

Equations

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

instance SemigroupCat.hasForgetToMagmaCat : CategoryTheory.HasForget₂ SemigroupCat MagmaCat

Equations

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

theorem AddEquiv.toAddMagmaCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [Add X] [Add Y] (e : X ≃+ Y) : CategoryTheory.CategoryStruct.comp e.toAddHom e.symm.toAddHom = CategoryTheory.CategoryStruct.id (AddMagmaCat.of X)

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 := ⋯ }

theorem AddEquiv.toAddMagmaCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [Add X] [Add Y] (e : X ≃+ Y) : CategoryTheory.CategoryStruct.comp e.symm.toAddHom e.toAddHom = CategoryTheory.CategoryStruct.id (AddMagmaCat.of Y)

@[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

@[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 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

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 := ⋯ }

theorem AddEquiv.toAddSemigroupCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) : CategoryTheory.CategoryStruct.comp e.symm.toAddHom e.toAddHom = CategoryTheory.CategoryStruct.id (AddSemigroupCat.of Y)

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

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

Equations

• e.toAddSemigroupCatIso = { hom := e.toAddHom, inv := e.symm.toAddHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem AddEquiv.toAddSemigroupCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) : CategoryTheory.CategoryStruct.comp e.toAddHom e.symm.toAddHom = CategoryTheory.CategoryStruct.id (AddSemigroupCat.of X)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• e.toSemigroupCatIso = { hom := e.toMulHom, inv := e.symm.toMulHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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.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.addSemigroupCatIsoToAddEquiv {X : AddSemigroupCat} {Y : AddSemigroupCat} (i : X ≅ Y) : ↑X ≃+ ↑Y

Build an AddEquiv from an isomorphism in the category AddSemigroup.

Equations

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

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

Build a MulEquiv from an isomorphism in the category Semigroup.

Equations

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

theorem addEquivIsoAddMagmaIso.proof_2 {X : Type u_1} {Y : Type u_1} [Add X] [Add Y] : (CategoryTheory.CategoryStruct.comp (fun (i : AddMagmaCat.of X ≅ AddMagmaCat.of Y) => i.addMagmaCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddMagmaCatIso) = CategoryTheory.CategoryStruct.comp (fun (i : AddMagmaCat.of X ≅ AddMagmaCat.of Y) => i.addMagmaCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddMagmaCatIso

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.

theorem addEquivIsoAddMagmaIso.proof_1 {X : Type u_1} {Y : Type u_1} [Add X] [Add Y] : (CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddMagmaCatIso) fun (i : AddMagmaCat.of X ≅ AddMagmaCat.of Y) => i.addMagmaCatIsoToAddEquiv) = CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddMagmaCatIso) fun (i : AddMagmaCat.of X ≅ AddMagmaCat.of Y) => i.addMagmaCatIsoToAddEquiv

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 := ⋯ }

theorem addEquivIsoAddSemigroupCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [AddSemigroup X] [AddSemigroup Y] : (CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddSemigroupCatIso) fun (i : AddSemigroupCat.of X ≅ AddSemigroupCat.of Y) => i.addSemigroupCatIsoToAddEquiv) = CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddSemigroupCatIso) fun (i : AddSemigroupCat.of X ≅ AddSemigroupCat.of Y) => i.addSemigroupCatIsoToAddEquiv

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

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

Equations

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

theorem addEquivIsoAddSemigroupCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [AddSemigroup X] [AddSemigroup Y] : (CategoryTheory.CategoryStruct.comp (fun (i : AddSemigroupCat.of X ≅ AddSemigroupCat.of Y) => i.addSemigroupCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddSemigroupCatIso) = CategoryTheory.CategoryStruct.comp (fun (i : AddSemigroupCat.of X ≅ AddSemigroupCat.of Y) => i.addSemigroupCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddSemigroupCatIso

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

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

Equations

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

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

Equations

• AddMagmaCat.forgetReflectsIsos = ⋯

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

Equations

• MagmaCat.forgetReflectsIsos = ⋯

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

Equations

• AddSemigroupCat.forgetReflectsIsos = ⋯

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

Equations

• SemigroupCat.forgetReflectsIsos = ⋯

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

Equations

• AddSemigroupCat.forget₂_full = ⋯

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

Equations

• SemigroupCat.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.