mathlib documentation

algebra.category.Mon.basic

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

We introduce the bundled categories:

Mon
AddMon
CommMon
AddCommMon along with the relevant forgetful functors between them.

def Mon :

Type (u+1)

The category of monoids and monoid morphisms.

Equations

Mon = category_theory.bundled monoid

def AddMon :

Type (u+1)

The category of additive monoids and monoid morphisms.

Equations

AddMon = category_theory.bundled add_monoid

def AddMon.assoc_add_monoid_hom (M : Type u_1) (N : Type u_2) [add_monoid M] [add_monoid N] :

Type (max u_1 u_2)

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

def Mon.assoc_monoid_hom (M : Type u_1) (N : Type u_2) [monoid M] [monoid N] :

Type (max u_1 u_2)

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

@[protected, instance]

def Mon.bundled_hom :

category_theory.bundled_hom Mon.assoc_monoid_hom

Equations

Mon.bundled_hom = {to_fun := λ (M N : Type u_1) [_inst_1 : monoid M] [_inst_2 : monoid N], monoid_hom.to_fun, id := λ (M : Type u_1) [_inst_1 : monoid M], monoid_hom.id M, comp := λ (M N P : Type u_1) [_inst_1 : monoid M] [_inst_2 : monoid N] [_inst_3 : monoid P], monoid_hom.comp, hom_ext := Mon.bundled_hom._proof_1, id_to_fun := Mon.bundled_hom._proof_2, comp_to_fun := Mon.bundled_hom._proof_3}

@[protected, instance]

def AddMon.bundled_hom :

category_theory.bundled_hom AddMon.assoc_add_monoid_hom

Equations

AddMon.bundled_hom = {to_fun := λ (M N : Type u_1) [_inst_1 : add_monoid M] [_inst_2 : add_monoid N], add_monoid_hom.to_fun, id := λ (M : Type u_1) [_inst_1 : add_monoid M], add_monoid_hom.id M, comp := λ (M N P : Type u_1) [_inst_1 : add_monoid M] [_inst_2 : add_monoid N] [_inst_3 : add_monoid P], add_monoid_hom.comp, hom_ext := AddMon.bundled_hom._proof_1, id_to_fun := AddMon.bundled_hom._proof_2, comp_to_fun := AddMon.bundled_hom._proof_3}

@[protected, instance]

def Mon.large_category :

category_theory.large_category Mon

@[protected, instance]

def Mon.concrete_category :

category_theory.concrete_category Mon

@[protected, instance]

def AddMon.large_category :

category_theory.large_category AddMon

@[protected, instance]

def AddMon.concrete_category :

category_theory.concrete_category AddMon

@[protected, instance]

def AddMon.has_coe_to_sort :

has_coe_to_sort AddMon (Type u_1)

Equations

AddMon.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

@[protected, instance]

def Mon.has_coe_to_sort :

has_coe_to_sort Mon (Type u_1)

Equations

Mon.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

def AddMon.of (M : Type u) [add_monoid M] :

Construct a bundled Mon from the underlying type and typeclass.

Equations

AddMon.of M = category_theory.bundled.of M

def Mon.of (M : Type u) [monoid M] :

Construct a bundled Mon from the underlying type and typeclass.

Equations

Mon.of M = category_theory.bundled.of M

def AddMon.of_hom {X Y : Type u} [add_monoid X] [add_monoid Y] (f : X →+ Y) :

AddMon.of X ⟶ AddMon.of Y

Typecheck a add_monoid_hom as a morphism in AddMon.

Equations

AddMon.of_hom f = f

def Mon.of_hom {X Y : Type u} [monoid X] [monoid Y] (f : X →* Y) :

Mon.of X ⟶ Mon.of Y

Typecheck a monoid_hom as a morphism in Mon.

Equations

Mon.of_hom f = f

@[simp]

theorem Mon.of_hom_apply {X Y : Type u} [monoid X] [monoid Y] (f : X →* Y) (x : X) :

⇑(Mon.of_hom f) x = ⇑f x

@[protected, instance]

def Mon.inhabited :

Equations

Mon.inhabited = {default := Mon.of punit (group.to_monoid punit)}

@[protected, instance]

def AddMon.inhabited :

inhabited AddMon

Equations

AddMon.inhabited = {default := AddMon.of punit (add_group.to_add_monoid punit)}

@[protected, instance]

def Mon.monoid (M : Mon) :

Equations

M.monoid = M.str

@[protected, instance]

def AddMon.add_monoid (M : AddMon) :

add_monoid ↥M

Equations

M.add_monoid = M.str

@[simp]

theorem AddMon.coe_of (R : Type u) [add_monoid R] :

↥(AddMon.of R) = R

@[simp]

theorem Mon.coe_of (R : Type u) [monoid R] :

↥(Mon.of R) = R

def AddCommMon :

Type (u+1)

The category of additive commutative monoids and monoid morphisms.

Equations

AddCommMon = category_theory.bundled add_comm_monoid

def CommMon :

Type (u+1)

The category of commutative monoids and monoid morphisms.

Equations

CommMon = category_theory.bundled comm_monoid

@[protected, instance]

def CommMon.comm_monoid.to_monoid.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection comm_monoid.to_monoid

Equations

CommMon.comm_monoid.to_monoid.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

@[protected, instance]

def AddCommMon.comm_monoid.to_monoid.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection add_comm_monoid.to_add_monoid

Equations

AddCommMon.comm_monoid.to_monoid.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

@[protected, instance]

def CommMon.large_category :

category_theory.large_category CommMon

@[protected, instance]

def CommMon.concrete_category :

category_theory.concrete_category CommMon

@[protected, instance]

def AddCommMon.large_category :

category_theory.large_category AddCommMon

@[protected, instance]

def AddCommMon.concrete_category :

category_theory.concrete_category AddCommMon

@[protected, instance]

def CommMon.has_coe_to_sort :

has_coe_to_sort CommMon (Type u_1)

Equations

CommMon.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

@[protected, instance]

def AddCommMon.has_coe_to_sort :

has_coe_to_sort AddCommMon (Type u_1)

Equations

AddCommMon.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

def AddCommMon.of (M : Type u) [add_comm_monoid M] :

Construct a bundled AddCommMon from the underlying type and typeclass.

Equations

AddCommMon.of M = category_theory.bundled.of M

def CommMon.of (M : Type u) [comm_monoid M] :

Construct a bundled CommMon from the underlying type and typeclass.

Equations

CommMon.of M = category_theory.bundled.of M

@[protected, instance]

def CommMon.inhabited :

inhabited CommMon

Equations

CommMon.inhabited = {default := CommMon.of punit (comm_group.to_comm_monoid punit)}

@[protected, instance]

def AddCommMon.inhabited :

inhabited AddCommMon

Equations

AddCommMon.inhabited = {default := AddCommMon.of punit (add_comm_group.to_add_comm_monoid punit)}

@[protected, instance]

def CommMon.comm_monoid (M : CommMon) :

comm_monoid ↥M

Equations

M.comm_monoid = M.str

@[protected, instance]

def AddCommMon.add_comm_monoid (M : AddCommMon) :

add_comm_monoid ↥M

Equations

M.add_comm_monoid = M.str

@[simp]

theorem AddCommMon.coe_of (R : Type u) [add_comm_monoid R] :

↥(AddCommMon.of R) = R

@[simp]

theorem CommMon.coe_of (R : Type u) [comm_monoid R] :

↥(CommMon.of R) = R

@[protected, instance]

def AddCommMon.has_forget_to_AddMon :

category_theory.has_forget₂ AddCommMon AddMon

Equations

AddCommMon.has_forget_to_AddMon = category_theory.bundled_hom.forget₂ AddMon.assoc_add_monoid_hom add_comm_monoid.to_add_monoid

@[protected, instance]

def CommMon.has_forget_to_Mon :

category_theory.has_forget₂ CommMon Mon

Equations

CommMon.has_forget_to_Mon = category_theory.bundled_hom.forget₂ Mon.assoc_monoid_hom comm_monoid.to_monoid

@[simp]

theorem add_equiv.to_AddMon_iso_hom {X Y : Type u} [add_monoid X] [add_monoid Y] (e : X ≃+ Y) :

e.to_AddMon_iso.hom = e.to_add_monoid_hom

@[simp]

theorem add_equiv.to_AddMon_iso_neg {X Y : Type u} [add_monoid X] [add_monoid Y] (e : X ≃+ Y) :

e.to_AddMon_iso.inv = e.symm.to_add_monoid_hom

def mul_equiv.to_Mon_iso {X Y : Type u} [monoid X] [monoid Y] (e : X ≃* Y) :

Mon.of X ≅ Mon.of Y

Build an isomorphism in the category Mon from a mul_equiv between monoids.

Equations

e.to_Mon_iso = {hom := e.to_monoid_hom, inv := e.symm.to_monoid_hom, hom_inv_id' := _, inv_hom_id' := _}

@[simp]

theorem mul_equiv.to_Mon_iso_inv {X Y : Type u} [monoid X] [monoid Y] (e : X ≃* Y) :

e.to_Mon_iso.inv = e.symm.to_monoid_hom

def add_equiv.to_AddMon_iso {X Y : Type u} [add_monoid X] [add_monoid Y] (e : X ≃+ Y) :

AddMon.of X ≅ AddMon.of Y

Build an isomorphism in the category AddMon from an add_equiv between add_monoids.

Equations

e.to_AddMon_iso = {hom := e.to_add_monoid_hom, inv := e.symm.to_add_monoid_hom, hom_inv_id' := _, inv_hom_id' := _}

@[simp]

theorem mul_equiv.to_Mon_iso_hom {X Y : Type u} [monoid X] [monoid Y] (e : X ≃* Y) :

e.to_Mon_iso.hom = e.to_monoid_hom

def mul_equiv.to_CommMon_iso {X Y : Type u} [comm_monoid X] [comm_monoid Y] (e : X ≃* Y) :

CommMon.of X ≅ CommMon.of Y

Build an isomorphism in the category CommMon from a mul_equiv between comm_monoids.

Equations

e.to_CommMon_iso = {hom := e.to_monoid_hom, inv := e.symm.to_monoid_hom, hom_inv_id' := _, inv_hom_id' := _}

@[simp]

theorem mul_equiv.to_CommMon_iso_inv {X Y : Type u} [comm_monoid X] [comm_monoid Y] (e : X ≃* Y) :

e.to_CommMon_iso.inv = e.symm.to_monoid_hom

@[simp]

theorem add_equiv.to_AddCommMon_iso_hom {X Y : Type u} [add_comm_monoid X] [add_comm_monoid Y] (e : X ≃+ Y) :

e.to_AddCommMon_iso.hom = e.to_add_monoid_hom

@[simp]

theorem add_equiv.to_AddCommMon_iso_neg {X Y : Type u} [add_comm_monoid X] [add_comm_monoid Y] (e : X ≃+ Y) :

e.to_AddCommMon_iso.inv = e.symm.to_add_monoid_hom

@[simp]

theorem mul_equiv.to_CommMon_iso_hom {X Y : Type u} [comm_monoid X] [comm_monoid Y] (e : X ≃* Y) :

e.to_CommMon_iso.hom = e.to_monoid_hom

def add_equiv.to_AddCommMon_iso {X Y : Type u} [add_comm_monoid X] [add_comm_monoid Y] (e : X ≃+ Y) :

AddCommMon.of X ≅ AddCommMon.of Y

Build an isomorphism in the category AddCommMon from an add_equiv between add_comm_monoids.

Equations

e.to_AddCommMon_iso = {hom := e.to_add_monoid_hom, inv := e.symm.to_add_monoid_hom, hom_inv_id' := _, inv_hom_id' := _}

def category_theory.iso.AddMon_iso_to_add_equiv {X Y : AddMon} (i : X ≅ Y) :

Build an add_equiv from an isomorphism in the category AddMon.

Equations

i.AddMon_iso_to_add_equiv = add_monoid_hom.to_add_equiv i.hom i.inv _ _

def category_theory.iso.Mon_iso_to_mul_equiv {X Y : Mon} (i : X ≅ Y) :

Build a mul_equiv from an isomorphism in the category Mon.

Equations

i.Mon_iso_to_mul_equiv = monoid_hom.to_mul_equiv i.hom i.inv _ _

def category_theory.iso.CommMon_iso_to_add_equiv {X Y : AddCommMon} (i : X ≅ Y) :

Build an add_equiv from an isomorphism in the category AddCommMon.

Equations

i.CommMon_iso_to_add_equiv = add_monoid_hom.to_add_equiv i.hom i.inv _ _

def category_theory.iso.CommMon_iso_to_mul_equiv {X Y : CommMon} (i : X ≅ Y) :

Build a mul_equiv from an isomorphism in the category CommMon.

Equations

i.CommMon_iso_to_mul_equiv = monoid_hom.to_mul_equiv i.hom i.inv _ _

def mul_equiv_iso_Mon_iso {X Y : Type u} [monoid X] [monoid Y] :

X ≃* Y ≅ Mon.of X ≅ Mon.of Y

multiplicative equivalences between monoids are the same as (isomorphic to) isomorphisms in Mon

Equations

mul_equiv_iso_Mon_iso = {hom := λ (e : X ≃* Y), e.to_Mon_iso, inv := λ (i : Mon.of X ≅ Mon.of Y), i.Mon_iso_to_mul_equiv, hom_inv_id' := _, inv_hom_id' := _}

def add_equiv_iso_AddMon_iso {X Y : Type u} [add_monoid X] [add_monoid Y] :

X ≃+ Y ≅ AddMon.of X ≅ AddMon.of Y

additive equivalences between add_monoids are the same as (isomorphic to) isomorphisms in AddMon

Equations

add_equiv_iso_AddMon_iso = {hom := λ (e : X ≃+ Y), e.to_AddMon_iso, inv := λ (i : AddMon.of X ≅ AddMon.of Y), i.AddMon_iso_to_add_equiv, hom_inv_id' := _, inv_hom_id' := _}

def mul_equiv_iso_CommMon_iso {X Y : Type u} [comm_monoid X] [comm_monoid Y] :

X ≃* Y ≅ CommMon.of X ≅ CommMon.of Y

multiplicative equivalences between comm_monoids are the same as (isomorphic to) isomorphisms in CommMon

Equations

mul_equiv_iso_CommMon_iso = {hom := λ (e : X ≃* Y), e.to_CommMon_iso, inv := λ (i : CommMon.of X ≅ CommMon.of Y), i.CommMon_iso_to_mul_equiv, hom_inv_id' := _, inv_hom_id' := _}

def add_equiv_iso_AddCommMon_iso {X Y : Type u} [add_comm_monoid X] [add_comm_monoid Y] :

X ≃+ Y ≅ AddCommMon.of X ≅ AddCommMon.of Y

additive equivalences between add_comm_monoids are the same as (isomorphic to) isomorphisms in AddCommMon

Equations

add_equiv_iso_AddCommMon_iso = {hom := λ (e : X ≃+ Y), e.to_AddCommMon_iso, inv := λ (i : AddCommMon.of X ≅ AddCommMon.of Y), i.CommMon_iso_to_add_equiv, hom_inv_id' := _, inv_hom_id' := _}

@[protected, instance]

def AddMon.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget AddMon)

@[protected, instance]

def Mon.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget Mon)

@[protected, instance]

def AddCommMon.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget AddCommMon)

@[protected, instance]

def CommMon.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget CommMon)

Once we've shown that the forgetful functors to type reflect isomorphisms, we automatically obtain that the forget₂ functors between our concrete categories reflect isomorphisms.