mathlib3 documentation

algebra.category.Semigroup.basic

Category instances for has_mul, has_add, semigroup and add_semigroup #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We introduce the bundled categories:

This closely follows algebra.category.Mon.basic.

TODO #

def AddMagma  :
Type (u+1)

The category of additive magmas and additive magma morphisms.

Equations
Instances for AddMagma
@[protected, instance]
Equations
@[protected, instance]
Equations
def Magma.of (M : Type u) [has_mul M] :

Construct a bundled Magma from the underlying type and typeclass.

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

Construct a bundled AddMagma from the underlying type and typeclass.

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

Typecheck a mul_hom as a morphism in Magma.

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

Typecheck a add_hom as a morphism in AddMagma.

Equations
@[simp]
theorem Magma.of_hom_apply {X Y : Type u} [has_mul X] [has_mul Y] (f : X →ₙ* Y) (x : X) :
@[simp]
theorem AddMagma.of_hom_apply {X Y : Type u} [has_add X] [has_add Y] (f : add_hom X Y) (x : X) :
@[protected, instance]
Equations
@[protected, instance]
def Magma.has_mul (M : Magma) :
Equations
@[simp]
theorem Magma.coe_of (R : Type u) [has_mul R] :
@[simp]
theorem AddMagma.coe_of (R : Type u) [has_add R] :

Construct a bundled AddSemigroup from the underlying type and typeclass.

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

Construct a bundled Semigroup from the underlying type and typeclass.

Equations

Typecheck a add_hom as a morphism in AddSemigroup.

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

Typecheck a mul_hom as a morphism in Semigroup.

Equations
@[simp]
theorem Semigroup.of_hom_apply {X Y : Type u} [semigroup X] [semigroup Y] (f : X →ₙ* Y) (x : X) :
@[simp]
theorem AddSemigroup.of_hom_apply {X Y : Type u} [add_semigroup X] [add_semigroup Y] (f : add_hom X Y) (x : X) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[simp]
theorem Semigroup.coe_of (R : Type u) [semigroup R] :
def add_equiv.to_AddMagma_iso {X Y : Type u} [has_add X] [has_add Y] (e : X ≃+ Y) :

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

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

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

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

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

Equations

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

Equations

Build a mul_equiv from an isomorphism in the category Magma.

Equations

Build an add_equiv from an isomorphism in the category AddMagma.

Equations

Build a mul_equiv from an isomorphism in the category Semigroup.

Equations

Build an add_equiv from an isomorphism in the category AddSemigroup.

Equations

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

Equations

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

Equations

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

Equations

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

Equations

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.