Adjunctions regarding the category of (abelian) groups #
This file contains construction of basic adjunctions concerning the category of groups and the category of abelian groups.
Main definitions #
AddCommGrp.free
: constructs the functor associating to a typeX
the free abelian group with generatorsx : X
.Grp.free
: constructs the functor associating to a typeX
the free group with generatorsx : X
.Grp.abelianize
: constructs the functor which associates to a groupG
its abelianizationGᵃᵇ
.
Main statements #
AddCommGrp.adj
: proves thatAddCommGrp.free
is the left adjoint of the forgetful functor from abelian groups to types.Grp.adj
: proves thatGrp.free
is the left adjoint of the forgetful functor from groups to types.abelianizeAdj
: proves thatGrp.abelianize
is left adjoint to the forgetful functor from abelian groups to groups.
The free functor Type u ⥤ AddCommGroup
sending a type X
to the
free abelian group with generators x : X
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
AddCommGrp.free_map_coe
{α : Type u}
{β : Type u}
{f : α → β}
(x : FreeAbelianGroup α)
:
(AddCommGrp.free.map f) x = f <$> x
The free-forgetful adjunction for abelian groups.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
Equations
Equations
The free functor Type u ⥤ Group
sending a type X
to the free group with generators x : X
.
Equations
- Grp.free = { obj := fun (α : Type ?u.10) => Grp.of (FreeGroup α), map := fun {X Y : Type ?u.10} => FreeGroup.map, map_id := Grp.free.proof_1, map_comp := @Grp.free.proof_2 }
Instances For
Equations
@[simp]
The functor taking a monoid to its subgroup of units.
Equations
- MonCat.units = { obj := fun (R : MonCat) => Grp.of (↑R)ˣ, map := fun {X Y : MonCat} (f : X ⟶ Y) => Grp.ofHom (Units.map f), map_id := MonCat.units.proof_1, map_comp := @MonCat.units.proof_2 }
Instances For
Equations
@[simp]
theorem
CommMonCat.units_map :
∀ {X Y : CommMonCat} (f : X ⟶ Y), CommMonCat.units.map f = CommGrp.ofHom (Units.map f)
@[simp]
The functor taking a monoid to its subgroup of units.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forgetful-units adjunction between CommGrp
and CommMonCat
.
Equations
- One or more equations did not get rendered due to their size.