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
The category of additive magmas and additive magma morphisms.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- MagmaCat.instCoeSortType = { coe := fun (X : MagmaCat) => ↑X }
Equations
- AddMagmaCat.instCoeSortType = { coe := fun (X : AddMagmaCat) => ↑X }
Equations
- R.forget_obj_eq_coe = ((CategoryTheory.forget MagmaCat).obj R = ↑R)
Instances For
Equations
- R.forget_obj_eq_coe = ((CategoryTheory.forget AddMagmaCat).obj R = ↑R)
Instances For
Equations
- X.instFunLike Y = inferInstanceAs (FunLike (↑X →ₙ* ↑Y) ↑X ↑Y)
Equations
- X.instFunLike Y = inferInstanceAs (FunLike (↑X →ₙ+ ↑Y) ↑X ↑Y)
Typecheck an AddHom
as a morphism in AddMagmaCat
.
Equations
- AddMagmaCat.ofHom f = f
Instances For
Equations
- MagmaCat.instInhabited = { default := MagmaCat.of PEmpty.{?u.1 + 1} }
Equations
- AddMagmaCat.instInhabited = { default := AddMagmaCat.of PEmpty.{?u.1 + 1} }
The category of additive semigroups and semigroup morphisms.
Equations
Instances For
Equations
- Semigrp.instCoeSortType = { coe := fun (X : Semigrp) => ↑X }
Equations
- AddSemigrp.instCoeSortType = { coe := fun (X : AddSemigrp) => ↑X }
Equations
- R.forget_obj_eq_coe = ((CategoryTheory.forget Semigrp).obj R = ↑R)
Instances For
Equations
- R.forget_obj_eq_coe = ((CategoryTheory.forget AddSemigrp).obj R = ↑R)
Instances For
Equations
- X.instSemigroupα = X.str
Equations
- X.instFunLike Y = inferInstanceAs (FunLike (↑X →ₙ* ↑Y) ↑X ↑Y)
Equations
- X.instFunLike Y = inferInstanceAs (FunLike (↑X →ₙ+ ↑Y) ↑X ↑Y)
Typecheck a MulHom
as a morphism in Semigrp
.
Equations
- Semigrp.ofHom f = f
Instances For
Typecheck an AddHom
as a morphism in AddSemigrp
.
Equations
- AddSemigrp.ofHom f = f
Instances For
Equations
- Semigrp.instInhabited = { default := Semigrp.of PEmpty.{?u.1 + 1} }
Equations
- AddSemigrp.instInhabited = { default := AddSemigrp.of PEmpty.{?u.1 + 1} }
Build an isomorphism in the category MagmaCat
from a MulEquiv
between Mul
s.
Equations
- e.toMagmaCatIso = { hom := e.toMulHom, inv := e.symm.toMulHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Build an isomorphism in the category AddMagmaCat
from an AddEquiv
between Add
s.
Equations
- e.toAddMagmaCatIso = { hom := e.toAddHom, inv := e.symm.toAddHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Build an isomorphism in the category Semigroup
from a MulEquiv
between Semigroup
s.
Equations
- e.toSemigrpIso = { hom := e.toMulHom, inv := e.symm.toMulHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Build an isomorphism in the category
AddSemigroup
from an AddEquiv
between AddSemigroup
s.
Equations
- e.toAddSemigrpIso = { hom := e.toAddHom, inv := e.symm.toAddHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Build a MulEquiv
from an isomorphism in the category MagmaCat
.
Equations
- i.magmaCatIsoToMulEquiv = MulHom.toMulEquiv i.hom i.inv ⋯ ⋯
Instances For
Build an AddEquiv
from an isomorphism in the category AddMagmaCat
.
Equations
- i.addMagmaCatIsoToAddEquiv = AddHom.toAddEquiv i.hom i.inv ⋯ ⋯
Instances For
Build a MulEquiv
from an isomorphism in the category Semigroup
.
Equations
- i.semigrpIsoToMulEquiv = MulHom.toMulEquiv i.hom i.inv ⋯ ⋯
Instances For
Build an AddEquiv
from an isomorphism in the category AddSemigroup
.
Equations
- i.addSemigrpIsoToAddEquiv = AddHom.toAddEquiv i.hom i.inv ⋯ ⋯
Instances For
multiplicative equivalences between Mul
s 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
additive equivalences between Add
s are the same
as (isomorphic to) isomorphisms in AddMagmaCat
Equations
- One or more equations did not get rendered due to their size.
Instances For
multiplicative equivalences between Semigroup
s 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
additive equivalences between AddSemigroup
s 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
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.