Documentation

Mathlib.Algebra.Category.Semigrp.Basic

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

Type (u + 1)

The category of magmas and magma morphisms.

Equations

MagmaCat = CategoryTheory.Bundled Mul

Instances For

def AddMagmaCat :

Type (u + 1)

The category of additive magmas and additive magma morphisms.

Equations

AddMagmaCat = CategoryTheory.Bundled Add

Instances For

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) :

Equations

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

Instances For

def AddMagmaCat.forget_obj_eq_coe (R : AddMagmaCat) :

Equations

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

Instances For

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 Y : MagmaCat) :

FunLike (X ⟶ Y) ↑X ↑Y

Equations

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

instance AddMagmaCat.instFunLike (X Y : AddMagmaCat) :

FunLike (X ⟶ Y) ↑X ↑Y

Equations

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

instance MagmaCat.instMulHomClass (X Y : MagmaCat) :

MulHomClass (X ⟶ Y) ↑X ↑Y

instance AddMagmaCat.instAddHomClass (X Y : AddMagmaCat) :

AddHomClass (X ⟶ Y) ↑X ↑Y

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

Construct a bundled MagmaCat from the underlying type and typeclass.

Equations

MagmaCat.of M = CategoryTheory.Bundled.of M

Instances For

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

Construct a bundled AddMagmaCat from the underlying type and typeclass.

Equations

AddMagmaCat.of M = CategoryTheory.Bundled.of M

Instances For

@[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 Y : Type u_1} [Mul X] [Mul Y] (e : X ≃* Y) :

⇑↑e = ⇑e

@[simp]

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

⇑↑e = ⇑e

def MagmaCat.ofHom {X 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

Instances For

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

AddMagmaCat.of X ⟶ AddMagmaCat.of Y

Typecheck an AddHom as a morphism in AddMagmaCat.

Equations

AddMagmaCat.ofHom f = f

Instances For

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

(MagmaCat.ofHom f) x = f x

theorem AddMagmaCat.ofHom_apply {X Y : Type u} [Add X] [Add Y] (f : 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} }

Type (u + 1)

The category of semigroups and semigroup morphisms.

Equations

Semigrp = CategoryTheory.Bundled Semigroup

Instances For

def AddSemigrp :

Type (u + 1)

The category of additive semigroups and semigroup morphisms.

Equations

AddSemigrp = CategoryTheory.Bundled AddSemigroup

Instances For

instance Semigrp.instParentProjectionMulSemigroupToMul :

CategoryTheory.BundledHom.ParentProjection @Semigroup.toMul

instance AddSemigrp.instParentProjectionAddAddSemigroupToAdd :

CategoryTheory.BundledHom.ParentProjection @AddSemigroup.toAdd

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) :

Equations

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

Instances For

def AddSemigrp.forget_obj_eq_coe (R : AddSemigrp) :

Equations

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

Instances For

instance Semigrp.instSemigroupα (X : Semigrp) :

Equations

X.instSemigroupα = X.str

instance AddSemigrp.instSemigroupα (X : AddSemigrp) :

AddSemigroup ↑X

Equations

X.instSemigroupα = X.str

instance Semigrp.instFunLike (X Y : Semigrp) :

FunLike (X ⟶ Y) ↑X ↑Y

Equations

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

instance AddSemigrp.instFunLike (X Y : AddSemigrp) :

FunLike (X ⟶ Y) ↑X ↑Y

Equations

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

instance Semigrp.instMulHomClass (X Y : Semigrp) :

MulHomClass (X ⟶ Y) ↑X ↑Y

instance AddSemigrp.instAddHomClass (X Y : AddSemigrp) :

AddHomClass (X ⟶ Y) ↑X ↑Y

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

Construct a bundled Semigrp from the underlying type and typeclass.

Equations

Semigrp.of M = CategoryTheory.Bundled.of M

Instances For

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

Construct a bundled AddSemigrp from the underlying type and typeclass.

Equations

AddSemigrp.of M = CategoryTheory.Bundled.of M

Instances For

@[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 Y : Type u_1} [Semigroup X] [Semigroup Y] (e : X ≃* Y) :

⇑↑e = ⇑e

@[simp]

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

⇑↑e = ⇑e

def Semigrp.ofHom {X 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

Instances For

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

AddSemigrp.of X ⟶ AddSemigrp.of Y

Typecheck an AddHom as a morphism in AddSemigrp.

Equations

AddSemigrp.ofHom f = f

Instances For

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

(Semigrp.ofHom f) x = f x

theorem AddSemigrp.ofHom_apply {X Y : Type u} [AddSemigroup X] [AddSemigroup Y] (f : 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 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 := ⋯ }

Instances For

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 := e.toAddHom, inv := e.symm.toAddHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

@[simp]

theorem AddEquiv.toAddMagmaCatIso_inv_apply {X 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 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 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 Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) (a✝ : Y) :

e.toMagmaCatIso.inv a✝ = e.symm.toFun a✝

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 := e.toMulHom, inv := e.symm.toMulHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

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 := e.toAddHom, inv := e.symm.toAddHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

@[simp]

theorem MulEquiv.toSemigrpIso_inv_apply {X 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 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 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 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 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 ⋯ ⋯

Instances For

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 = AddHom.toAddEquiv i.hom i.inv ⋯ ⋯

Instances For

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 = MulHom.toMulEquiv i.hom i.inv ⋯ ⋯

Instances For

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 = AddHom.toAddEquiv i.hom i.inv ⋯ ⋯

Instances For

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

Instances For

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.

Instances For

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

Instances For

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

Instances For

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

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.