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.

def AddMonCat : Type (u + 1)

The category of additive monoids and monoid morphisms.

Equations

• AddMonCat = CategoryTheory.Bundled AddMonoid

def MonCat : Type (u + 1)

The category of monoids and monoid morphisms.

Equations

• MonCat = CategoryTheory.Bundled Monoid

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

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

Equations

• AddMonCat.AssocAddMonoidHom M N = (M →+ N)

@[inline, reducible]

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

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

Equations

• MonCat.AssocMonoidHom M N = (M →* N)

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

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 : Type u_1} (x : AddMonoid X) (x_1 : AddMonoid Y) (f : AddMonCat.AssocAddMonoidHom X Y) => ⇑f) Iα Iβ a₁ = (fun {X Y : Type u_1} (x : AddMonoid X) (x_1 : AddMonoid Y) (f : AddMonCat.AssocAddMonoidHom X Y) => ⇑f) Iα Iβ a₂) : a₁ = a₂

instance AddMonCat.bundledHom : CategoryTheory.BundledHom AddMonCat.AssocAddMonoidHom

Equations

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

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

instance MonCat.bundledHom : CategoryTheory.BundledHom MonCat.AssocMonoidHom

Equations

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

instance instAddMonCatLargeCategory : CategoryTheory.LargeCategory AddMonCat

Equations

• instAddMonCatLargeCategory = CategoryTheory.BundledHom.category AddMonCat.AssocAddMonoidHom

instance AddMonCat.concreteCategory : CategoryTheory.ConcreteCategory AddMonCat

Equations

• AddMonCat.concreteCategory = CategoryTheory.BundledHom.concreteCategory AddMonCat.AssocAddMonoidHom

instance MonCat.concreteCategory : CategoryTheory.ConcreteCategory MonCat

Equations

• MonCat.concreteCategory = CategoryTheory.BundledHom.concreteCategory MonCat.AssocMonoidHom

instance AddMonCat.instCoeSortMonCatType : CoeSort AddMonCat (Type u_1)

Equations

• AddMonCat.instCoeSortMonCatType = { coe := fun (X : AddMonCat) => ↑X }

instance MonCat.instCoeSortMonCatType : CoeSort MonCat (Type u_1)

Equations

• MonCat.instCoeSortMonCatType = { coe := fun (X : MonCat) => ↑X }

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

Equations

• AddMonCat.instMonoidα X = X.str

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

Equations

• MonCat.instMonoidα X = X.str

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

Equations

• AddMonCat.instCoeFunHomMonCatToQuiverToCategoryStructInstMonCatLargeCategoryForAllαAddMonoid = { coe := fun (f : ↑X →+ ↑Y) => ⇑f }

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

Equations

• MonCat.instCoeFunHomMonCatToQuiverToCategoryStructInstMonCatLargeCategoryForAllαMonoid = { coe := fun (f : ↑X →* ↑Y) => ⇑f }

instance AddMonCat.instFunLike (X : AddMonCat) (Y : AddMonCat) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

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

instance MonCat.instFunLike (X : MonCat) (Y : MonCat) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

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

instance AddMonCat.instAddMonoidHomClass (X : AddMonCat) (Y : AddMonCat) : AddMonoidHomClass (X ⟶ Y) ↑X ↑Y

Equations

• ⋯ = ⋯

instance MonCat.instMonoidHomClass (X : MonCat) (Y : MonCat) : MonoidHomClass (X ⟶ Y) ↑X ↑Y

Equations

• ⋯ = ⋯

@[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.

Equations

• AddMonCat.of M = CategoryTheory.Bundled.of M

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

Construct a bundled MonCat from the underlying type and typeclass.

Equations

• MonCat.of M = CategoryTheory.Bundled.of M

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

Equations

• AddMonCat.instInhabitedMonCat = { default := AddMonCat.of PUnit.{u_1 + 1} }

instance MonCat.instInhabitedMonCat : Inhabited MonCat

Equations

• MonCat.instInhabitedMonCat = { default := MonCat.of PUnit.{u_1 + 1} }

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.

Equations

• AddMonCat.ofHom f = f

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.

Equations

• MonCat.ofHom f = f

@[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)

Equations

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

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

Equations

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

@[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)

Equations

• AddMonCat.instGroupαAddMonoidOfToAddMonoidToSubNegAddMonoid = inst

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

Equations

• MonCat.instGroupαMonoidOfToMonoidToDivInvMonoid = inst

def AddCommMonCat : Type (u + 1)

The category of additive commutative monoids and monoid morphisms.

Equations

• AddCommMonCat = CategoryTheory.Bundled AddCommMonoid

def CommMonCat : Type (u + 1)

The category of commutative monoids and monoid morphisms.

Equations

• CommMonCat = CategoryTheory.Bundled CommMonoid

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

Equations

• AddCommMonCat.instParentProjectionTypeAddMonoidAddCommMonoidToAddMonoid = ⋯

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

Equations

• CommMonCat.instParentProjectionTypeMonoidCommMonoidToMonoid = ⋯

instance instAddCommMonCatLargeCategory : CategoryTheory.LargeCategory AddCommMonCat

Equations

• instAddCommMonCatLargeCategory = CategoryTheory.BundledHom.category (CategoryTheory.BundledHom.MapHom AddMonCat.AssocAddMonoidHom @AddCommMonoid.toAddMonoid)

instance AddCommMonCat.concreteCategory : CategoryTheory.ConcreteCategory AddCommMonCat

Equations

• AddCommMonCat.concreteCategory = id inferInstance

instance CommMonCat.concreteCategory : CategoryTheory.ConcreteCategory CommMonCat

Equations

• CommMonCat.concreteCategory = id inferInstance

instance AddCommMonCat.instCoeSortCommMonCatType : CoeSort AddCommMonCat (Type u_1)

Equations

• AddCommMonCat.instCoeSortCommMonCatType = { coe := fun (X : AddCommMonCat) => ↑X }

instance CommMonCat.instCoeSortCommMonCatType : CoeSort CommMonCat (Type u_1)

Equations

• CommMonCat.instCoeSortCommMonCatType = { coe := fun (X : CommMonCat) => ↑X }

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

Equations

• AddCommMonCat.instCommMonoidα X = X.str

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

Equations

• CommMonCat.instCommMonoidα X = X.str

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

Equations

• AddCommMonCat.instCoeFunHomCommMonCatToQuiverToCategoryStructInstCommMonCatLargeCategoryForAllαAddCommMonoid = { coe := fun (f : ↑X →+ ↑Y) => ⇑f }

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

Equations

• CommMonCat.instCoeFunHomCommMonCatToQuiverToCategoryStructInstCommMonCatLargeCategoryForAllαCommMonoid = { coe := fun (f : ↑X →* ↑Y) => ⇑f }

instance AddCommMonCat.instFunLike (X : AddCommMonCat) (Y : AddCommMonCat) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• AddCommMonCat.instFunLike X Y = let_fun this := inferInstance; this

instance CommMonCat.instFunLike (X : CommMonCat) (Y : CommMonCat) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• CommMonCat.instFunLike X Y = let_fun this := inferInstance; this

@[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 AddCommMonCat from the underlying type and typeclass.

Equations

• AddCommMonCat.of M = CategoryTheory.Bundled.of M

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

Construct a bundled CommMonCat from the underlying type and typeclass.

Equations

• CommMonCat.of M = CategoryTheory.Bundled.of M

instance AddCommMonCat.instInhabitedCommMonCat : Inhabited AddCommMonCat

Equations

• AddCommMonCat.instInhabitedCommMonCat = { default := AddCommMonCat.of PUnit.{u_1 + 1} }

instance CommMonCat.instInhabitedCommMonCat : Inhabited CommMonCat

Equations

• CommMonCat.instInhabitedCommMonCat = { default := CommMonCat.of PUnit.{u_1 + 1} }

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

Equations

• AddCommMonCat.hasForgetToAddMonCat = CategoryTheory.BundledHom.forget₂ AddMonCat.AssocAddMonoidHom @AddCommMonoid.toAddMonoid

instance CommMonCat.hasForgetToMonCat : CategoryTheory.HasForget₂ CommMonCat MonCat

Equations

• CommMonCat.hasForgetToMonCat = CategoryTheory.BundledHom.forget₂ MonCat.AssocMonoidHom @CommMonoid.toMonoid

instance AddCommMonCat.instCoeCommMonCatMonCat : Coe AddCommMonCat AddMonCat

Equations

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

instance CommMonCat.instCoeCommMonCatMonCat : Coe CommMonCat MonCat

Equations

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

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.

Equations

• AddCommMonCat.ofHom f = f

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.

Equations

• CommMonCat.ofHom f = f

@[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_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)

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.

Equations

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

@[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_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))

@[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))

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.

Equations

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

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.

Equations

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

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)

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)

@[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.

Equations

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

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

Build an AddEquiv from an isomorphism in the category AddMonCat.

Equations

• CategoryTheory.Iso.addMonCatIsoToAddEquiv i = AddMonoidHom.toAddEquiv i.hom i.inv ⋯ ⋯

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

Build a MulEquiv from an isomorphism in the category MonCat.

Equations

• CategoryTheory.Iso.monCatIsoToMulEquiv i = MonoidHom.toMulEquiv i.hom i.inv ⋯ ⋯

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

Build an AddEquiv from an isomorphism in the category AddCommMonCat.

Equations

• CategoryTheory.Iso.commMonCatIsoToAddEquiv i = AddMonoidHom.toAddEquiv i.hom i.inv ⋯ ⋯

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

Build a MulEquiv from an isomorphism in the category CommMonCat.

Equations

• CategoryTheory.Iso.commMonCatIsoToMulEquiv i = MonoidHom.toMulEquiv i.hom i.inv ⋯ ⋯

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

Equations

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

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

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

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

Equations

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

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

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

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

Equations

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

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

Equations

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

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

Equations

• AddMonCat.forget_reflects_isos = ⋯

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

Equations

• MonCat.forget_reflects_isos = ⋯

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

Equations

• AddCommMonCat.forget_reflects_isos = ⋯

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

Equations

• CommMonCat.forget_reflects_isos = ⋯

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

Equations

• AddCommMonCat.forget₂_full = ⋯

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

Equations

• CommMonCat.forget₂_full = ⋯