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

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 groups and group morphisms.

• carrier : Type u

  The underlying type.

• str : AddMonoid self.carrier

structure MonCat : Type (u + 1)

The category of groups and group morphisms.

• carrier : Type u

  The underlying type.

• str : Monoid self.carrier

def MonCat.instCoeSortType : CoeSort MonCat (Type u)

Equations

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

def AddMonCat.instCoeSortType : CoeSort AddMonCat (Type u)

Equations

• Eq 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

• Eq (MonCat.of 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

• Eq (AddMonCat.of M) { carrier := M, str := inst✝ }

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

The type of morphisms in AddMonCat R.

• hom' : AddMonoidHom A.carrier B.carrier

  The underlying monoid homomorphism.

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

theorem AddMonCat.Hom.ext_iff {A B : AddMonCat} {x y : A.Hom B} : Iff (Eq x y) (Eq x.hom' y.hom')

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

The type of morphisms in MonCat R.

• hom' : MonoidHom A.carrier B.carrier

  The underlying monoid homomorphism.

theorem MonCat.Hom.ext_iff {A B : MonCat} {x y : A.Hom B} : Iff (Eq x y) (Eq x.hom' y.hom')

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

def MonCat.instCategory : CategoryTheory.Category MonCat

Equations

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

def AddMonCat.instCategory : CategoryTheory.Category AddMonCat

Equations

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

def MonCat.instConcreteCategoryMonoidHomCarrier : CategoryTheory.ConcreteCategory MonCat fun (x1 x2 : MonCat) => MonoidHom x1.carrier x2.carrier

Equations

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

def AddMonCat.instConcreteCategoryAddMonoidHomCarrier : CategoryTheory.ConcreteCategory AddMonCat fun (x1 x2 : AddMonCat) => AddMonoidHom x1.carrier x2.carrier

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) : MonoidHom X.carrier Y.carrier

Turn a morphism in MonCat back into a MonoidHom.

Equations

• Eq f.hom (CategoryTheory.ConcreteCategory.hom f)

@[reducible, inline]

abbrev AddMonCat.Hom.hom {X Y : AddMonCat} (f : X.Hom Y) : AddMonoidHom X.carrier Y.carrier

Turn a morphism in AddMonCat back into an AddMonoidHom.

Equations

• Eq f.hom (CategoryTheory.ConcreteCategory.hom f)

@[reducible, inline]

abbrev MonCat.ofHom {X Y : Type u} [Monoid X] [Monoid Y] (f : MonoidHom X Y) : Quiver.Hom (of X) (of Y)

Typecheck a MonoidHom as a morphism in MonCat.

Equations

• Eq (MonCat.ofHom f) (CategoryTheory.ConcreteCategory.ofHom f)

@[reducible, inline]

abbrev AddMonCat.ofHom {X Y : Type u} [AddMonoid X] [AddMonoid Y] (f : AddMonoidHom X Y) : Quiver.Hom (of X) (of Y)

Typecheck an AddMonoidHom as a morphism in AddMonCat.

Equations

• Eq (AddMonCat.ofHom f) (CategoryTheory.ConcreteCategory.ofHom f)

def MonCat.Hom.Simps.hom (X Y : MonCat) (f : X.Hom Y) : MonoidHom X.carrier Y.carrier

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

Equations

• Eq (MonCat.Hom.Simps.hom X Y f) f.hom

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

theorem MonCat.coe_id {X : MonCat} : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X))) id

theorem AddMonCat.coe_id {X : AddMonCat} : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X))) id

theorem MonCat.coe_comp {X Y Z : MonCat} {f : Quiver.Hom X Y} {g : Quiver.Hom Y Z} : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g))) (Function.comp (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g)) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f)))

theorem AddMonCat.coe_comp {X Y Z : AddMonCat} {f : Quiver.Hom X Y} {g : Quiver.Hom Y Z} : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g))) (Function.comp (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g)) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f)))

theorem MonCat.forget_map {X Y : MonCat} (f : Quiver.Hom X Y) : Eq ((CategoryTheory.forget MonCat).map f) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f))

theorem AddMonCat.forget_map {X Y : AddMonCat} (f : Quiver.Hom X Y) : Eq ((CategoryTheory.forget AddMonCat).map f) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f))

theorem MonCat.ext {X Y : MonCat} {f g : Quiver.Hom X Y} (w : ∀ (x : X.carrier), Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) x) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g) x)) : Eq f g

theorem AddMonCat.ext {X Y : AddMonCat} {f g : Quiver.Hom X Y} (w : ∀ (x : X.carrier), Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) x) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g) x)) : Eq f g

theorem AddMonCat.ext_iff {X Y : AddMonCat} {f g : Quiver.Hom X Y} : Iff (Eq f g) (∀ (x : X.carrier), Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) x) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g) x))

theorem MonCat.ext_iff {X Y : MonCat} {f g : Quiver.Hom X Y} : Iff (Eq f g) (∀ (x : X.carrier), Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) x) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g) x))

theorem MonCat.coe_of (M : Type u) [Monoid M] : Eq (of M).carrier M

theorem AddMonCat.coe_of (M : Type u) [AddMonoid M] : Eq (of M).carrier M

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

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

theorem MonCat.id_apply (M : MonCat) (x : M.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x) x

theorem AddMonCat.id_apply (M : AddMonCat) (x : M.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x) x

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

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

theorem MonCat.comp_apply {M N T : MonCat} (f : Quiver.Hom M N) (g : Quiver.Hom N T) (x : M.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) x))

theorem AddMonCat.comp_apply {M N T : AddMonCat} (f : Quiver.Hom M N) (g : Quiver.Hom N T) (x : M.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) x))

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

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

theorem MonCat.hom_ext_iff {M N : MonCat} {f g : Quiver.Hom M N} : Iff (Eq f g) (Eq (Hom.hom f) (Hom.hom g))

theorem AddMonCat.hom_ext_iff {M N : AddMonCat} {f g : Quiver.Hom M N} : Iff (Eq f g) (Eq (Hom.hom f) (Hom.hom g))

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

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

theorem MonCat.ofHom_hom {M N : MonCat} (f : Quiver.Hom M N) : Eq (ofHom (Hom.hom f)) f

theorem AddMonCat.ofHom_hom {M N : AddMonCat} (f : Quiver.Hom M N) : Eq (ofHom (Hom.hom f)) f

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

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

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

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

theorem MonCat.ofHom_apply {X Y : Type u} [Monoid X] [Monoid Y] (f : MonoidHom X Y) (x : X) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (ofHom f)) x) (DFunLike.coe f x)

theorem AddMonCat.ofHom_apply {X Y : Type u} [AddMonoid X] [AddMonoid Y] (f : AddMonoidHom X Y) (x : X) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (ofHom f)) x) (DFunLike.coe f x)

theorem MonCat.inv_hom_apply {M N : MonCat} (e : CategoryTheory.Iso M N) (x : M.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.inv) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.hom) x)) x

theorem AddMonCat.neg_hom_apply {M N : AddMonCat} (e : CategoryTheory.Iso M N) (x : M.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.inv) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.hom) x)) x

theorem MonCat.hom_inv_apply {M N : MonCat} (e : CategoryTheory.Iso M N) (s : N.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.hom) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.inv) s)) s

theorem AddMonCat.hom_neg_apply {M N : AddMonCat} (e : CategoryTheory.Iso M N) (s : N.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.hom) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.inv) s)) s

def MonCat.instInhabited : Inhabited MonCat

Equations

• Eq MonCat.instInhabited { default := MonCat.of PUnit }

def AddMonCat.instInhabited : Inhabited AddMonCat

Equations

• Eq AddMonCat.instInhabited { default := AddMonCat.of PUnit }

def MonCat.instOneHom (X Y : MonCat) : One (Quiver.Hom X Y)

Equations

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

def AddMonCat.instZeroHom (X Y : AddMonCat) : Zero (Quiver.Hom X Y)

Equations

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

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

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

theorem MonCat.oneHom_apply (X Y : MonCat) (x : X.carrier) : Eq (DFunLike.coe (Hom.hom 1) x) 1

theorem AddMonCat.zeroHom_apply (X Y : AddMonCat) (x : X.carrier) : Eq (DFunLike.coe (Hom.hom 0) x) 0

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

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

theorem MonCat.mul_of {A : Type u_1} [Monoid A] (a b : A) : Eq (HMul.hMul a b) (HMul.hMul a b)

theorem AddMonCat.add_of {A : Type u_1} [AddMonoid A] (a b : A) : Eq (HAdd.hAdd a b) (HAdd.hAdd 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.

theorem AddMonCat.uliftFunctor_obj_coe (X : AddMonCat) : Eq (uliftFunctor.obj X).carrier (ULift X.carrier)

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

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

theorem MonCat.uliftFunctor_obj_coe (X : MonCat) : Eq (uliftFunctor.obj X).carrier (ULift X.carrier)

structure AddCommMonCat : Type (u + 1)

The category of additive groups and group morphisms.

• carrier : Type u

  The underlying type.

• str : AddCommMonoid self.carrier

structure CommMonCat : Type (u + 1)

The category of groups and group morphisms.

• carrier : Type u

  The underlying type.

• str : CommMonoid self.carrier

def CommMonCat.instCoeSortType : CoeSort CommMonCat (Type u)

Equations

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

def AddCommMonCat.instCoeSortType : CoeSort AddCommMonCat (Type u)

Equations

• Eq 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

• Eq (CommMonCat.of 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

• Eq (AddCommMonCat.of M) { carrier := M, str := inst✝ }

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

The type of morphisms in AddCommMonCat R.

• hom' : AddMonoidHom A.carrier B.carrier

  The underlying monoid homomorphism.

theorem AddCommMonCat.Hom.ext_iff {A B : AddCommMonCat} {x y : A.Hom B} : Iff (Eq x y) (Eq x.hom' y.hom')

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

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

The type of morphisms in CommMonCat R.

• hom' : MonoidHom A.carrier B.carrier

  The underlying monoid homomorphism.

theorem CommMonCat.Hom.ext_iff {A B : CommMonCat} {x y : A.Hom B} : Iff (Eq x y) (Eq x.hom' y.hom')

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

def CommMonCat.instCategory : CategoryTheory.Category CommMonCat

Equations

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

def AddCommMonCat.instCategory : CategoryTheory.Category AddCommMonCat

Equations

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

def CommMonCat.instConcreteCategoryMonoidHomCarrier : CategoryTheory.ConcreteCategory CommMonCat fun (x1 x2 : CommMonCat) => MonoidHom x1.carrier x2.carrier

Equations

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

def AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier : CategoryTheory.ConcreteCategory AddCommMonCat fun (x1 x2 : AddCommMonCat) => AddMonoidHom x1.carrier x2.carrier

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) : MonoidHom X.carrier Y.carrier

Turn a morphism in CommMonCat back into a MonoidHom.

Equations

• Eq f.hom (CategoryTheory.ConcreteCategory.hom f)

@[reducible, inline]

abbrev AddCommMonCat.Hom.hom {X Y : AddCommMonCat} (f : X.Hom Y) : AddMonoidHom X.carrier Y.carrier

Turn a morphism in AddCommMonCat back into an AddMonoidHom.

Equations

• Eq f.hom (CategoryTheory.ConcreteCategory.hom f)

@[reducible, inline]

abbrev CommMonCat.ofHom {X Y : Type u} [CommMonoid X] [CommMonoid Y] (f : MonoidHom X Y) : Quiver.Hom (of X) (of Y)

Typecheck a MonoidHom as a morphism in CommMonCat.

Equations

• Eq (CommMonCat.ofHom f) (CategoryTheory.ConcreteCategory.ofHom f)

@[reducible, inline]

abbrev AddCommMonCat.ofHom {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] (f : AddMonoidHom X Y) : Quiver.Hom (of X) (of Y)

Typecheck an AddMonoidHom as a morphism in AddCommMonCat.

Equations

• Eq (AddCommMonCat.ofHom f) (CategoryTheory.ConcreteCategory.ofHom f)

def CommMonCat.Hom.Simps.hom (X Y : CommMonCat) (f : X.Hom Y) : MonoidHom X.carrier Y.carrier

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

Equations

• Eq (CommMonCat.Hom.Simps.hom X Y f) f.hom

def AddCommMonCat.Hom.Simps.hom (X Y : AddCommMonCat) (f : X.Hom Y) : AddMonoidHom X.carrier Y.carrier

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

Equations

• Eq (AddCommMonCat.Hom.Simps.hom X Y f) f.hom

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

theorem CommMonCat.coe_id {X : CommMonCat} : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X))) id

theorem AddCommMonCat.coe_id {X : AddCommMonCat} : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X))) id

theorem CommMonCat.coe_comp {X Y Z : CommMonCat} {f : Quiver.Hom X Y} {g : Quiver.Hom Y Z} : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g))) (Function.comp (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g)) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f)))

theorem AddCommMonCat.coe_comp {X Y Z : AddCommMonCat} {f : Quiver.Hom X Y} {g : Quiver.Hom Y Z} : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g))) (Function.comp (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g)) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f)))

theorem CommMonCat.forget_map {X Y : CommMonCat} (f : Quiver.Hom X Y) : Eq ((CategoryTheory.forget CommMonCat).map f) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f))

theorem AddCommMonCat.forget_map {X Y : AddCommMonCat} (f : Quiver.Hom X Y) : Eq ((CategoryTheory.forget AddCommMonCat).map f) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f))

theorem CommMonCat.ext {X Y : CommMonCat} {f g : Quiver.Hom X Y} (w : ∀ (x : X.carrier), Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) x) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g) x)) : Eq f g

theorem AddCommMonCat.ext {X Y : AddCommMonCat} {f g : Quiver.Hom X Y} (w : ∀ (x : X.carrier), Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) x) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g) x)) : Eq f g

theorem AddCommMonCat.ext_iff {X Y : AddCommMonCat} {f g : Quiver.Hom X Y} : Iff (Eq f g) (∀ (x : X.carrier), Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) x) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g) x))

theorem CommMonCat.ext_iff {X Y : CommMonCat} {f g : Quiver.Hom X Y} : Iff (Eq f g) (∀ (x : X.carrier), Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) x) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g) x))

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

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

theorem CommMonCat.id_apply (M : CommMonCat) (x : M.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x) x

theorem AddCommMonCat.id_apply (M : AddCommMonCat) (x : M.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x) x

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

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

theorem CommMonCat.comp_apply {M N T : CommMonCat} (f : Quiver.Hom M N) (g : Quiver.Hom N T) (x : M.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) x))

theorem AddCommMonCat.comp_apply {M N T : AddCommMonCat} (f : Quiver.Hom M N) (g : Quiver.Hom N T) (x : M.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) x))

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

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

theorem CommMonCat.hom_ext_iff {M N : CommMonCat} {f g : Quiver.Hom M N} : Iff (Eq f g) (Eq (Hom.hom f) (Hom.hom g))

theorem AddCommMonCat.hom_ext_iff {M N : AddCommMonCat} {f g : Quiver.Hom M N} : Iff (Eq f g) (Eq (Hom.hom f) (Hom.hom g))

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

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

theorem CommMonCat.ofHom_hom {M N : CommMonCat} (f : Quiver.Hom M N) : Eq (ofHom (Hom.hom f)) f

theorem AddCommMonCat.ofHom_hom {M N : AddCommMonCat} (f : Quiver.Hom M N) : Eq (ofHom (Hom.hom f)) f

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

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

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

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

theorem CommMonCat.ofHom_apply {X Y : Type u} [CommMonoid X] [CommMonoid Y] (f : MonoidHom X Y) (x : X) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (ofHom f)) x) (DFunLike.coe f x)

theorem AddCommMonCat.ofHom_apply {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] (f : AddMonoidHom X Y) (x : X) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (ofHom f)) x) (DFunLike.coe f x)

theorem CommMonCat.inv_hom_apply {M N : CommMonCat} (e : CategoryTheory.Iso M N) (x : M.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.inv) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.hom) x)) x

theorem AddCommMonCat.neg_hom_apply {M N : AddCommMonCat} (e : CategoryTheory.Iso M N) (x : M.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.inv) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.hom) x)) x

theorem CommMonCat.hom_inv_apply {M N : CommMonCat} (e : CategoryTheory.Iso M N) (s : N.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.hom) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.inv) s)) s

theorem AddCommMonCat.hom_neg_apply {M N : AddCommMonCat} (e : CategoryTheory.Iso M N) (s : N.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.hom) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom e.inv) s)) s

def CommMonCat.instInhabited : Inhabited CommMonCat

Equations

• Eq CommMonCat.instInhabited { default := CommMonCat.of PUnit }

def AddCommMonCat.instInhabited : Inhabited AddCommMonCat

Equations

• Eq AddCommMonCat.instInhabited { default := AddCommMonCat.of PUnit }

theorem CommMonCat.coe_of (R : Type u) [CommMonoid R] : Eq (of R).carrier R

theorem AddCommMonCat.coe_of (R : Type u) [AddCommMonoid R] : Eq (of R).carrier R

def CommMonCat.hasForgetToMonCat : CategoryTheory.HasForget₂ CommMonCat MonCat

Equations

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

def AddCommMonCat.hasForgetToAddMonCat : CategoryTheory.HasForget₂ AddCommMonCat AddMonCat

Equations

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

theorem CommMonCat.coe_forget₂_obj (X : CommMonCat) : Eq ((CategoryTheory.forget₂ CommMonCat MonCat).obj X).carrier X.carrier

theorem AddCommMonCat.coe_forget₂_obj (X : AddCommMonCat) : Eq ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).obj X).carrier X.carrier

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

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

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

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

def CommMonCat.instCoeMonCat : Coe CommMonCat MonCat

Equations

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

def AddCommMonCat.instCoeMonCat : Coe AddCommMonCat AddMonCat

Equations

• Eq 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.

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

theorem AddCommMonCat.uliftFunctor_obj_coe (X : AddCommMonCat) : Eq (uliftFunctor.obj X).carrier (ULift X.carrier)

theorem CommMonCat.uliftFunctor_obj_coe (X : CommMonCat) : Eq (uliftFunctor.obj X).carrier (ULift X.carrier)

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

def MulEquiv.toMonCatIso {X Y : Type u} [Monoid X] [Monoid Y] (e : MulEquiv X Y) : CategoryTheory.Iso (MonCat.of X) (MonCat.of Y)

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

Equations

• Eq 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 : AddEquiv X Y) : CategoryTheory.Iso (AddMonCat.of X) (AddMonCat.of Y)

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

Equations

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

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

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

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

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

def MulEquiv.toCommMonCatIso {X Y : Type u} [CommMonoid X] [CommMonoid Y] (e : MulEquiv X Y) : CategoryTheory.Iso (CommMonCat.of X) (CommMonCat.of Y)

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

Equations

• Eq 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 : AddEquiv X Y) : CategoryTheory.Iso (AddCommMonCat.of X) (AddCommMonCat.of Y)

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

Equations

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

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

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

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

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

def CategoryTheory.Iso.monCatIsoToMulEquiv {X Y : MonCat} (i : Iso X Y) : MulEquiv X.carrier Y.carrier

Build a MulEquiv from an isomorphism in the category MonCat.

Equations

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

def CategoryTheory.Iso.addMonCatIsoToAddEquiv {X Y : AddMonCat} (i : Iso X Y) : AddEquiv X.carrier Y.carrier

Build an AddEquiv from an isomorphism in the category AddMonCat.

Equations

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

def CategoryTheory.Iso.commMonCatIsoToMulEquiv {X Y : CommMonCat} (i : Iso X Y) : MulEquiv X.carrier Y.carrier

Build a MulEquiv from an isomorphism in the category CommMonCat.

Equations

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

def CategoryTheory.Iso.commMonCatIsoToAddEquiv {X Y : AddCommMonCat} (i : Iso X Y) : AddEquiv X.carrier Y.carrier

Build an AddEquiv from an isomorphism in the category AddCommMonCat.

Equations

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

def mulEquivIsoMonCatIso {X Y : Type u} [Monoid X] [Monoid Y] : CategoryTheory.Iso (MulEquiv X Y) (CategoryTheory.Iso (MonCat.of X) (MonCat.of Y))

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

Equations

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

def addEquivIsoAddMonCatIso {X Y : Type u} [AddMonoid X] [AddMonoid Y] : CategoryTheory.Iso (AddEquiv X Y) (CategoryTheory.Iso (AddMonCat.of X) (AddMonCat.of Y))

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

Equations

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

def mulEquivIsoCommMonCatIso {X Y : Type u} [CommMonoid X] [CommMonoid Y] : CategoryTheory.Iso (MulEquiv X Y) (CategoryTheory.Iso (CommMonCat.of X) (CommMonCat.of Y))

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

Equations

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

def addEquivIsoAddCommMonCatIso {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] : CategoryTheory.Iso (AddEquiv X Y) (CategoryTheory.Iso (AddCommMonCat.of X) (AddCommMonCat.of 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.

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

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

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

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

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

Ensure that forget₂ CommMonCat MonCat automatically reflects isomorphisms. We could have used CategoryTheory.HasForget.ReflectsIso alternatively.

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

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

@[deprecated "Proven by `simp only [MonCat.hom_id, comp_id]`" (since := "2025-01-28")]

theorem MonoidHom.comp_id_monCat {G : MonCat} {H : Type u} [Monoid H] (f : MonoidHom G.carrier H) : Eq (f.comp (MonCat.Hom.hom (CategoryTheory.CategoryStruct.id G))) f

@[deprecated "Proven by `simp only [MonCat.hom_id, comp_id]`" (since := "2025-01-28")]

theorem AddMonoidHom.comp_id_monCat {G : AddMonCat} {H : Type u} [AddMonoid H] (f : AddMonoidHom G.carrier H) : Eq (f.comp (AddMonCat.Hom.hom (CategoryTheory.CategoryStruct.id G))) f

@[deprecated "Proven by `simp only [MonCat.hom_id, id_comp]`" (since := "2025-01-28")]

theorem MonoidHom.id_monCat_comp {G : Type u} [Monoid G] {H : MonCat} (f : MonoidHom G H.carrier) : Eq ((MonCat.Hom.hom (CategoryTheory.CategoryStruct.id H)).comp f) f

@[deprecated "Proven by `simp only [MonCat.hom_id, id_comp]`" (since := "2025-01-28")]

theorem AddMonoidHom.id_monCat_comp {G : Type u} [AddMonoid G] {H : AddMonCat} (f : AddMonoidHom G H.carrier) : Eq ((AddMonCat.Hom.hom (CategoryTheory.CategoryStruct.id H)).comp f) f

@[deprecated "Proven by `simp only [CommMonCat.hom_id, comp_id]`" (since := "2025-01-28")]

theorem MonoidHom.comp_id_commMonCat {G : CommMonCat} {H : Type u} [CommMonoid H] (f : MonoidHom G.carrier H) : Eq (f.comp (CommMonCat.Hom.hom (CategoryTheory.CategoryStruct.id G))) f

@[deprecated "Proven by `simp only [CommMonCat.hom_id, comp_id]`" (since := "2025-01-28")]

theorem AddMonoidHom.comp_id_commMonCat {G : AddCommMonCat} {H : Type u} [AddCommMonoid H] (f : AddMonoidHom G.carrier H) : Eq (f.comp (AddCommMonCat.Hom.hom (CategoryTheory.CategoryStruct.id G))) f

@[deprecated "Proven by `simp only [CommMonCat.hom_id, id_comp]`" (since := "2025-01-28")]

theorem MonoidHom.id_commMonCat_comp {G : Type u} [CommMonoid G] {H : CommMonCat} (f : MonoidHom G H.carrier) : Eq ((CommMonCat.Hom.hom (CategoryTheory.CategoryStruct.id H)).comp f) f

@[deprecated "Proven by `simp only [CommMonCat.hom_id, id_comp]`" (since := "2025-01-28")]

theorem AddMonoidHom.id_commMonCat_comp {G : Type u} [AddCommMonoid G] {H : AddCommMonCat} (f : AddMonoidHom G H.carrier) : Eq ((AddCommMonCat.Hom.hom (CategoryTheory.CategoryStruct.id H)).comp f) f

def AddMonCat.equivalence : CategoryTheory.Equivalence AddMonCat MonCat

The equivalence between AddMonCat and MonCat.

Equations

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

theorem AddMonCat.equivalence_functor_map {X✝ Y✝ : AddMonCat} (f : Quiver.Hom X✝ Y✝) : Eq (equivalence.functor.map f) (MonCat.ofHom (DFunLike.coe AddMonoidHom.toMultiplicative (Hom.hom f)))

theorem AddMonCat.equivalence_inverse_obj_coe (X : MonCat) : Eq (equivalence.inverse.obj X).carrier (Additive X.carrier)

theorem AddMonCat.equivalence_counitIso : Eq equivalence.counitIso (CategoryTheory.Iso.refl ({ obj := fun (X : MonCat) => of (Additive X.carrier), map := fun {X Y : MonCat} (f : Quiver.Hom X Y) => ofHom (DFunLike.coe MonoidHom.toAdditive (MonCat.Hom.hom f)), map_id := equivalence._proof_69, map_comp := @equivalence._proof_70 }.comp { obj := fun (X : AddMonCat) => MonCat.of (Multiplicative X.carrier), map := fun {X Y : AddMonCat} (f : Quiver.Hom X Y) => MonCat.ofHom (DFunLike.coe AddMonoidHom.toMultiplicative (Hom.hom f)), map_id := equivalence._proof_67, map_comp := @equivalence._proof_68 }))

theorem AddMonCat.equivalence_inverse_map {X✝ Y✝ : MonCat} (f : Quiver.Hom X✝ Y✝) : Eq (equivalence.inverse.map f) (ofHom (DFunLike.coe MonoidHom.toAdditive (MonCat.Hom.hom f)))

theorem AddMonCat.equivalence_functor_obj_coe (X : AddMonCat) : Eq (equivalence.functor.obj X).carrier (Multiplicative X.carrier)

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

def AddCommMonCat.equivalence : CategoryTheory.Equivalence AddCommMonCat CommMonCat

The equivalence between AddCommMonCat and CommMonCat.

Equations

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

theorem AddCommMonCat.equivalence_inverse_map {X✝ Y✝ : CommMonCat} (f : Quiver.Hom X✝ Y✝) : Eq (equivalence.inverse.map f) (ofHom (DFunLike.coe MonoidHom.toAdditive (CommMonCat.Hom.hom f)))

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

theorem AddCommMonCat.equivalence_functor_obj_coe (X : AddCommMonCat) : Eq (equivalence.functor.obj X).carrier (Multiplicative X.carrier)

theorem AddCommMonCat.equivalence_inverse_obj_coe (X : CommMonCat) : Eq (equivalence.inverse.obj X).carrier (Additive X.carrier)

theorem AddCommMonCat.equivalence_functor_map {X✝ Y✝ : AddCommMonCat} (f : Quiver.Hom X✝ Y✝) : Eq (equivalence.functor.map f) (CommMonCat.ofHom (DFunLike.coe AddMonoidHom.toMultiplicative (Hom.hom f)))

theorem AddCommMonCat.equivalence_counitIso : Eq equivalence.counitIso (CategoryTheory.Iso.refl ({ obj := fun (X : CommMonCat) => of (Additive X.carrier), map := fun {X Y : CommMonCat} (f : Quiver.Hom X Y) => ofHom (DFunLike.coe MonoidHom.toAdditive (CommMonCat.Hom.hom f)), map_id := equivalence._proof_74, map_comp := @equivalence._proof_75 }.comp { obj := fun (X : AddCommMonCat) => CommMonCat.of (Multiplicative X.carrier), map := fun {X Y : AddCommMonCat} (f : Quiver.Hom X Y) => CommMonCat.ofHom (DFunLike.coe AddMonoidHom.toMultiplicative (Hom.hom f)), map_id := equivalence._proof_72, map_comp := @equivalence._proof_73 }))