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

@[reducible, inline]

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)

@[reducible, inline]

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 x_1 : Type u_1} (x_2 : AddMonoid x) (x_3 : AddMonoid x_1) (f : AddMonCat.AssocAddMonoidHom x x_1) => ⇑f) I I ((fun {α : Type u_1} (x : AddMonoid α) => AddMonoidHom.id α) I) = id

instance AddMonCat.bundledHom : CategoryTheory.BundledHom AddMonCat.AssocAddMonoidHom

Equations

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

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

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.instCoeSortType : CoeSort AddMonCat (Type u_1)

Equations

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

instance MonCat.instCoeSortType : CoeSort MonCat (Type u_1)

Equations

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

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

Equations

• X.instMonoidα = X.str

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

Equations

• X.instMonoidα = X.str

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• X.instFunLike 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 AddMonCat.ext_iff {X : AddMonCat} {Y : AddMonCat} {f : X ⟶ Y} {g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), f x = g x

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

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.instInhabited : Inhabited AddMonCat

Equations

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

instance MonCat.instInhabited : Inhabited MonCat

Equations

• MonCat.instInhabited = { 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.instZeroHom (X : AddMonCat) (Y : AddMonCat) : Zero (X ⟶ Y)

Equations

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

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

Equations

• X.instOneHom 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αAddMonoidOf {G : Type u_1} [AddGroup G] : AddGroup ↑(AddMonCat.of G)

Equations

• AddMonCat.instGroupαAddMonoidOf = inst

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

Equations

• MonCat.instGroupαMonoidOf = inst

theorem AddMonCat.uliftFunctor.proof_2 {X : AddMonCat} {Y : AddMonCat} {Z : AddMonCat} (f : X ⟶ Y) (g : Y ⟶ Z) : { obj := fun (X : AddMonCat) => AddMonCat.of (ULift.{u_2, u_1} ↑X), map := fun {x x_1 : AddMonCat} (f : x ⟶ x_1) => AddMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g) = { obj := fun (X : AddMonCat) => AddMonCat.of (ULift.{u_2, u_1} ↑X), map := fun {x x_1 : AddMonCat} (f : x ⟶ x_1) => AddMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g)

theorem AddMonCat.uliftFunctor.proof_1 (X : AddMonCat) : { obj := fun (X : AddMonCat) => AddMonCat.of (ULift.{u_2, u_1} ↑X), map := fun {x x_1 : AddMonCat} (f : x ⟶ x_1) => AddMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X) = { obj := fun (X : AddMonCat) => AddMonCat.of (ULift.{u_2, u_1} ↑X), map := fun {x x_1 : AddMonCat} (f : x ⟶ x_1) => AddMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X)

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 MonCat.uliftFunctor_obj (X : MonCat) : MonCat.uliftFunctor.obj X = MonCat.of (ULift.{v, u} ↑X)

@[simp]

theorem AddMonCat.uliftFunctor_map : ∀ {x x_1 : AddMonCat} (f : x ⟶ x_1), AddMonCat.uliftFunctor.map f = AddMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom))

@[simp]

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

@[simp]

theorem MonCat.uliftFunctor_map : ∀ {x x_1 : MonCat} (f : x ⟶ x_1), MonCat.uliftFunctor.map f = MonCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp (MonoidHom.comp f MulEquiv.ulift.toMonoidHom))

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 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.instParentProjectionAddMonoidAddCommMonoidToAddMonoid : CategoryTheory.BundledHom.ParentProjection @AddCommMonoid.toAddMonoid

Equations

• AddCommMonCat.instParentProjectionAddMonoidAddCommMonoidToAddMonoid = ⋯

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

Equations

• CommMonCat.instParentProjectionMonoidCommMonoidToMonoid = ⋯

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.instCoeSortType : CoeSort AddCommMonCat (Type u_1)

Equations

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

instance CommMonCat.instCoeSortType : CoeSort CommMonCat (Type u_1)

Equations

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

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

Equations

• X.instCommMonoidα = X.str

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

Equations

• X.instCommMonoidα = X.str

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

Equations

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

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

Equations

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

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

Equations

• X.instFunLike Y = inferInstance

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

Equations

• X.instFunLike Y = inferInstance

@[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 AddCommMonCat.ext_iff {X : AddCommMonCat} {Y : AddCommMonCat} {f : X ⟶ Y} {g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), f x = g x

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

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.instInhabited : Inhabited AddCommMonCat

Equations

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

instance CommMonCat.instInhabited : Inhabited CommMonCat

Equations

• CommMonCat.instInhabited = { 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.instCoeMonCat : Coe AddCommMonCat AddMonCat

Equations

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

instance CommMonCat.instCoeMonCat : Coe CommMonCat MonCat

Equations

• CommMonCat.instCoeMonCat = { 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 AddCommMonCat.uliftFunctor.proof_1 (X : AddCommMonCat) : { obj := fun (X : AddCommMonCat) => AddCommMonCat.of (ULift.{u_2, u_1} ↑X), map := fun {x x_1 : AddCommMonCat} (f : x ⟶ x_1) => AddCommMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X) = { obj := fun (X : AddCommMonCat) => AddCommMonCat.of (ULift.{u_2, u_1} ↑X), map := fun {x x_1 : AddCommMonCat} (f : x ⟶ x_1) => AddCommMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X)

theorem AddCommMonCat.uliftFunctor.proof_2 {X : AddCommMonCat} {Y : AddCommMonCat} {Z : AddCommMonCat} (f : X ⟶ Y) (g : Y ⟶ Z) : { obj := fun (X : AddCommMonCat) => AddCommMonCat.of (ULift.{u_2, u_1} ↑X), map := fun {x x_1 : AddCommMonCat} (f : x ⟶ x_1) => AddCommMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g) = { obj := fun (X : AddCommMonCat) => AddCommMonCat.of (ULift.{u_2, u_1} ↑X), map := fun {x x_1 : AddCommMonCat} (f : x ⟶ x_1) => AddCommMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g)

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 CommMonCat.uliftFunctor_obj (X : CommMonCat) : CommMonCat.uliftFunctor.obj X = CommMonCat.of (ULift.{v, u} ↑X)

@[simp]

theorem CommMonCat.uliftFunctor_map : ∀ {x x_1 : CommMonCat} (f : x ⟶ x_1), CommMonCat.uliftFunctor.map f = CommMonCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp (MonoidHom.comp f MulEquiv.ulift.toMonoidHom))

@[simp]

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

@[simp]

theorem AddCommMonCat.uliftFunctor_map : ∀ {x x_1 : AddCommMonCat} (f : x ⟶ x_1), AddCommMonCat.uliftFunctor.map f = AddCommMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom))

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.

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 e.toAddMonoidHom) (AddMonCat.ofHom e.symm.toAddMonoidHom) = 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 e.symm.toAddMonoidHom) (AddMonCat.ofHom e.toAddMonoidHom) = 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

• 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 : Type u} {Y : Type u} [Monoid X] [Monoid Y] (e : X ≃* Y) : e.toMonCatIso.inv = MonCat.ofHom e.symm.toMonoidHom

@[simp]

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

@[simp]

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

@[simp]

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

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

• e.toMonCatIso = { hom := MonCat.ofHom e.toMonoidHom, inv := MonCat.ofHom e.symm.toMonoidHom, 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

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

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 e.toAddMonoidHom) (AddCommMonCat.ofHom e.symm.toAddMonoidHom) = 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 e.symm.toAddMonoidHom) (AddCommMonCat.ofHom e.toAddMonoidHom) = CategoryTheory.CategoryStruct.id (AddCommMonCat.of Y)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

• e.toCommMonCatIso = { hom := CommMonCat.ofHom e.toMonoidHom, inv := CommMonCat.ofHom e.symm.toMonoidHom, 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

• i.addMonCatIsoToAddEquiv = 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

• i.monCatIsoToMulEquiv = 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

• i.commMonCatIsoToAddEquiv = 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

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

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) => i.addMonCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddMonCatIso) = CategoryTheory.CategoryStruct.comp (fun (i : AddMonCat.of X ≅ AddMonCat.of Y) => i.addMonCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddMonCatIso

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

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

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

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

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

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.

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

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) => i.commMonCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddCommMonCatIso) = CategoryTheory.CategoryStruct.comp (fun (i : AddCommMonCat.of X ≅ AddCommMonCat.of Y) => i.commMonCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddCommMonCatIso

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

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

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

Equations

• AddMonCat.forget_reflects_isos = ⋯

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

Equations

• MonCat.forget_reflects_isos = ⋯

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

Equations

• AddCommMonCat.forget_reflects_isos = ⋯

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

Equations

• CommMonCat.forget_reflects_isos = ⋯

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

Equations

• AddCommMonCat.forget₂_full = ⋯

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

Equations

• CommMonCat.forget₂_full = ⋯

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

@[simp]

theorem AddMonoidHom.comp_id_monCat {G : AddMonCat} {H : Type u} [AddMonoid H] (f : ↑G →+ H) : f.comp (CategoryTheory.CategoryStruct.id G) = f

@[simp]

theorem MonoidHom.comp_id_monCat {G : MonCat} {H : Type u} [Monoid H] (f : ↑G →* H) : f.comp (CategoryTheory.CategoryStruct.id G) = f

@[simp]

theorem AddMonoidHom.id_monCat_comp {G : Type u} [AddMonoid G] {H : AddMonCat} (f : G →+ ↑H) : AddMonoidHom.comp (CategoryTheory.CategoryStruct.id H) f = f

@[simp]

theorem MonoidHom.id_monCat_comp {G : Type u} [Monoid G] {H : MonCat} (f : G →* ↑H) : MonoidHom.comp (CategoryTheory.CategoryStruct.id H) f = f

@[simp]

theorem AddMonoidHom.comp_id_commMonCat {G : AddCommMonCat} {H : Type u} [AddCommMonoid H] (f : ↑G →+ H) : f.comp (CategoryTheory.CategoryStruct.id G) = f

@[simp]

theorem MonoidHom.comp_id_commMonCat {G : CommMonCat} {H : Type u} [CommMonoid H] (f : ↑G →* H) : f.comp (CategoryTheory.CategoryStruct.id G) = f

@[simp]

theorem AddMonoidHom.id_commMonCat_comp {G : Type u} [AddCommMonoid G] {H : AddCommMonCat} (f : G →+ ↑H) : AddMonoidHom.comp (CategoryTheory.CategoryStruct.id H) f = f

@[simp]

theorem MonoidHom.id_commMonCat_comp {G : Type u} [CommMonoid G] {H : CommMonCat} (f : G →* ↑H) : MonoidHom.comp (CategoryTheory.CategoryStruct.id H) f = f