Category instances for Monoid, AddMonoid, CommMonoid, and AddCommMonoid.

We introduce the bundled categories:

• MonCat
• AddMonCat
• CommMonCat
• AddCommMonCat

along with the relevant forgetful functors between them.

structure AddMonCat : Type (u + 1)

The category of additive monoids and monoid morphisms.

• carrier : Type u

  The underlying type.

• str : AddMonoid ↑self

structure MonCat : Type (u + 1)

The category of monoids and monoid morphisms.

• carrier : Type u

  The underlying type.

• str : Monoid ↑self

@[instance_reducible]

instance MonCat.instCoeSortType : CoeSort MonCat (Type u)

Equations

• MonCat.instCoeSortType = { coe := MonCat.carrier }

@[instance_reducible]

instance AddMonCat.instCoeSortType : CoeSort AddMonCat (Type u)

Equations

• AddMonCat.instCoeSortType = { coe := AddMonCat.carrier }

@[reducible, inline]

abbrev MonCat.of (M : Type u) [Monoid M] : MonCat

Construct a bundled MonCat from the underlying type and typeclass.

Equations

• ↧M = { carrier := M, str := inst✝ }

@[reducible, inline]

abbrev AddMonCat.of (M : Type u) [AddMonoid M] : AddMonCat

Construct a bundled AddMonCat from the underlying type and typeclass.

Equations

• ↧M = { carrier := M, str := inst✝ }

def AddMonCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prints AddMonCat.of X as ↧X.

Equations

• AddMonCat.delabOf = CategoryTheory.delabOf

def MonCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prints MonCat.of X as ↧X.

Equations

• MonCat.delabOf = CategoryTheory.delabOf

structure AddMonCat.Hom (A B : AddMonCat) : Type u

The type of morphisms in AddMonCat.

• _mkInternal :: (
• hom' : ↑A →+ ↑B

  The underlying monoid homomorphism.

• )

theorem AddMonCat.Hom.ext_iff {A B : AddMonCat} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

theorem AddMonCat.Hom.ext {A B : AddMonCat} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

structure MonCat.Hom (A B : MonCat) : Type u

The type of morphisms in MonCat.

• _mkInternal :: (
• hom' : ↑A →* ↑B

  The underlying monoid homomorphism.

• )

theorem MonCat.Hom.ext_iff {A B : MonCat} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

theorem MonCat.Hom.ext {A B : MonCat} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

@[instance_reducible]

instance MonCat.instCategory : CategoryTheory.Category.{u, u + 1} MonCat

Equations

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

@[instance_reducible]

instance AddMonCat.instCategory : CategoryTheory.Category.{u, u + 1} AddMonCat

Equations

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

@[instance_reducible]

instance MonCat.instConcreteCategoryMonoidHomCarrier : CategoryTheory.ConcreteCategory MonCat fun (x1 x2 : MonCat) => ↑x1 →* ↑x2

Equations

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

@[instance_reducible]

instance AddMonCat.instConcreteCategoryAddMonoidHomCarrier : CategoryTheory.ConcreteCategory AddMonCat fun (x1 x2 : AddMonCat) => ↑x1 →+ ↑x2

Equations

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

@[reducible, inline]

abbrev MonCat.Hom.hom {X Y : MonCat} (f : X.Hom Y) : ↑X →* ↑Y

Turn a morphism in MonCat back into a MonoidHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev AddMonCat.Hom.hom {X Y : AddMonCat} (f : X.Hom Y) : ↑X →+ ↑Y

Turn a morphism in AddMonCat back into an AddMonoidHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev MonCat.ofHom {X Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) : ↧X ⟶ ↧Y

Typecheck a MonoidHom as a morphism in MonCat.

Equations

• MonCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

@[reducible, inline]

abbrev AddMonCat.ofHom {X Y : Type u} [AddMonoid X] [AddMonoid Y] (f : X →+ Y) : ↧X ⟶ ↧Y

Typecheck an AddMonoidHom as a morphism in AddMonCat.

Equations

• AddMonCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def MonCat.Hom.Simps.hom (X Y : MonCat) (f : X.Hom Y) : ↑X →* ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• MonCat.Hom.Simps.hom X Y f = f.hom

def AddMonCat.Hom.Simps.hom (X Y : AddMonCat) (f : X.Hom Y) : ↑X →+ ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• AddMonCat.Hom.Simps.hom X Y f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem MonCat.coe_id {X : MonCat} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem AddMonCat.coe_id {X : AddMonCat} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem MonCat.coe_comp {X Y Z : MonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem AddMonCat.coe_comp {X Y Z : AddMonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem MonCat.forget_map {X Y : MonCat} (f : X ⟶ Y) : ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget MonCat).map f)) = ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem AddMonCat.forget_map {X Y : AddMonCat} (f : X ⟶ Y) : ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget AddMonCat).map f)) = ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem MonCat.ext {X Y : MonCat} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem AddMonCat.ext {X Y : AddMonCat} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem MonCat.ext_iff {X Y : MonCat} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

theorem AddMonCat.ext_iff {X Y : AddMonCat} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

theorem MonCat.coe_of (M : Type u) [Monoid M] : ↑↧M = M

theorem AddMonCat.coe_of (M : Type u) [AddMonoid M] : ↑↧M = M

@[simp]

theorem MonCat.hom_id {M : MonCat} : Hom.hom (CategoryTheory.CategoryStruct.id M) = MonoidHom.id ↑M

@[simp]

theorem AddMonCat.hom_id {M : AddMonCat} : Hom.hom (CategoryTheory.CategoryStruct.id M) = AddMonoidHom.id ↑M

theorem MonCat.id_apply (M : MonCat) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x

theorem AddMonCat.id_apply (M : AddMonCat) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x

@[simp]

theorem MonCat.hom_comp {M N T : MonCat} (f : M ⟶ N) (g : N ⟶ T) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

@[simp]

theorem AddMonCat.hom_comp {M N T : AddMonCat} (f : M ⟶ N) (g : N ⟶ T) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem MonCat.comp_apply {M N T : MonCat} (f : M ⟶ N) (g : N ⟶ T) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem AddMonCat.comp_apply {M N T : AddMonCat} (f : M ⟶ N) (g : N ⟶ T) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem MonCat.hom_ext {M N : MonCat} {f g : M ⟶ N} (hf : Hom.hom f = Hom.hom g) : f = g

theorem AddMonCat.hom_ext {M N : AddMonCat} {f g : M ⟶ N} (hf : Hom.hom f = Hom.hom g) : f = g

theorem AddMonCat.hom_ext_iff {M N : AddMonCat} {f g : M ⟶ N} : f = g ↔ Hom.hom f = Hom.hom g

theorem MonCat.hom_ext_iff {M N : MonCat} {f g : M ⟶ N} : f = g ↔ Hom.hom f = Hom.hom g

@[simp]

theorem MonCat.hom_ofHom {M N : Type u} [Monoid M] [Monoid N] (f : M →* N) : Hom.hom (ofHom f) = f

@[simp]

theorem AddMonCat.hom_ofHom {M N : Type u} [AddMonoid M] [AddMonoid N] (f : M →+ N) : Hom.hom (ofHom f) = f

@[simp]

theorem MonCat.ofHom_hom {M N : MonCat} (f : M ⟶ N) : ofHom (Hom.hom f) = f

@[simp]

theorem AddMonCat.ofHom_hom {M N : AddMonCat} (f : M ⟶ N) : ofHom (Hom.hom f) = f

@[simp]

theorem MonCat.ofHom_id {M : Type u} [Monoid M] : ofHom (MonoidHom.id M) = CategoryTheory.CategoryStruct.id ↧M

@[simp]

theorem AddMonCat.ofHom_id {M : Type u} [AddMonoid M] : ofHom (AddMonoidHom.id M) = CategoryTheory.CategoryStruct.id ↧M

@[simp]

theorem MonCat.ofHom_comp {M N P : Type u} [Monoid M] [Monoid N] [Monoid P] (f : M →* N) (g : N →* P) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

@[simp]

theorem AddMonCat.ofHom_comp {M N P : Type u} [AddMonoid M] [AddMonoid N] [AddMonoid P] (f : M →+ N) (g : N →+ P) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem MonCat.ofHom_apply {X Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem AddMonCat.ofHom_apply {X Y : Type u} [AddMonoid X] [AddMonoid Y] (f : X →+ Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem MonCat.inv_hom_apply {M N : MonCat} (e : M ≅ N) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem AddMonCat.neg_hom_apply {M N : AddMonCat} (e : M ≅ N) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem MonCat.hom_inv_apply {M N : MonCat} (e : M ≅ N) (s : ↑N) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

theorem AddMonCat.hom_neg_apply {M N : AddMonCat} (e : M ≅ N) (s : ↑N) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

@[instance_reducible]

instance MonCat.instInhabited : Inhabited MonCat

Equations

• MonCat.instInhabited = { default := ↧PUnit.{?u.1 + 1} }

@[instance_reducible]

instance AddMonCat.instInhabited : Inhabited AddMonCat

Equations

• AddMonCat.instInhabited = { default := ↧PUnit.{?u.1 + 1} }

@[instance_reducible]

instance MonCat.instOneHom (X Y : MonCat) : One (X ⟶ Y)

Equations

• X.instOneHom Y = { one := MonCat.ofHom 1 }

@[instance_reducible]

instance AddMonCat.instZeroHom (X Y : AddMonCat) : Zero (X ⟶ Y)

Equations

• X.instZeroHom Y = { zero := AddMonCat.ofHom 0 }

@[simp]

theorem MonCat.hom_one (X Y : MonCat) : Hom.hom 1 = 1

@[simp]

theorem AddMonCat.hom_zero (X Y : AddMonCat) : Hom.hom 0 = 0

theorem MonCat.oneHom_apply (X Y : MonCat) (x : ↑X) : (Hom.hom 1) x = 1

theorem AddMonCat.zeroHom_apply (X Y : AddMonCat) (x : ↑X) : (Hom.hom 0) x = 0

@[simp]

theorem MonCat.one_of {A : Type u_1} [Monoid A] : 1 = 1

@[simp]

theorem AddMonCat.zero_of {A : Type u_1} [AddMonoid A] : 0 = 0

@[simp]

theorem MonCat.mul_of {A : Type u_1} [Monoid A] (a b : A) : a * b = a * b

@[simp]

theorem AddMonCat.add_of {A : Type u_1} [AddMonoid A] (a b : A) : a + b = a + b

def MonCat.uliftFunctor : CategoryTheory.Functor MonCat MonCat

Universe lift functor for monoids.

Equations

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

def AddMonCat.uliftFunctor : CategoryTheory.Functor AddMonCat AddMonCat

Universe lift functor for additive monoids.

Equations

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

@[simp]

theorem AddMonCat.uliftFunctor_obj_coe (X : AddMonCat) : ↑(uliftFunctor.obj X) = ULift.{u, v} ↑X

@[simp]

theorem AddMonCat.uliftFunctor_map {x✝ x✝¹ : AddMonCat} (f : x✝ ⟶ x✝¹) : uliftFunctor.map f = ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp ((Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom))

@[simp]

theorem MonCat.uliftFunctor_map {x✝ x✝¹ : MonCat} (f : x✝ ⟶ x✝¹) : uliftFunctor.map f = ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom))

@[simp]

theorem MonCat.uliftFunctor_obj_coe (X : MonCat) : ↑(uliftFunctor.obj X) = ULift.{u, v} ↑X

structure AddCommMonCat : Type (u + 1)

The category of additive commutative monoids and monoid morphisms.

• carrier : Type u

  The underlying type.

• str : AddCommMonoid ↑self

structure CommMonCat : Type (u + 1)

The category of commutative monoids and monoid morphisms.

• carrier : Type u

  The underlying type.

• str : CommMonoid ↑self

@[instance_reducible]

instance CommMonCat.instCoeSortType : CoeSort CommMonCat (Type u)

Equations

• CommMonCat.instCoeSortType = { coe := CommMonCat.carrier }

@[instance_reducible]

instance AddCommMonCat.instCoeSortType : CoeSort AddCommMonCat (Type u)

Equations

• AddCommMonCat.instCoeSortType = { coe := AddCommMonCat.carrier }

@[reducible, inline]

abbrev CommMonCat.of (M : Type u) [CommMonoid M] : CommMonCat

Construct a bundled CommMonCat from the underlying type and typeclass.

Equations

• ↧M = { carrier := M, str := inst✝ }

@[reducible, inline]

abbrev AddCommMonCat.of (M : Type u) [AddCommMonoid M] : AddCommMonCat

Construct a bundled AddCommMonCat from the underlying type and typeclass.

Equations

• ↧M = { carrier := M, str := inst✝ }

def AddCommMonCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prints AddCommMonCat.of X as ↧X.

Equations

• AddCommMonCat.delabOf = CategoryTheory.delabOf

def CommMonCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prints CommMonCat.of X as ↧X.

Equations

• CommMonCat.delabOf = CategoryTheory.delabOf

structure AddCommMonCat.Hom (A B : AddCommMonCat) : Type u

The type of morphisms in AddCommMonCat.

• _mkInternal :: (
• hom' : ↑A →+ ↑B

  The underlying monoid homomorphism.

• )

theorem AddCommMonCat.Hom.ext {A B : AddCommMonCat} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

theorem AddCommMonCat.Hom.ext_iff {A B : AddCommMonCat} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

structure CommMonCat.Hom (A B : CommMonCat) : Type u

The type of morphisms in CommMonCat.

• _mkInternal :: (
• hom' : ↑A →* ↑B

  The underlying monoid homomorphism.

• )

theorem CommMonCat.Hom.ext_iff {A B : CommMonCat} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

theorem CommMonCat.Hom.ext {A B : CommMonCat} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

@[instance_reducible]

instance CommMonCat.instCategory : CategoryTheory.Category.{u, u + 1} CommMonCat

Equations

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

@[instance_reducible]

instance AddCommMonCat.instCategory : CategoryTheory.Category.{u, u + 1} AddCommMonCat

Equations

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

@[instance_reducible]

instance CommMonCat.instConcreteCategoryMonoidHomCarrier : CategoryTheory.ConcreteCategory CommMonCat fun (x1 x2 : CommMonCat) => ↑x1 →* ↑x2

Equations

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

@[instance_reducible]

instance AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier : CategoryTheory.ConcreteCategory AddCommMonCat fun (x1 x2 : AddCommMonCat) => ↑x1 →+ ↑x2

Equations

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

@[reducible, inline]

abbrev CommMonCat.Hom.hom {X Y : CommMonCat} (f : X.Hom Y) : ↑X →* ↑Y

Turn a morphism in CommMonCat back into a MonoidHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev AddCommMonCat.Hom.hom {X Y : AddCommMonCat} (f : X.Hom Y) : ↑X →+ ↑Y

Turn a morphism in AddCommMonCat back into an AddMonoidHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev CommMonCat.ofHom {X Y : Type u} [CommMonoid X] [CommMonoid Y] (f : X →* Y) : ↧X ⟶ ↧Y

Typecheck a MonoidHom as a morphism in CommMonCat.

Equations

• CommMonCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

@[reducible, inline]

abbrev AddCommMonCat.ofHom {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] (f : X →+ Y) : ↧X ⟶ ↧Y

Typecheck an AddMonoidHom as a morphism in AddCommMonCat.

Equations

• AddCommMonCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def CommMonCat.Hom.Simps.hom (X Y : CommMonCat) (f : X.Hom Y) : ↑X →* ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• CommMonCat.Hom.Simps.hom X Y f = f.hom

def AddCommMonCat.Hom.Simps.hom (X Y : AddCommMonCat) (f : X.Hom Y) : ↑X →+ ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• AddCommMonCat.Hom.Simps.hom X Y f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem CommMonCat.coe_id {X : CommMonCat} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem AddCommMonCat.coe_id {X : AddCommMonCat} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem CommMonCat.coe_comp {X Y Z : CommMonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem AddCommMonCat.coe_comp {X Y Z : AddCommMonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem CommMonCat.ext {X Y : CommMonCat} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem AddCommMonCat.ext {X Y : AddCommMonCat} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem AddCommMonCat.ext_iff {X Y : AddCommMonCat} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

theorem CommMonCat.ext_iff {X Y : CommMonCat} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

@[simp]

theorem CommMonCat.hom_id {M : CommMonCat} : Hom.hom (CategoryTheory.CategoryStruct.id M) = MonoidHom.id ↑M

@[simp]

theorem AddCommMonCat.hom_id {M : AddCommMonCat} : Hom.hom (CategoryTheory.CategoryStruct.id M) = AddMonoidHom.id ↑M

theorem CommMonCat.id_apply (M : CommMonCat) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x

theorem AddCommMonCat.id_apply (M : AddCommMonCat) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x

@[simp]

theorem CommMonCat.hom_comp {M N T : CommMonCat} (f : M ⟶ N) (g : N ⟶ T) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

@[simp]

theorem AddCommMonCat.hom_comp {M N T : AddCommMonCat} (f : M ⟶ N) (g : N ⟶ T) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem CommMonCat.comp_apply {M N T : CommMonCat} (f : M ⟶ N) (g : N ⟶ T) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem AddCommMonCat.comp_apply {M N T : AddCommMonCat} (f : M ⟶ N) (g : N ⟶ T) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem CommMonCat.hom_ext {M N : CommMonCat} {f g : M ⟶ N} (hf : Hom.hom f = Hom.hom g) : f = g

theorem AddCommMonCat.hom_ext {M N : AddCommMonCat} {f g : M ⟶ N} (hf : Hom.hom f = Hom.hom g) : f = g

theorem AddCommMonCat.hom_ext_iff {M N : AddCommMonCat} {f g : M ⟶ N} : f = g ↔ Hom.hom f = Hom.hom g

theorem CommMonCat.hom_ext_iff {M N : CommMonCat} {f g : M ⟶ N} : f = g ↔ Hom.hom f = Hom.hom g

@[simp]

theorem CommMonCat.hom_ofHom {M N : Type u} [CommMonoid M] [CommMonoid N] (f : M →* N) : Hom.hom (ofHom f) = f

@[simp]

theorem AddCommMonCat.hom_ofHom {M N : Type u} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) : Hom.hom (ofHom f) = f

@[simp]

theorem CommMonCat.ofHom_hom {M N : CommMonCat} (f : M ⟶ N) : ofHom (Hom.hom f) = f

@[simp]

theorem AddCommMonCat.ofHom_hom {M N : AddCommMonCat} (f : M ⟶ N) : ofHom (Hom.hom f) = f

@[simp]

theorem CommMonCat.ofHom_id {M : Type u} [CommMonoid M] : ofHom (MonoidHom.id M) = CategoryTheory.CategoryStruct.id ↧M

@[simp]

theorem AddCommMonCat.ofHom_id {M : Type u} [AddCommMonoid M] : ofHom (AddMonoidHom.id M) = CategoryTheory.CategoryStruct.id ↧M

@[simp]

theorem CommMonCat.ofHom_comp {M N P : Type u} [CommMonoid M] [CommMonoid N] [CommMonoid P] (f : M →* N) (g : N →* P) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

@[simp]

theorem AddCommMonCat.ofHom_comp {M N P : Type u} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] (f : M →+ N) (g : N →+ P) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem CommMonCat.ofHom_apply {X Y : Type u} [CommMonoid X] [CommMonoid Y] (f : X →* Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem AddCommMonCat.ofHom_apply {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] (f : X →+ Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem CommMonCat.inv_hom_apply {M N : CommMonCat} (e : M ≅ N) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem AddCommMonCat.neg_hom_apply {M N : AddCommMonCat} (e : M ≅ N) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem CommMonCat.hom_inv_apply {M N : CommMonCat} (e : M ≅ N) (s : ↑N) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

theorem AddCommMonCat.hom_neg_apply {M N : AddCommMonCat} (e : M ≅ N) (s : ↑N) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

@[instance_reducible]

instance CommMonCat.instInhabited : Inhabited CommMonCat

Equations

• CommMonCat.instInhabited = { default := ↧PUnit.{?u.1 + 1} }

@[instance_reducible]

instance AddCommMonCat.instInhabited : Inhabited AddCommMonCat

Equations

• AddCommMonCat.instInhabited = { default := ↧PUnit.{?u.1 + 1} }

theorem CommMonCat.coe_of (R : Type u) [CommMonoid R] : ↑↧R = R

theorem AddCommMonCat.coe_of (R : Type u) [AddCommMonoid R] : ↑↧R = R

@[instance_reducible]

instance CommMonCat.hasForgetToMonCat : CategoryTheory.HasForget₂ CommMonCat MonCat

Equations

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

@[instance_reducible]

instance AddCommMonCat.hasForgetToAddMonCat : CategoryTheory.HasForget₂ AddCommMonCat AddMonCat

Equations

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

@[simp]

theorem CommMonCat.coe_forget₂_obj (X : CommMonCat) : ↑((CategoryTheory.forget₂ CommMonCat MonCat).obj X) = ↑X

@[simp]

theorem AddCommMonCat.coe_forget₂_obj (X : AddCommMonCat) : ↑((CategoryTheory.forget₂ AddCommMonCat AddMonCat).obj X) = ↑X

@[simp]

theorem CommMonCat.hom_forget₂_map {X Y : CommMonCat} (f : X ⟶ Y) : MonCat.Hom.hom ((CategoryTheory.forget₂ CommMonCat MonCat).map f) = Hom.hom f

@[simp]

theorem AddCommMonCat.hom_forget₂_map {X Y : AddCommMonCat} (f : X ⟶ Y) : AddMonCat.Hom.hom ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).map f) = Hom.hom f

@[simp]

theorem CommMonCat.forget₂_map_ofHom {X Y : Type u} [CommMonoid X] [CommMonoid Y] (f : X →* Y) : (CategoryTheory.forget₂ CommMonCat MonCat).map (ofHom f) = MonCat.ofHom f

@[simp]

theorem AddCommMonCat.forget₂_map_ofHom {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] (f : X →+ Y) : (CategoryTheory.forget₂ AddCommMonCat AddMonCat).map (ofHom f) = AddMonCat.ofHom f

def CommMonCat.fullyFaithfulForgetToMonCat : (CategoryTheory.forget₂ CommMonCat MonCat).FullyFaithful

The forgetful functor from CommMonCat to MonCat is fully faithful.

Equations

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

def AddCommMonCat.fullyFaithfulForgetToAddMonCat : (CategoryTheory.forget₂ AddCommMonCat AddMonCat).FullyFaithful

The forgetful functor from AddCommMonCat to AddMonCat is fully faithful.

Equations

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

instance CommMonCat.instFullMonCatForget₂MonoidHomCarrierCarrier : (CategoryTheory.forget₂ CommMonCat MonCat).Full

instance AddCommMonCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier : (CategoryTheory.forget₂ AddCommMonCat AddMonCat).Full

@[instance_reducible]

instance CommMonCat.instCoeMonCat : Coe CommMonCat MonCat

Equations

• CommMonCat.instCoeMonCat = { coe := (CategoryTheory.forget₂ CommMonCat MonCat).obj }

@[instance_reducible]

instance AddCommMonCat.instCoeMonCat : Coe AddCommMonCat AddMonCat

Equations

• AddCommMonCat.instCoeMonCat = { coe := (CategoryTheory.forget₂ AddCommMonCat AddMonCat).obj }

def CommMonCat.uliftFunctor : CategoryTheory.Functor CommMonCat CommMonCat

Universe lift functor for commutative monoids.

Equations

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

def AddCommMonCat.uliftFunctor : CategoryTheory.Functor AddCommMonCat AddCommMonCat

Universe lift functor for additive commutative monoids.

Equations

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

@[simp]

theorem AddCommMonCat.uliftFunctor_map {x✝ x✝¹ : AddCommMonCat} (f : x✝ ⟶ x✝¹) : uliftFunctor.map f = ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp ((Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom))

@[simp]

theorem CommMonCat.uliftFunctor_map {x✝ x✝¹ : CommMonCat} (f : x✝ ⟶ x✝¹) : uliftFunctor.map f = ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom))

@[simp]

theorem CommMonCat.uliftFunctor_obj_coe (X : CommMonCat) : ↑(uliftFunctor.obj X) = ULift.{u, v} ↑X

@[simp]

theorem AddCommMonCat.uliftFunctor_obj_coe (X : AddCommMonCat) : ↑(uliftFunctor.obj X) = ULift.{u, v} ↑X

def MulEquiv.toMonCatIso {X Y : Type u} [Monoid X] [Monoid Y] (e : X ≃* Y) : ↧X ≅ ↧Y

Build an isomorphism in the category MonCat from a MulEquiv between Monoids.

Equations

• e.toMonCatIso = { hom := MonCat.ofHom e.toMonoidHom, inv := MonCat.ofHom e.symm.toMonoidHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def AddEquiv.toAddMonCatIso {X Y : Type u} [AddMonoid X] [AddMonoid Y] (e : X ≃+ Y) : ↧X ≅ ↧Y

Build an isomorphism in the category AddMonCat from an AddEquiv between AddMonoids.

Equations

• e.toAddMonCatIso = { hom := AddMonCat.ofHom e.toAddMonoidHom, inv := AddMonCat.ofHom e.symm.toAddMonoidHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem MulEquiv.toMonCatIso_inv {X Y : Type u} [Monoid X] [Monoid Y] (e : X ≃* Y) : e.toMonCatIso.inv = MonCat.ofHom e.symm.toMonoidHom

@[simp]

theorem AddEquiv.toAddMonCatIso_hom {X Y : Type u} [AddMonoid X] [AddMonoid Y] (e : X ≃+ Y) : e.toAddMonCatIso.hom = AddMonCat.ofHom e.toAddMonoidHom

@[simp]

theorem AddEquiv.toAddMonCatIso_inv {X Y : Type u} [AddMonoid X] [AddMonoid Y] (e : X ≃+ Y) : e.toAddMonCatIso.inv = AddMonCat.ofHom e.symm.toAddMonoidHom

@[simp]

theorem MulEquiv.toMonCatIso_hom {X Y : Type u} [Monoid X] [Monoid Y] (e : X ≃* Y) : e.toMonCatIso.hom = MonCat.ofHom e.toMonoidHom

def MulEquiv.toCommMonCatIso {X Y : Type u} [CommMonoid X] [CommMonoid Y] (e : X ≃* Y) : ↧X ≅ ↧Y

Build an isomorphism in the category CommMonCat from a MulEquiv between CommMonoids.

Equations

• e.toCommMonCatIso = { hom := CommMonCat.ofHom e.toMonoidHom, inv := CommMonCat.ofHom e.symm.toMonoidHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def AddEquiv.toAddCommMonCatIso {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] (e : X ≃+ Y) : ↧X ≅ ↧Y

Build an isomorphism in the category AddCommMonCat from an AddEquiv between AddCommMonoids.

Equations

• e.toAddCommMonCatIso = { hom := AddCommMonCat.ofHom e.toAddMonoidHom, inv := AddCommMonCat.ofHom e.symm.toAddMonoidHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem AddEquiv.toAddCommMonCatIso_hom {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] (e : X ≃+ Y) : e.toAddCommMonCatIso.hom = AddCommMonCat.ofHom e.toAddMonoidHom

@[simp]

theorem MulEquiv.toCommMonCatIso_inv {X Y : Type u} [CommMonoid X] [CommMonoid Y] (e : X ≃* Y) : e.toCommMonCatIso.inv = CommMonCat.ofHom e.symm.toMonoidHom

@[simp]

theorem AddEquiv.toAddCommMonCatIso_inv {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] (e : X ≃+ Y) : e.toAddCommMonCatIso.inv = AddCommMonCat.ofHom e.symm.toAddMonoidHom

@[simp]

theorem MulEquiv.toCommMonCatIso_hom {X Y : Type u} [CommMonoid X] [CommMonoid Y] (e : X ≃* Y) : e.toCommMonCatIso.hom = CommMonCat.ofHom e.toMonoidHom

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

Build a MulEquiv from an isomorphism in the category MonCat.

Equations

• i.monCatIsoToMulEquiv = (MonCat.Hom.hom i.hom).toMulEquiv (MonCat.Hom.hom i.inv) ⋯ ⋯

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

Build an AddEquiv from an isomorphism in the category AddMonCat.

Equations

• i.addMonCatIsoToAddEquiv = (AddMonCat.Hom.hom i.hom).toAddEquiv (AddMonCat.Hom.hom i.inv) ⋯ ⋯

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

Build a MulEquiv from an isomorphism in the category CommMonCat.

Equations

• i.commMonCatIsoToMulEquiv = (CommMonCat.Hom.hom i.hom).toMulEquiv (CommMonCat.Hom.hom i.inv) ⋯ ⋯

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

Build an AddEquiv from an isomorphism in the category AddCommMonCat.

Equations

• i.commMonCatIsoToAddEquiv = (AddCommMonCat.Hom.hom i.hom).toAddEquiv (AddCommMonCat.Hom.hom i.inv) ⋯ ⋯

def mulEquivIsoMonCatIso {X Y : Type u} [Monoid X] [Monoid Y] : X ≃* Y ≅ ↧X ≅ ↧Y

multiplicative equivalences between Monoids are the same as (isomorphic to) isomorphisms in MonCat

Equations

• mulEquivIsoMonCatIso = { hom := TypeCat.ofHom fun (e : X ≃* Y) => e.toMonCatIso, inv := TypeCat.ofHom fun (i : ↧X ≅ ↧Y) => i.monCatIsoToMulEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def addEquivIsoAddMonCatIso {X Y : Type u} [AddMonoid X] [AddMonoid Y] : X ≃+ Y ≅ ↧X ≅ ↧Y

additive equivalences between AddMonoids are the same as (isomorphic to) isomorphisms in AddMonCat

Equations

• addEquivIsoAddMonCatIso = { hom := TypeCat.ofHom fun (e : X ≃+ Y) => e.toAddMonCatIso, inv := TypeCat.ofHom fun (i : ↧X ≅ ↧Y) => i.addMonCatIsoToAddEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def mulEquivIsoCommMonCatIso {X Y : Type u} [CommMonoid X] [CommMonoid Y] : X ≃* Y ≅ ↧X ≅ ↧Y

multiplicative equivalences between CommMonoids are the same as (isomorphic to) isomorphisms in CommMonCat

Equations

• mulEquivIsoCommMonCatIso = { hom := TypeCat.ofHom fun (e : X ≃* Y) => e.toCommMonCatIso, inv := TypeCat.ofHom fun (i : ↧X ≅ ↧Y) => i.commMonCatIsoToMulEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def addEquivIsoAddCommMonCatIso {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] : X ≃+ Y ≅ ↧X ≅ ↧Y

additive equivalences between AddCommMonoids are the same as (isomorphic to) isomorphisms in AddCommMonCat

Equations

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

instance MonCat.forget_reflects_isos : (CategoryTheory.forget MonCat).ReflectsIsomorphisms

instance AddMonCat.forget_reflects_isos : (CategoryTheory.forget AddMonCat).ReflectsIsomorphisms

instance CommMonCat.forget_reflects_isos : (CategoryTheory.forget CommMonCat).ReflectsIsomorphisms

instance AddCommMonCat.forget_reflects_isos : (CategoryTheory.forget AddCommMonCat).ReflectsIsomorphisms

instance CommMonCat.forget₂_full : (CategoryTheory.forget₂ CommMonCat MonCat).Full

Ensure that forget₂ CommMonCat MonCat automatically reflects isomorphisms.

instance AddCommMonCat.forget₂_full : (CategoryTheory.forget₂ AddCommMonCat AddMonCat).Full

Ensure that forget₂ AddCommMonCat AddMonCat automatically reflects isomorphisms.

@[simp] lemmas for MonoidHom.comp and categorical identities.

def AddMonCat.equivalence : AddMonCat ≌ MonCat

The equivalence between AddMonCat and MonCat.

Equations

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

@[simp]

theorem AddMonCat.equivalence_unitIso : equivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id AddMonCat)

@[simp]

theorem AddMonCat.equivalence_functor_obj_coe (X : AddMonCat) : ↑(equivalence.functor.obj X) = Multiplicative ↑X

@[simp]

theorem AddMonCat.equivalence_inverse_obj_coe (X : MonCat) : ↑(equivalence.inverse.obj X) = Additive ↑X

@[simp]

theorem AddMonCat.equivalence_inverse_map {X✝ Y✝ : MonCat} (f : X✝ ⟶ Y✝) : equivalence.inverse.map f = ofHom (MonoidHom.toAdditive (MonCat.Hom.hom f))

@[simp]

theorem AddMonCat.equivalence_functor_map {X✝ Y✝ : AddMonCat} (f : X✝ ⟶ Y✝) : equivalence.functor.map f = MonCat.ofHom (AddMonoidHom.toMultiplicative (Hom.hom f))

@[simp]

theorem AddMonCat.equivalence_counitIso : equivalence.counitIso = CategoryTheory.Iso.refl ({ obj := fun (X : MonCat) => ↧(Additive ↑X), map := fun {X Y : MonCat} (f : X ⟶ Y) => ofHom (MonoidHom.toAdditive (MonCat.Hom.hom f)), map_id := equivalence._proof_3, map_comp := @equivalence._proof_4 }.comp { obj := fun (X : AddMonCat) => ↧(Multiplicative ↑X), map := fun {X Y : AddMonCat} (f : X ⟶ Y) => MonCat.ofHom (AddMonoidHom.toMultiplicative (Hom.hom f)), map_id := equivalence._proof_1, map_comp := @equivalence._proof_2 })

def AddCommMonCat.equivalence : AddCommMonCat ≌ CommMonCat

The equivalence between AddCommMonCat and CommMonCat.

Equations

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

@[simp]

theorem AddCommMonCat.equivalence_inverse_obj_coe (X : CommMonCat) : ↑(equivalence.inverse.obj X) = Additive ↑X

@[simp]

theorem AddCommMonCat.equivalence_functor_map {X✝ Y✝ : AddCommMonCat} (f : X✝ ⟶ Y✝) : equivalence.functor.map f = CommMonCat.ofHom (AddMonoidHom.toMultiplicative (Hom.hom f))

@[simp]

theorem AddCommMonCat.equivalence_counitIso : equivalence.counitIso = CategoryTheory.Iso.refl ({ obj := fun (X : CommMonCat) => ↧(Additive ↑X), map := fun {X Y : CommMonCat} (f : X ⟶ Y) => ofHom (MonoidHom.toAdditive (CommMonCat.Hom.hom f)), map_id := equivalence._proof_3, map_comp := @equivalence._proof_4 }.comp { obj := fun (X : AddCommMonCat) => ↧(Multiplicative ↑X), map := fun {X Y : AddCommMonCat} (f : X ⟶ Y) => CommMonCat.ofHom (AddMonoidHom.toMultiplicative (Hom.hom f)), map_id := equivalence._proof_1, map_comp := @equivalence._proof_2 })

@[simp]

theorem AddCommMonCat.equivalence_unitIso : equivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id AddCommMonCat)

@[simp]

theorem AddCommMonCat.equivalence_functor_obj_coe (X : AddCommMonCat) : ↑(equivalence.functor.obj X) = Multiplicative ↑X

@[simp]

theorem AddCommMonCat.equivalence_inverse_map {X✝ Y✝ : CommMonCat} (f : X✝ ⟶ Y✝) : equivalence.inverse.map f = ofHom (MonoidHom.toAdditive (CommMonCat.Hom.hom f))