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.

def MagmaCat : Type (u + 1)

The category of magmas and magma morphisms.

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

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

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

instance AddMagmaCat.bundledHom : CategoryTheory.BundledHom AddHom

instance MagmaCat.bundledHom : CategoryTheory.BundledHom MulHom

instance MagmaCat.instConcreteCategory : CategoryTheory.ConcreteCategory MagmaCat

instance instAddMagmaCatLargeCategory : CategoryTheory.LargeCategory AddMagmaCat

instance AddMagmaCat.instConcreteCategory : CategoryTheory.ConcreteCategory AddMagmaCat

instance AddMagmaCat.instCoeSortAddMagmaCatType : CoeSort AddMagmaCat (Type u_1)

instance MagmaCat.instCoeSortMagmaCatType : CoeSort MagmaCat (Type u_1)

def MagmaCat.forget_obj_eq_coe (R : MagmaCat) : Prop

def AddMagmaCat.forget_obj_eq_coe (R : AddMagmaCat) : Prop

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

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

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

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

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

Construct a bundled AddMagmaCat from the underlying type and typeclass.

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

Construct a bundled MagmaCat from the underlying type and typeclass.

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

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.

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

instance MagmaCat.instInhabitedMagmaCat : Inhabited MagmaCat

def AddSemigroupCat : Type (u + 1)

The category of additive semigroups and semigroup morphisms.

def SemigroupCat : Type (u + 1)

The category of semigroups and semigroup morphisms.

theorem AddSemigroupCat.instParentProjectionTypeAddAddSemigroupToAdd.proof_1 : CategoryTheory.BundledHom.ParentProjection @AddSemigroup.toAdd

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

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

instance SemigroupCat.instConcreteCategory : CategoryTheory.ConcreteCategory SemigroupCat

instance AddSemigroupCat.instConcreteCategory : CategoryTheory.ConcreteCategory AddSemigroupCat

instance instAddSemigroupCatLargeCategory : CategoryTheory.LargeCategory AddSemigroupCat

instance AddSemigroupCat.instCoeSortAddSemigroupCatType : CoeSort AddSemigroupCat (Type u_1)

instance SemigroupCat.instCoeSortSemigroupCatType : CoeSort SemigroupCat (Type u_1)

def SemigroupCat.forget_obj_eq_coe (R : SemigroupCat) : Prop

def AddSemigroupCat.forget_obj_eq_coe (R : AddSemigroupCat) : Prop

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

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

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

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

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

Construct a bundled AddSemigroupCat from the underlying type and typeclass.

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

Construct a bundled SemigroupCat from the underlying type and typeclass.

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

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.

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

instance SemigroupCat.instInhabitedSemigroupCat : Inhabited SemigroupCat

instance AddSemigroupCat.hasForgetToAddMagmaCat : CategoryTheory.HasForget₂ AddSemigroupCat AddMagmaCat

instance SemigroupCat.hasForgetToMagmaCat : CategoryTheory.HasForget₂ SemigroupCat MagmaCat

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)

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.

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

@[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 = Equiv.toFun e.toEquiv 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 = Equiv.toFun (AddEquiv.symm e).toEquiv 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 = Equiv.toFun e.toEquiv 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.

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)

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.

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)

@[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 = Equiv.toFun (MulEquiv.symm e).toEquiv 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 = Equiv.toFun (AddEquiv.symm e).toEquiv 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 = Equiv.toFun e.toEquiv 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 = Equiv.toFun e.toEquiv 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.

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

Build an AddEquiv from an isomorphism in the category AddMagma.

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

Build a MulEquiv from an isomorphism in the category Magma.

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

Build an AddEquiv from an isomorphism in the category AddSemigroup.

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

Build a MulEquiv from an isomorphism in the category Semigroup.

theorem addEquivIsoAddMagmaIso.proof_2 {X : Type u_1} {Y : Type u_1} [Add X] [Add Y] : (CategoryTheory.CategoryStruct.comp (fun i => CategoryTheory.Iso.addMagmaCatIsoToAddEquiv i) fun e => AddEquiv.toAddMagmaCatIso e) = CategoryTheory.CategoryStruct.comp (fun i => CategoryTheory.Iso.addMagmaCatIsoToAddEquiv i) fun e => AddEquiv.toAddMagmaCatIso e

theorem addEquivIsoAddMagmaIso.proof_1 {X : Type u_1} {Y : Type u_1} [Add X] [Add Y] : (CategoryTheory.CategoryStruct.comp (fun e => AddEquiv.toAddMagmaCatIso e) fun i => CategoryTheory.Iso.addMagmaCatIsoToAddEquiv i) = CategoryTheory.CategoryStruct.comp (fun e => AddEquiv.toAddMagmaCatIso e) fun i => CategoryTheory.Iso.addMagmaCatIsoToAddEquiv i

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

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

theorem addEquivIsoAddSemigroupCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [AddSemigroup X] [AddSemigroup Y] : (CategoryTheory.CategoryStruct.comp (fun i => CategoryTheory.Iso.addSemigroupCatIsoToAddEquiv i) fun e => AddEquiv.toAddSemigroupCatIso e) = CategoryTheory.CategoryStruct.comp (fun i => CategoryTheory.Iso.addSemigroupCatIsoToAddEquiv i) fun e => AddEquiv.toAddSemigroupCatIso e

theorem addEquivIsoAddSemigroupCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [AddSemigroup X] [AddSemigroup Y] : (CategoryTheory.CategoryStruct.comp (fun e => AddEquiv.toAddSemigroupCatIso e) fun i => CategoryTheory.Iso.addSemigroupCatIsoToAddEquiv i) = CategoryTheory.CategoryStruct.comp (fun e => AddEquiv.toAddSemigroupCatIso e) fun i => 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

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

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

theorem AddMagmaCat.forgetReflectsIsos.proof_1 : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget AddMagmaCat)

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

theorem AddSemigroupCat.forgetReflectsIsos.proof_1 : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget AddSemigroupCat)

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

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

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

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} f => f) f) = f

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

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.