Category instances for monoid, add_monoid, comm_monoid, and add_comm_monoid.

We introduce the bundled categories:

• MonCat
• AddMonCat
• CommMonCat
• AddCommMonCat along with the relevant forgetful functors between them.

def AddMonCat : Type (u + 1)

The category of additive monoids and monoid morphisms.

def MonCat : Type (u + 1)

The category of monoids and monoid morphisms.

abbrev AddMonCat.AssocAddMonoidHom (M : Type u_1) (N : Type u_2) [AddMonoid M] [AddMonoid N] : Type (max u_2 u_1)

AddMonoidHom doesn't actually assume associativity. This alias is needed to make the category theory machinery work.

@[inline, reducible]

abbrev MonCat.AssocMonoidHom (M : Type u_1) (N : Type u_2) [Monoid M] [Monoid N] : Type (max u_2 u_1)

MonoidHom doesn't actually assume associativity. This alias is needed to make the category theory machinery work.

theorem AddMonCat.bundledHom.proof_2 {α : Type u_1} (I : AddMonoid α) : (fun {X Y} x x_1 f => ↑f) I I ((fun {α} x => AddMonoidHom.id α) I) = id

theorem AddMonCat.bundledHom.proof_3 {α : Type u_1} {β : Type u_1} {γ : Type u_1} (Iα : AddMonoid α) (Iβ : AddMonoid β) (Iγ : AddMonoid γ) (f : AddMonCat.AssocAddMonoidHom α β) (g : AddMonCat.AssocAddMonoidHom β γ) : ↑g ∘ ↑f = ↑g ∘ ↑f

theorem AddMonCat.bundledHom.proof_1 {α : Type u_1} {β : Type u_1} (Iα : AddMonoid α) (Iβ : AddMonoid β) ⦃a₁ : AddMonCat.AssocAddMonoidHom α β⦄ ⦃a₂ : AddMonCat.AssocAddMonoidHom α β⦄ (a : (fun {X Y} x x_1 f => ↑f) Iα Iβ a₁ = (fun {X Y} x x_1 f => ↑f) Iα Iβ a₂) : a₁ = a₂

instance AddMonCat.bundledHom : CategoryTheory.BundledHom AddMonCat.AssocAddMonoidHom

instance MonCat.bundledHom : CategoryTheory.BundledHom MonCat.AssocMonoidHom

instance instAddMonCatLargeCategory : CategoryTheory.LargeCategory AddMonCat

instance AddMonCat.concreteCategory : CategoryTheory.ConcreteCategory AddMonCat

instance MonCat.concreteCategory : CategoryTheory.ConcreteCategory MonCat

instance AddMonCat.instCoeSortMonCatType : CoeSort AddMonCat (Type u_1)

instance MonCat.instCoeSortMonCatType : CoeSort MonCat (Type u_1)

instance AddMonCat.instMonoidα (X : AddMonCat) : AddMonoid ↑X

instance MonCat.instMonoidα (X : MonCat) : Monoid ↑X

instance AddMonCat.instCoeFunHomMonCatToQuiverToCategoryStructInstMonCatLargeCategoryForAllαAddMonoid {X : AddMonCat} {Y : AddMonCat} : CoeFun (X ⟶ Y) fun x => ↑X → ↑Y

instance MonCat.instCoeFunHomMonCatToQuiverToCategoryStructInstMonCatLargeCategoryForAllαMonoid {X : MonCat} {Y : MonCat} : CoeFun (X ⟶ Y) fun x => ↑X → ↑Y

instance AddMonCat.Hom_FunLike (X : AddMonCat) (Y : AddMonCat) : FunLike (X ⟶ Y) ↑X fun x => ↑Y

instance MonCat.Hom_FunLike (X : MonCat) (Y : MonCat) : FunLike (X ⟶ Y) ↑X fun x => ↑Y

@[simp]

theorem AddMonCat.coe_id {X : AddMonCat} : ↑(CategoryTheory.CategoryStruct.id X) = id

@[simp]

theorem MonCat.coe_id {X : MonCat} : ↑(CategoryTheory.CategoryStruct.id X) = id

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Construct a bundled AddMonCat from the underlying type and typeclass.

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

Construct a bundled MonCat from the underlying type and typeclass.

theorem AddMonCat.coe_of (R : Type u) [AddMonoid R] : ↑(AddMonCat.of R) = R

theorem MonCat.coe_of (R : Type u) [Monoid R] : ↑(MonCat.of R) = R

instance AddMonCat.instInhabitedMonCat : Inhabited AddMonCat

instance MonCat.instInhabitedMonCat : Inhabited MonCat

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

Typecheck an AddMonoidHom as a morphism in AddMonCat.

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

Typecheck a MonoidHom as a morphism in MonCat.

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance AddMonCat.instGroupαAddMonoidOfToAddMonoidToSubNegAddMonoid {G : Type u_1} [AddGroup G] : AddGroup ↑(AddMonCat.of G)

instance MonCat.instGroupαMonoidOfToMonoidToDivInvMonoid {G : Type u_1} [Group G] : Group ↑(MonCat.of G)

def AddCommMonCat : Type (u + 1)

The category of additive commutative monoids and monoid morphisms.

def CommMonCat : Type (u + 1)

The category of commutative monoids and monoid morphisms.

theorem AddCommMonCat.instParentProjectionTypeAddMonoidAddCommMonoidToAddMonoid.proof_1 : CategoryTheory.BundledHom.ParentProjection @AddCommMonoid.toAddMonoid

instance AddCommMonCat.instParentProjectionTypeAddMonoidAddCommMonoidToAddMonoid : CategoryTheory.BundledHom.ParentProjection @AddCommMonoid.toAddMonoid

instance CommMonCat.instParentProjectionTypeMonoidCommMonoidToMonoid : CategoryTheory.BundledHom.ParentProjection @CommMonoid.toMonoid

instance instAddCommMonCatLargeCategory : CategoryTheory.LargeCategory AddCommMonCat

instance AddCommMonCat.concreteCategory : CategoryTheory.ConcreteCategory AddCommMonCat

instance CommMonCat.concreteCategory : CategoryTheory.ConcreteCategory CommMonCat

instance AddCommMonCat.instCoeSortCommMonCatType : CoeSort AddCommMonCat (Type u_1)

instance CommMonCat.instCoeSortCommMonCatType : CoeSort CommMonCat (Type u_1)

instance AddCommMonCat.instCommMonoidα (X : AddCommMonCat) : AddCommMonoid ↑X

instance CommMonCat.instCommMonoidα (X : CommMonCat) : CommMonoid ↑X

instance AddCommMonCat.instCoeFunHomCommMonCatToQuiverToCategoryStructInstCommMonCatLargeCategoryForAllαAddCommMonoid {X : AddCommMonCat} {Y : AddCommMonCat} : CoeFun (X ⟶ Y) fun x => ↑X → ↑Y

instance CommMonCat.instCoeFunHomCommMonCatToQuiverToCategoryStructInstCommMonCatLargeCategoryForAllαCommMonoid {X : CommMonCat} {Y : CommMonCat} : CoeFun (X ⟶ Y) fun x => ↑X → ↑Y

instance AddCommMonCat.Hom_FunLike (X : AddCommMonCat) (Y : AddCommMonCat) : FunLike (X ⟶ Y) ↑X fun x => ↑Y

instance CommMonCat.Hom_FunLike (X : CommMonCat) (Y : CommMonCat) : FunLike (X ⟶ Y) ↑X fun x => ↑Y

@[simp]

theorem AddCommMonCat.coe_id {X : AddCommMonCat} : ↑(CategoryTheory.CategoryStruct.id X) = id

@[simp]

theorem CommMonCat.coe_id {X : CommMonCat} : ↑(CategoryTheory.CategoryStruct.id X) = id

@[simp]

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

@[simp]

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

@[simp]

theorem AddCommMonCat.forget_map {X : AddCommMonCat} {Y : AddCommMonCat} (f : X ⟶ Y) : (CategoryTheory.forget AddCommMonCat).map f = ↑f

@[simp]

theorem CommMonCat.forget_map {X : CommMonCat} {Y : CommMonCat} (f : X ⟶ Y) : (CategoryTheory.forget CommMonCat).map f = ↑f

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

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

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

Construct a bundled AddCommMon from the underlying type and typeclass.

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

Construct a bundled CommMonCat from the underlying type and typeclass.

instance AddCommMonCat.instInhabitedCommMonCat : Inhabited AddCommMonCat

instance CommMonCat.instInhabitedCommMonCat : Inhabited CommMonCat

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

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

instance AddCommMonCat.hasForgetToAddMonCat : CategoryTheory.HasForget₂ AddCommMonCat AddMonCat

instance CommMonCat.hasForgetToMonCat : CategoryTheory.HasForget₂ CommMonCat MonCat

instance AddCommMonCat.instCoeCommMonCatMonCat : Coe AddCommMonCat AddMonCat

instance CommMonCat.instCoeCommMonCatMonCat : Coe CommMonCat MonCat

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

Typecheck an AddMonoidHom as a morphism in AddCommMonCat.

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

Typecheck a MonoidHom as a morphism in CommMonCat.

@[simp]

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

@[simp]

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

theorem AddEquiv.toAddMonCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [AddMonoid X] [AddMonoid Y] (e : X ≃+ Y) : CategoryTheory.CategoryStruct.comp (AddMonCat.ofHom (AddEquiv.toAddMonoidHom (AddEquiv.symm e))) (AddMonCat.ofHom (AddEquiv.toAddMonoidHom e)) = CategoryTheory.CategoryStruct.id (AddMonCat.of Y)

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

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

theorem AddEquiv.toAddMonCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [AddMonoid X] [AddMonoid Y] (e : X ≃+ Y) : CategoryTheory.CategoryStruct.comp (AddMonCat.ofHom (AddEquiv.toAddMonoidHom e)) (AddMonCat.ofHom (AddEquiv.toAddMonoidHom (AddEquiv.symm e))) = CategoryTheory.CategoryStruct.id (AddMonCat.of X)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem AddEquiv.toAddCommMonCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [AddCommMonoid X] [AddCommMonoid Y] (e : X ≃+ Y) : CategoryTheory.CategoryStruct.comp (AddCommMonCat.ofHom (AddEquiv.toAddMonoidHom (AddEquiv.symm e))) (AddCommMonCat.ofHom (AddEquiv.toAddMonoidHom e)) = CategoryTheory.CategoryStruct.id (AddCommMonCat.of Y)

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

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

theorem AddEquiv.toAddCommMonCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [AddCommMonoid X] [AddCommMonoid Y] (e : X ≃+ Y) : CategoryTheory.CategoryStruct.comp (AddCommMonCat.ofHom (AddEquiv.toAddMonoidHom e)) (AddCommMonCat.ofHom (AddEquiv.toAddMonoidHom (AddEquiv.symm e))) = CategoryTheory.CategoryStruct.id (AddCommMonCat.of X)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Build an AddEquiv from an isomorphism in the category AddMonCat.

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

Build a MulEquiv from an isomorphism in the category MonCat.

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

Build an AddEquiv from an isomorphism in the category AddCommMonCat.

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

Build a MulEquiv from an isomorphism in the category CommMonCat.

theorem addEquivIsoAddMonCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [AddMonoid X] [AddMonoid Y] : (CategoryTheory.CategoryStruct.comp (fun i => CategoryTheory.Iso.addMonCatIsoToAddEquiv i) fun e => AddEquiv.toAddMonCatIso e) = CategoryTheory.CategoryStruct.comp (fun i => CategoryTheory.Iso.addMonCatIsoToAddEquiv i) fun e => AddEquiv.toAddMonCatIso e

theorem addEquivIsoAddMonCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [AddMonoid X] [AddMonoid Y] : (CategoryTheory.CategoryStruct.comp (fun e => AddEquiv.toAddMonCatIso e) fun i => CategoryTheory.Iso.addMonCatIsoToAddEquiv i) = CategoryTheory.CategoryStruct.comp (fun e => AddEquiv.toAddMonCatIso e) fun i => CategoryTheory.Iso.addMonCatIsoToAddEquiv i

def addEquivIsoAddMonCatIso {X : Type u} {Y : Type u} [AddMonoid X] [AddMonoid Y] : X ≃+ Y ≅ AddMonCat.of X ≅ AddMonCat.of Y

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

def mulEquivIsoMonCatIso {X : Type u} {Y : Type u} [Monoid X] [Monoid Y] : X ≃* Y ≅ MonCat.of X ≅ MonCat.of Y

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

theorem addEquivIsoAddCommMonCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [AddCommMonoid X] [AddCommMonoid Y] : (CategoryTheory.CategoryStruct.comp (fun e => AddEquiv.toAddCommMonCatIso e) fun i => CategoryTheory.Iso.commMonCatIsoToAddEquiv i) = CategoryTheory.CategoryStruct.comp (fun e => AddEquiv.toAddCommMonCatIso e) fun i => CategoryTheory.Iso.commMonCatIsoToAddEquiv i

theorem addEquivIsoAddCommMonCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [AddCommMonoid X] [AddCommMonoid Y] : (CategoryTheory.CategoryStruct.comp (fun i => CategoryTheory.Iso.commMonCatIsoToAddEquiv i) fun e => AddEquiv.toAddCommMonCatIso e) = CategoryTheory.CategoryStruct.comp (fun i => CategoryTheory.Iso.commMonCatIsoToAddEquiv i) fun e => AddEquiv.toAddCommMonCatIso e

def addEquivIsoAddCommMonCatIso {X : Type u} {Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] : X ≃+ Y ≅ AddCommMonCat.of X ≅ AddCommMonCat.of Y

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

def mulEquivIsoCommMonCatIso {X : Type u} {Y : Type u} [CommMonoid X] [CommMonoid Y] : X ≃* Y ≅ CommMonCat.of X ≅ CommMonCat.of Y

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

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

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

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

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

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

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

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

theorem AddCommMonCat.forget₂Full.proof_1 {X_1 : AddCommMonCat} {Y_1 : AddCommMonCat} (f : (CategoryTheory.forget₂ AddCommMonCat AddMonCat).obj X_1 ⟶ (CategoryTheory.forget₂ AddCommMonCat AddMonCat).obj Y_1) : (CategoryTheory.forget₂ AddCommMonCat AddMonCat).map ((fun {X Y} f => f) f) = f

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