algebra.category.Semigroup.basic

source

def AddMagma :

Type (u+1)

The category of additive magmas and additive magma morphisms.

Equations

AddMagma = category_theory.bundled has_add

Instances for AddMagma

source

def Magma :

Type (u+1)

The category of magmas and magma morphisms.

Equations

Magma = category_theory.bundled has_mul

Instances for Magma

source

@[protected, instance]

def AddMagma.bundled_hom :

category_theory.bundled_hom add_hom

Equations

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

source

@[protected, instance]

def Magma.bundled_hom :

category_theory.bundled_hom mul_hom

Equations

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

source

@[protected, instance]

def Magma.large_category :

category_theory.large_category Magma

source

@[protected, instance]

def Magma.concrete_category :

category_theory.concrete_category Magma

source

@[protected, instance]

def AddMagma.large_category :

category_theory.large_category AddMagma

source

@[protected, instance]

def AddMagma.concrete_category :

category_theory.concrete_category AddMagma

source

@[protected, instance]

def AddMagma.has_coe_to_sort :

has_coe_to_sort AddMagma (Type u_1)

Equations

AddMagma.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

@[protected, instance]

def Magma.has_coe_to_sort :

has_coe_to_sort Magma (Type u_1)

Equations

Magma.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

def Magma.of (M : Type u) [has_mul M] :

Magma

Construct a bundled Magma from the underlying type and typeclass.

Equations

Magma.of M = category_theory.bundled.of M

source

def AddMagma.of (M : Type u) [has_add M] :

AddMagma

Construct a bundled AddMagma from the underlying type and typeclass.

Equations

AddMagma.of M = category_theory.bundled.of M

source

def Magma.of_hom {X Y : Type u} [has_mul X] [has_mul Y] (f : X →ₙ* Y) :

Magma.of X ⟶ Magma.of Y

Typecheck a mul_hom as a morphism in Magma.

Equations

Magma.of_hom f = f

source

def AddMagma.of_hom {X Y : Type u} [has_add X] [has_add Y] (f : add_hom X Y) :

AddMagma.of X ⟶ AddMagma.of Y

Typecheck a add_hom as a morphism in AddMagma.

Equations

AddMagma.of_hom f = f

source

@[simp]

theorem Magma.of_hom_apply {X Y : Type u} [has_mul X] [has_mul Y] (f : X →ₙ* Y) (x : X) :

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

source

@[simp]

theorem AddMagma.of_hom_apply {X Y : Type u} [has_add X] [has_add Y] (f : add_hom X Y) (x : X) :

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

source

@[protected, instance]

def Magma.inhabited :

inhabited Magma

Equations

Magma.inhabited = {default := Magma.of pempty (semigroup.to_has_mul pempty)}

source

@[protected, instance]

def AddMagma.inhabited :

inhabited AddMagma

Equations

AddMagma.inhabited = {default := AddMagma.of pempty (add_semigroup.to_has_add pempty)}

source

@[protected, instance]

def AddMagma.has_add (M : AddMagma) :

has_add ↥M

Equations

M.has_add = M.str

source

@[protected, instance]

def Magma.has_mul (M : Magma) :

has_mul ↥M

Equations

M.has_mul = M.str

source

@[simp]

theorem Magma.coe_of (R : Type u) [has_mul R] :

↥(Magma.of R) = R

source

@[simp]

theorem AddMagma.coe_of (R : Type u) [has_add R] :

↥(AddMagma.of R) = R

source

def AddSemigroup :

Type (u+1)

The category of additive semigroups and semigroup morphisms.

Equations

AddSemigroup = category_theory.bundled add_semigroup

Instances for AddSemigroup

source

def Semigroup :

Type (u+1)

The category of semigroups and semigroup morphisms.

Equations

Semigroup = category_theory.bundled semigroup

Instances for Semigroup

source

@[protected, instance]

def AddSemigroup.semigroup.to_has_mul.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection add_semigroup.to_has_add

Equations

AddSemigroup.semigroup.to_has_mul.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

source

@[protected, instance]

def Semigroup.semigroup.to_has_mul.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection semigroup.to_has_mul

Equations

Semigroup.semigroup.to_has_mul.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

source

@[protected, instance]

def Semigroup.concrete_category :

category_theory.concrete_category Semigroup

source

@[protected, instance]

def Semigroup.large_category :

category_theory.large_category Semigroup

source

@[protected, instance]

def AddSemigroup.large_category :

category_theory.large_category AddSemigroup

source

@[protected, instance]

def AddSemigroup.concrete_category :

category_theory.concrete_category AddSemigroup

source

@[protected, instance]

def Semigroup.has_coe_to_sort :

has_coe_to_sort Semigroup (Type u_1)

Equations

Semigroup.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

@[protected, instance]

def AddSemigroup.has_coe_to_sort :

has_coe_to_sort AddSemigroup (Type u_1)

Equations

AddSemigroup.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

def AddSemigroup.of (M : Type u) [add_semigroup M] :

AddSemigroup

Construct a bundled AddSemigroup from the underlying type and typeclass.

Equations

AddSemigroup.of M = category_theory.bundled.of M

source

def Semigroup.of (M : Type u) [semigroup M] :

Semigroup

Construct a bundled Semigroup from the underlying type and typeclass.

Equations

Semigroup.of M = category_theory.bundled.of M

source

def AddSemigroup.of_hom {X Y : Type u} [add_semigroup X] [add_semigroup Y] (f : add_hom X Y) :

AddSemigroup.of X ⟶ AddSemigroup.of Y

Typecheck a add_hom as a morphism in AddSemigroup.

Equations

AddSemigroup.of_hom f = f

source

def Semigroup.of_hom {X Y : Type u} [semigroup X] [semigroup Y] (f : X →ₙ* Y) :

Semigroup.of X ⟶ Semigroup.of Y

Typecheck a mul_hom as a morphism in Semigroup.

Equations

Semigroup.of_hom f = f

source

@[simp]

theorem Semigroup.of_hom_apply {X Y : Type u} [semigroup X] [semigroup Y] (f : X →ₙ* Y) (x : X) :

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

source

@[simp]

theorem AddSemigroup.of_hom_apply {X Y : Type u} [add_semigroup X] [add_semigroup Y] (f : add_hom X Y) (x : X) :

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

source

@[protected, instance]

def AddSemigroup.inhabited :

inhabited AddSemigroup

Equations

AddSemigroup.inhabited = {default := AddSemigroup.of pempty add_semigroup_pempty}

source

@[protected, instance]

def Semigroup.inhabited :

inhabited Semigroup

Equations

Semigroup.inhabited = {default := Semigroup.of pempty semigroup_pempty}

source

@[protected, instance]

def Semigroup.semigroup (M : Semigroup) :

semigroup ↥M

Equations

M.semigroup = M.str

source

@[protected, instance]

def AddSemigroup.add_semigroup (M : AddSemigroup) :

add_semigroup ↥M

Equations

M.add_semigroup = M.str

source

@[simp]

theorem AddSemigroup.coe_of (R : Type u) [add_semigroup R] :

↥(AddSemigroup.of R) = R

source

@[simp]

theorem Semigroup.coe_of (R : Type u) [semigroup R] :

↥(Semigroup.of R) = R

source

@[protected, instance]

def AddSemigroup.has_forget_to_AddMagma :

category_theory.has_forget₂ AddSemigroup AddMagma

Equations

AddSemigroup.has_forget_to_AddMagma = category_theory.bundled_hom.forget₂ add_hom add_semigroup.to_has_add

source

@[protected, instance]

def Semigroup.has_forget_to_Magma :

category_theory.has_forget₂ Semigroup Magma

Equations

Semigroup.has_forget_to_Magma = category_theory.bundled_hom.forget₂ mul_hom semigroup.to_has_mul

source

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

AddMagma.of X ≅ AddMagma.of Y

Build an isomorphism in the category AddMagma from an add_equiv between has_adds.

Equations

e.to_AddMagma_iso = {hom := e.to_add_hom, inv := e.symm.to_add_hom, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

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

e.to_AddMagma_iso.hom = e.to_add_hom

source

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

Magma.of X ≅ Magma.of Y

Build an isomorphism in the category Magma from a mul_equiv between has_muls.

Equations

e.to_Magma_iso = {hom := e.to_mul_hom, inv := e.symm.to_mul_hom, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

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

e.to_AddMagma_iso.inv = e.symm.to_add_hom

source

@[simp]

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

e.to_Magma_iso.inv = e.symm.to_mul_hom

source

@[simp]

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

e.to_Magma_iso.hom = e.to_mul_hom

source

@[simp]

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

e.to_AddSemigroup_iso.hom = e.to_add_hom

source

@[simp]

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

e.to_Semigroup_iso.hom = e.to_mul_hom

source

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

Semigroup.of X ≅ Semigroup.of Y

Build an isomorphism in the category Semigroup from a mul_equiv between semigroups.

Equations

e.to_Semigroup_iso = {hom := e.to_mul_hom, inv := e.symm.to_mul_hom, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

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

e.to_AddSemigroup_iso.inv = e.symm.to_add_hom

source

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

AddSemigroup.of X ≅ AddSemigroup.of Y

Build an isomorphism in the category AddSemigroup from an add_equiv between add_semigroups.

Equations

e.to_AddSemigroup_iso = {hom := e.to_add_hom, inv := e.symm.to_add_hom, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

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

e.to_Semigroup_iso.inv = e.symm.to_mul_hom

source

def category_theory.iso.Magma_iso_to_mul_equiv {X Y : Magma} (i : X ≅ Y) :

↥X ≃* ↥Y

Build a mul_equiv from an isomorphism in the category Magma.

Equations

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

source

def category_theory.iso.AddMagma_iso_to_add_equiv {X Y : AddMagma} (i : X ≅ Y) :

↥X ≃+ ↥Y

Build an add_equiv from an isomorphism in the category AddMagma.

Equations

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

source

def category_theory.iso.Semigroup_iso_to_mul_equiv {X Y : Semigroup} (i : X ≅ Y) :

↥X ≃* ↥Y

Build a mul_equiv from an isomorphism in the category Semigroup.

Equations

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

source

def category_theory.iso.Semigroup_iso_to_add_equiv {X Y : AddSemigroup} (i : X ≅ Y) :

↥X ≃+ ↥Y

Build an add_equiv from an isomorphism in the category AddSemigroup.

Equations

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

source

def add_equiv_iso_AddMagma_iso {X Y : Type u} [has_add X] [has_add Y] :

X ≃+ Y ≅ AddMagma.of X ≅ AddMagma.of Y

additive equivalences between has_adds are the same as (isomorphic to) isomorphisms in AddMagma

Equations

add_equiv_iso_AddMagma_iso = {hom := λ (e : X ≃+ Y), e.to_AddMagma_iso, inv := λ (i : AddMagma.of X ≅ AddMagma.of Y), i.AddMagma_iso_to_add_equiv, hom_inv_id' := _, inv_hom_id' := _}

source

def mul_equiv_iso_Magma_iso {X Y : Type u} [has_mul X] [has_mul Y] :

X ≃* Y ≅ Magma.of X ≅ Magma.of Y

multiplicative equivalences between has_muls are the same as (isomorphic to) isomorphisms in Magma

Equations

mul_equiv_iso_Magma_iso = {hom := λ (e : X ≃* Y), e.to_Magma_iso, inv := λ (i : Magma.of X ≅ Magma.of Y), i.Magma_iso_to_mul_equiv, hom_inv_id' := _, inv_hom_id' := _}

source

def mul_equiv_iso_Semigroup_iso {X Y : Type u} [semigroup X] [semigroup Y] :

X ≃* Y ≅ Semigroup.of X ≅ Semigroup.of Y

multiplicative equivalences between semigroups are the same as (isomorphic to) isomorphisms in Semigroup

Equations

mul_equiv_iso_Semigroup_iso = {hom := λ (e : X ≃* Y), e.to_Semigroup_iso, inv := λ (i : Semigroup.of X ≅ Semigroup.of Y), i.Semigroup_iso_to_mul_equiv, hom_inv_id' := _, inv_hom_id' := _}

source

def add_equiv_iso_AddSemigroup_iso {X Y : Type u} [add_semigroup X] [add_semigroup Y] :

X ≃+ Y ≅ AddSemigroup.of X ≅ AddSemigroup.of Y

additive equivalences between add_semigroups are the same as (isomorphic to) isomorphisms in AddSemigroup

Equations

add_equiv_iso_AddSemigroup_iso = {hom := λ (e : X ≃+ Y), e.to_AddSemigroup_iso, inv := λ (i : AddSemigroup.of X ≅ AddSemigroup.of Y), i.Semigroup_iso_to_add_equiv, hom_inv_id' := _, inv_hom_id' := _}

source

@[protected, instance]

def AddMagma.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget AddMagma)

source

@[protected, instance]

def Magma.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget Magma)

source

@[protected, instance]

def AddSemigroup.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget AddSemigroup)

source

@[protected, instance]

def Semigroup.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget Semigroup)

mathlib documentation

Category instances for has_mul, has_add, semigroup and add_semigroup #

TODO #