mathlib docs: algebra.category.Mon.basic

source

def Mon :

Type (u+1)

The category of monoids and monoid morphisms.

Equations

Mon = category_theory.bundled monoid

source

def AddMon :

Type (u+1)

The category of additive monoids and monoid morphisms.

source

@[instance]

def Mon.bundled_hom :

category_theory.bundled_hom monoid_hom

Equations

Mon.bundled_hom = {to_fun := monoid_hom.to_fun, id := monoid_hom.id, comp := monoid_hom.comp, hom_ext := monoid_hom.coe_inj, id_to_fun := Mon.bundled_hom._proof_1, comp_to_fun := Mon.bundled_hom._proof_2}

source

@[instance]

def AddMon.bundled_hom :

category_theory.bundled_hom add_monoid_hom

source

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

AddMon

Construct a bundled Mon from the underlying type and typeclass.

source

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

Mon

Construct a bundled Mon from the underlying type and typeclass.

Equations

Mon.of M = category_theory.bundled.of M

source

@[instance]

def Mon.inhabited :

inhabited Mon

Equations

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

source

@[instance]

def AddMon.inhabited :

inhabited AddMon

source

@[instance]

def Mon.monoid (M : Mon) :

monoid ↥M

Equations

M.monoid = M.str

source

@[instance]

def AddMon.add_monoid (M : AddMon) :

add_monoid ↥M

source

@[simp]

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

↥(AddMon.of R) = R

source

@[simp]

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

↥(Mon.of R) = R

source

def AddCommMon :

Type (u+1)

The category of additive commutative monoids and monoid morphisms.

source

def CommMon :

Type (u+1)

The category of commutative monoids and monoid morphisms.

Equations

CommMon = category_theory.bundled comm_monoid

source

@[instance]

def AddCommMon.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection add_comm_monoid.to_add_monoid

source

@[instance]

def CommMon.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection comm_monoid.to_monoid

Equations

CommMon.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

source

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

AddCommMon

Construct a bundled AddCommMon from the underlying type and typeclass.

source

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

CommMon

Construct a bundled CommMon from the underlying type and typeclass.

Equations

CommMon.of M = category_theory.bundled.of M

source

@[instance]

def CommMon.inhabited :

inhabited CommMon

Equations

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

source

@[instance]

def AddCommMon.inhabited :

inhabited AddCommMon

source

@[instance]

def CommMon.comm_monoid (M : CommMon) :

comm_monoid ↥M

Equations

M.comm_monoid = M.str

source

@[instance]

def AddCommMon.add_comm_monoid (M : AddCommMon) :

add_comm_monoid ↥M

source

@[simp]

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

↥(AddCommMon.of R) = R

source

@[simp]

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

↥(CommMon.of R) = R

source

@[instance]

def AddCommMon.has_forget_to_AddMon :

category_theory.has_forget₂ AddCommMon AddMon

source

@[instance]

def CommMon.has_forget_to_Mon :

category_theory.has_forget₂ CommMon Mon

Equations

CommMon.has_forget_to_Mon = category_theory.bundled_hom.forget₂ monoid_hom comm_monoid.to_monoid

source

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' := _}

source

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.

source

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

source

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

source

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

source

@[simp]

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

e.to_AddMon_iso.inv = e.symm.to_add_monoid_hom

source

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' := _}

source

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.

source

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

source

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

source

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

source

@[simp]

theorem add_equiv.to_AddCommMon_iso_inv {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

source

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

↥X ≃+ ↥Y

Build an add_equiv from an isomorphism in the category AddMon.

source

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

↥X ≃* ↥Y

Build a mul_equiv from an isomorphism in the category Mon.

Equations

i.Mon_iso_to_mul_equiv = {to_fun := ⇑(i.hom), inv_fun := ⇑(i.inv), left_inv := _, right_inv := _, map_mul' := _}

source

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

↥X ≃+ ↥Y

Build an add_equiv from an isomorphism in the category AddCommMon.

source

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

↥X ≃* ↥Y

Build a mul_equiv from an isomorphism in the category CommMon.

Equations

i.CommMon_iso_to_mul_equiv = {to_fun := ⇑(i.hom), inv_fun := ⇑(i.inv), left_inv := _, right_inv := _, map_mul' := _}

source

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' := _}

source

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

source

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' := _}

source

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

source

@[instance]

def AddMon.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget AddMon)

source

@[instance]

def Mon.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget Mon)

Equations

Mon.forget_reflects_isos = {reflects := λ (X Y : Mon) (f : X ⟶ Y) (_x : category_theory.is_iso ((category_theory.forget Mon).map f)), let i : (category_theory.forget Mon).obj X ≅ (category_theory.forget Mon).obj Y := category_theory.as_iso ((category_theory.forget Mon).map f), e : ↥X ≃* ↥Y := {to_fun := f.to_fun, inv_fun := i.to_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _} in {inv := e.to_Mon_iso.inv, hom_inv_id' := _, inv_hom_id' := _}}

source

@[instance]

def AddCommMon.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget AddCommMon)

source

@[instance]

def CommMon.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget CommMon)

Equations

CommMon.forget_reflects_isos = {reflects := λ (X Y : CommMon) (f : X ⟶ Y) (_x : category_theory.is_iso ((category_theory.forget CommMon).map f)), let i : (category_theory.forget CommMon).obj X ≅ (category_theory.forget CommMon).obj Y := category_theory.as_iso ((category_theory.forget CommMon).map f), e : ↥X ≃* ↥Y := {to_fun := f.to_fun, inv_fun := i.to_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _} in {inv := e.to_CommMon_iso.inv, hom_inv_id' := _, inv_hom_id' := _}}

mathlib documentation

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