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

Equations

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

instance MagmaCat.instCoeSortMagmaCatType : CoeSort MagmaCat (Type u_1)

Equations

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

def MagmaCat.forget_obj_eq_coe (R : MagmaCat) : Prop

Equations

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

def AddMagmaCat.forget_obj_eq_coe (R : AddMagmaCat) : Prop

Equations

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

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

Equations

• AddMagmaCat.instMulα X = X.str

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

Equations

• MagmaCat.instMulα X = X.str

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

Equations

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

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

Equations

• MagmaCat.instFunLike X 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.instInhabitedAddMagmaCat : Inhabited AddMagmaCat

Equations

• AddMagmaCat.instInhabitedAddMagmaCat = { default := AddMagmaCat.of PEmpty.{u_1 + 1} }

instance MagmaCat.instInhabitedMagmaCat : Inhabited MagmaCat

Equations

• MagmaCat.instInhabitedMagmaCat = { 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.instParentProjectionTypeAddAddSemigroupToAdd : CategoryTheory.BundledHom.ParentProjection @AddSemigroup.toAdd

Equations

• AddSemigroupCat.instParentProjectionTypeAddAddSemigroupToAdd = ⋯

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

Equations

• SemigroupCat.instParentProjectionTypeMulSemigroupToMul = ⋯

instance SemigroupCat.instConcreteCategory : CategoryTheory.ConcreteCategory SemigroupCat

Equations

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

instance AddSemigroupCat.instConcreteCategory : CategoryTheory.ConcreteCategory AddSemigroupCat

Equations

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

instance instAddSemigroupCatLargeCategory : CategoryTheory.LargeCategory AddSemigroupCat

Equations

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

instance AddSemigroupCat.instCoeSortAddSemigroupCatType : CoeSort AddSemigroupCat (Type u_1)

Equations

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

instance SemigroupCat.instCoeSortSemigroupCatType : CoeSort SemigroupCat (Type u_1)

Equations

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

def SemigroupCat.forget_obj_eq_coe (R : SemigroupCat) : Prop

Equations

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

def AddSemigroupCat.forget_obj_eq_coe (R : AddSemigroupCat) : Prop

Equations

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

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

Equations

• AddSemigroupCat.instSemigroupα X = X.str

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

Equations

• SemigroupCat.instSemigroupα X = X.str

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

Equations

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

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

Equations

• SemigroupCat.instFunLike X 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.instInhabitedAddSemigroupCat : Inhabited AddSemigroupCat

Equations

• AddSemigroupCat.instInhabitedAddSemigroupCat = { default := AddSemigroupCat.of PEmpty.{u_1 + 1} }

instance SemigroupCat.instInhabitedSemigroupCat : Inhabited SemigroupCat

Equations

• SemigroupCat.instInhabitedSemigroupCat = { 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

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

• AddEquiv.toAddMagmaCatIso e = { hom := AddEquiv.toAddHom e, inv := AddEquiv.toAddHom (AddEquiv.symm e), hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

@[simp]

theorem MulEquiv.toMagmaCatIso_hom_apply {X : Type u} {Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) : ∀ (a : X), (MulEquiv.toMagmaCatIso e).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), (AddEquiv.toAddMagmaCatIso e).inv a = (AddEquiv.symm e).toFun a

@[simp]

theorem AddEquiv.toAddMagmaCatIso_hom_apply {X : Type u} {Y : Type u} [Add X] [Add Y] (e : X ≃+ Y) : ∀ (a : X), (AddEquiv.toAddMagmaCatIso e).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), (MulEquiv.toMagmaCatIso e).inv a = (MulEquiv.symm 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

• MulEquiv.toMagmaCatIso e = { hom := MulEquiv.toMulHom e, inv := MulEquiv.toMulHom (MulEquiv.symm e), 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 (AddEquiv.toAddHom (AddEquiv.symm e)) (AddEquiv.toAddHom e) = CategoryTheory.CategoryStruct.id (AddSemigroupCat.of Y)

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

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

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

@[simp]

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

@[simp]

theorem AddEquiv.toAddSemigroupCatIso_hom_apply {X : Type u} {Y : Type u} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) : ∀ (a : X), (AddEquiv.toAddSemigroupCatIso e).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), (AddEquiv.toAddSemigroupCatIso e).inv a = (AddEquiv.symm e).toFun a

@[simp]

theorem MulEquiv.toSemigroupCatIso_hom_apply {X : Type u} {Y : Type u} [Semigroup X] [Semigroup Y] (e : X ≃* Y) : ∀ (a : X), (MulEquiv.toSemigroupCatIso e).hom a = e.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

• MulEquiv.toSemigroupCatIso e = { hom := MulEquiv.toMulHom e, inv := MulEquiv.toMulHom (MulEquiv.symm e), 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 AddMagma.

Equations

• CategoryTheory.Iso.addMagmaCatIsoToAddEquiv i = 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 Magma.

Equations

• CategoryTheory.Iso.magmaCatIsoToMulEquiv i = 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

• CategoryTheory.Iso.addSemigroupCatIsoToAddEquiv i = 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

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

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 AddMagma

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) => AddEquiv.toAddMagmaCatIso e) fun (i : AddMagmaCat.of X ≅ AddMagmaCat.of Y) => CategoryTheory.Iso.addMagmaCatIsoToAddEquiv i) = CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => AddEquiv.toAddMagmaCatIso e) fun (i : AddMagmaCat.of X ≅ AddMagmaCat.of Y) => CategoryTheory.Iso.addMagmaCatIsoToAddEquiv i

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) => CategoryTheory.Iso.addMagmaCatIsoToAddEquiv i) fun (e : X ≃+ Y) => AddEquiv.toAddMagmaCatIso e) = CategoryTheory.CategoryStruct.comp (fun (i : AddMagmaCat.of X ≅ AddMagmaCat.of Y) => CategoryTheory.Iso.addMagmaCatIsoToAddEquiv i) fun (e : X ≃+ Y) => AddEquiv.toAddMagmaCatIso e

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 Magma

Equations

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

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

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) => CategoryTheory.Iso.addSemigroupCatIsoToAddEquiv i) fun (e : X ≃+ Y) => AddEquiv.toAddSemigroupCatIso e) = CategoryTheory.CategoryStruct.comp (fun (i : AddSemigroupCat.of X ≅ AddSemigroupCat.of Y) => CategoryTheory.Iso.addSemigroupCatIsoToAddEquiv i) fun (e : X ≃+ Y) => AddEquiv.toAddSemigroupCatIso e

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.ReflectsIsomorphisms (CategoryTheory.forget AddMagmaCat)

Equations

• AddMagmaCat.forgetReflectsIsos = ⋯

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

Equations

• MagmaCat.forgetReflectsIsos = ⋯

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

Equations

• AddSemigroupCat.forgetReflectsIsos = ⋯

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

Equations

• SemigroupCat.forgetReflectsIsos = ⋯

theorem AddSemigroupCat.forget₂Full.proof_1 {X_1 : AddSemigroupCat} {Y_1 : AddSemigroupCat} (f : (CategoryTheory.forget₂ AddSemigroupCat AddMagmaCat).obj X_1 ⟶ (CategoryTheory.forget₂ AddSemigroupCat AddMagmaCat).obj Y_1) : (CategoryTheory.forget₂ AddSemigroupCat AddMagmaCat).map ((fun {X Y : AddSemigroupCat} (f : (CategoryTheory.forget₂ AddSemigroupCat AddMagmaCat).obj X ⟶ (CategoryTheory.forget₂ AddSemigroupCat AddMagmaCat).obj Y) => f) f) = f

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

Equations

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

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

Equations

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

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.