Documentation

Mathlib.Algebra.Category.GroupCat.Basic

We introduce the bundled categories:

• GroupCat
• AddGroupCat
• CommGroupCat
• AddCommGroupCat along with the relevant forgetful functors between them, and to the bundled monoid categories.
Type (u + 1)

The category of additive groups and group morphisms

Equations
Instances For
def GroupCat :
Type (u + 1)

The category of groups and group morphisms.

Equations
Instances For
Equations
instance GroupCat.instParentProjectionMonoidGroup :
CategoryTheory.BundledHom.ParentProjection fun {α : Type u_1} (h : ) => DivInvMonoid.toMonoid
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
Equations
• X.instGroupα = X.str
instance GroupCat.instGroupα (X : GroupCat) :
Group X
Equations
• X.instGroupα = X.str
CoeFun (X Y) fun (x : X Y) => XY
Equations
• AddGroupCat.instCoeFunHomForallαAddGroup = { coe := fun (f : X →+ Y) => f }
instance GroupCat.instCoeFunHomForallαGroup {X : GroupCat} {Y : GroupCat} :
CoeFun (X Y) fun (x : X Y) => XY
Equations
• GroupCat.instCoeFunHomForallαGroup = { coe := fun (f : X →* Y) => f }
FunLike (X Y) X Y
Equations
• X.instFunLike Y = let_fun this := inferInstance; this
instance GroupCat.instFunLike (X : GroupCat) (Y : GroupCat) :
FunLike (X Y) X Y
Equations
• X.instFunLike Y = let_fun this := inferInstance; this
@[simp]
@[simp]
theorem GroupCat.coe_id {X : GroupCat} :
@[simp]
= g f
@[simp]
theorem GroupCat.coe_comp {X : GroupCat} {Y : GroupCat} {Z : GroupCat} {f : X Y} {g : Y Z} :
= g f
theorem GroupCat.comp_def {X : GroupCat} {Y : GroupCat} {Z : GroupCat} {f : X Y} {g : Y Z} :
@[simp]
theorem GroupCat.forget_map {X : GroupCat} {Y : GroupCat} (f : X Y) :
f = f
theorem AddGroupCat.ext {X : AddGroupCat} {Y : AddGroupCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
f = g
theorem GroupCat.ext {X : GroupCat} {Y : GroupCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
f = g

Construct a bundled AddGroup from the underlying type and typeclass.

Equations
Instances For
def GroupCat.of (X : Type u) [] :

Construct a bundled Group from the underlying type and typeclass.

Equations
Instances For
@[simp]
theorem AddGroupCat.coe_of (R : Type u) [] :
() = R
@[simp]
theorem GroupCat.coe_of (R : Type u) [] :
() = R
Equations
Equations
Equations
• G.instZeroHom H = inferInstance
instance GroupCat.instOneHom (G : GroupCat) (H : GroupCat) :
One (G H)
Equations
• G.instOneHom H = inferInstance
@[simp]
0 g = 0
@[simp]
theorem GroupCat.one_apply (G : GroupCat) (H : GroupCat) (g : G) :
1 g = 1
def AddGroupCat.ofHom {X : Type u} {Y : Type u} [] [] (f : X →+ Y) :

Typecheck an AddMonoidHom as a morphism in AddGroup.

Equations
Instances For
def GroupCat.ofHom {X : Type u} {Y : Type u} [] [] (f : X →* Y) :

Typecheck a MonoidHom as a morphism in GroupCat.

Equations
Instances For
theorem AddGroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [] [] (f : X →+ Y) (x : X) :
x = f x
theorem GroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [] [] (f : X →* Y) (x : X) :
() x = f x
instance AddGroupCat.ofUnique (G : Type u_1) [] [i : ] :
Unique ()
Equations
instance GroupCat.ofUnique (G : Type u_1) [] [i : ] :
Unique ()
Equations
Type (u + 1)

The category of additive commutative groups and group morphisms.

Equations
Instances For
def CommGroupCat :
Type (u + 1)

The category of commutative groups and group morphisms.

Equations
Instances For
@[reducible, inline]
abbrev Ab :
Type (u_1 + 1)

Ab is an abbreviation for AddCommGroup, for the sake of mathematicians' sanity.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
• X.commGroupInstance = X.str
CoeFun (X Y) fun (x : X Y) => XY
Equations
• AddCommGroupCat.instCoeFunHomForallαAddCommGroup = { coe := fun (f : X →+ Y) => f }
instance CommGroupCat.instCoeFunHomForallαCommGroup {X : CommGroupCat} {Y : CommGroupCat} :
CoeFun (X Y) fun (x : X Y) => XY
Equations
• CommGroupCat.instCoeFunHomForallαCommGroup = { coe := fun (f : X →* Y) => f }
Equations
• X.instFunLike Y = let_fun this := inferInstance; this
instance CommGroupCat.instFunLike (X : CommGroupCat) (Y : CommGroupCat) :
FunLike (X Y) X Y
Equations
• X.instFunLike Y = let_fun this := inferInstance; this
@[simp]
@[simp]
= g f
@[simp]
theorem CommGroupCat.coe_comp {X : CommGroupCat} {Y : CommGroupCat} {Z : CommGroupCat} {f : X Y} {g : Y Z} :
= g f
theorem CommGroupCat.comp_def {X : CommGroupCat} {Y : CommGroupCat} {Z : CommGroupCat} {f : X Y} {g : Y Z} :
@[simp]
= f
@[simp]
theorem CommGroupCat.forget_map {X : CommGroupCat} {Y : CommGroupCat} (f : X Y) :
= f
theorem AddCommGroupCat.ext {X : AddCommGroupCat} {Y : AddCommGroupCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
f = g
theorem CommGroupCat.ext {X : CommGroupCat} {Y : CommGroupCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
f = g

Construct a bundled AddCommGroup from the underlying type and typeclass.

Equations
Instances For

Construct a bundled CommGroup from the underlying type and typeclass.

Equations
Instances For
Equations
Equations
theorem AddCommGroupCat.coe_of (R : Type u) [] :
= R
theorem CommGroupCat.coe_of (R : Type u) [] :
() = R
instance AddCommGroupCat.ofUnique (G : Type u_1) [] [i : ] :
Equations
instance CommGroupCat.ofUnique (G : Type u_1) [] [i : ] :
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
• G.instZeroHom H = inferInstance
Equations
• G.instOneHom H = inferInstance
@[simp]
0 g = 0
@[simp]
theorem CommGroupCat.one_apply (G : CommGroupCat) (H : CommGroupCat) (g : G) :
1 g = 1
def AddCommGroupCat.ofHom {X : Type u} {Y : Type u} [] [] (f : X →+ Y) :

Typecheck an AddMonoidHom as a morphism in AddCommGroup.

Equations
Instances For
def CommGroupCat.ofHom {X : Type u} {Y : Type u} [] [] (f : X →* Y) :

Typecheck a MonoidHom as a morphism in CommGroup.

Equations
Instances For
@[simp]
theorem AddCommGroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [] [] (f : X →+ Y) (x : X) :
= f x
@[simp]
theorem CommGroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [] [] (f : X →* Y) (x : X) :
x = f x

Any element of an abelian group gives a unique morphism from ℤ sending 1 to that element.

Equations
• = () g
Instances For
@[simp]
theorem AddCommGroupCat.asHom_apply {G : AddCommGroupCat} (g : G) (i : ) :
= i g
theorem AddCommGroupCat.int_hom_ext {G : AddCommGroupCat} (f : ) (g : ) (w : f 1 = g 1) :
f = g
X Y

Build an isomorphism in the category AddGroup from an AddEquiv between AddGroups.

Equations
Instances For
@[simp]
theorem MulEquiv.toGroupCatIso_inv {X : GroupCat} {Y : GroupCat} (e : X ≃* Y) :
e.toGroupCatIso.inv = e.symm.toMonoidHom
@[simp]
theorem MulEquiv.toGroupCatIso_hom {X : GroupCat} {Y : GroupCat} (e : X ≃* Y) :
e.toGroupCatIso.hom = e.toMonoidHom
@[simp]
@[simp]
def MulEquiv.toGroupCatIso {X : GroupCat} {Y : GroupCat} (e : X ≃* Y) :
X Y

Build an isomorphism in the category GroupCat from a MulEquiv between Groups.

Equations
• e.toGroupCatIso = { hom := e.toMonoidHom, inv := e.symm.toMonoidHom, hom_inv_id := , inv_hom_id := }
Instances For

Build an isomorphism in the category AddCommGroupCat from an AddEquiv between AddCommGroups.

Equations
Instances For
@[simp]
@[simp]
@[simp]
theorem MulEquiv.toCommGroupCatIso_inv {X : CommGroupCat} {Y : CommGroupCat} (e : X ≃* Y) :
e.toCommGroupCatIso.inv = e.symm.toMonoidHom
@[simp]
theorem MulEquiv.toCommGroupCatIso_hom {X : CommGroupCat} {Y : CommGroupCat} (e : X ≃* Y) :
e.toCommGroupCatIso.hom = e.toMonoidHom
def MulEquiv.toCommGroupCatIso {X : CommGroupCat} {Y : CommGroupCat} (e : X ≃* Y) :
X Y

Build an isomorphism in the category CommGroupCat from a MulEquiv between CommGroups.

Equations
• e.toCommGroupCatIso = { hom := e.toMonoidHom, inv := e.symm.toMonoidHom, hom_inv_id := , inv_hom_id := }
Instances For

Build an addEquiv from an isomorphism in the category AddGroup

Equations
Instances For
def CategoryTheory.Iso.groupIsoToMulEquiv {X : GroupCat} {Y : GroupCat} (i : X Y) :
X ≃* Y

Build a MulEquiv from an isomorphism in the category GroupCat.

Equations
Instances For

Build an AddEquiv from an isomorphism in the category AddCommGroup.

Equations
Instances For
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.Iso.commGroupIsoToMulEquiv_apply {X : CommGroupCat} {Y : CommGroupCat} (i : X Y) (a : X) :
i.commGroupIsoToMulEquiv a = i.hom a
@[simp]
theorem CategoryTheory.Iso.commGroupIsoToMulEquiv_symm_apply {X : CommGroupCat} {Y : CommGroupCat} (i : X Y) (a : Y) :
i.commGroupIsoToMulEquiv.symm a = i.inv a

Build a MulEquiv from an isomorphism in the category CommGroup.

Equations
Instances For
(CategoryTheory.CategoryStruct.comp (fun (i : X Y) => i.addGroupIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddGroupCatIso) =
(CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddGroupCatIso) fun (i : X Y) => i.addGroupIsoToAddEquiv) =
X ≃+ Y X Y

Additive equivalences between AddGroups are the same as (isomorphic to) isomorphisms in AddGroupCat.

Equations
• addEquivIsoAddGroupIso = { hom := fun (e : X ≃+ Y) => e.toAddGroupCatIso, inv := fun (i : X Y) => i.addGroupIsoToAddEquiv, hom_inv_id := , inv_hom_id := }
Instances For
def mulEquivIsoGroupIso {X : GroupCat} {Y : GroupCat} :
X ≃* Y X Y

multiplicative equivalences between Groups are the same as (isomorphic to) isomorphisms in GroupCat

Equations
• mulEquivIsoGroupIso = { hom := fun (e : X ≃* Y) => e.toGroupCatIso, inv := fun (i : X Y) => i.groupIsoToMulEquiv, hom_inv_id := , inv_hom_id := }
Instances For

Additive equivalences between AddCommGroups are the same as (isomorphic to) isomorphisms in AddCommGroupCat.

Equations
• addEquivIsoAddCommGroupIso = { hom := fun (e : X ≃+ Y) => e.toAddCommGroupCatIso, inv := fun (i : X Y) => i.addCommGroupIsoToAddEquiv, hom_inv_id := , inv_hom_id := }
Instances For

Multiplicative equivalences between CommGroups are the same as (isomorphic to) isomorphisms in CommGroupCat.

Equations
• mulEquivIsoCommGroupIso = { hom := fun (e : X ≃* Y) => e.toCommGroupCatIso, inv := fun (i : X Y) => i.commGroupIsoToMulEquiv, hom_inv_id := , inv_hom_id := }
Instances For

The (bundled) group of automorphisms of a type is isomorphic to the (bundled) group of permutations.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The (unbundled) group of automorphisms of a type is MulEquiv to the (unbundled) group of permutations.

Equations
• CategoryTheory.Aut.mulEquivPerm = CategoryTheory.Aut.isoPerm.groupIsoToMulEquiv
Instances For
.ReflectsIsomorphisms
Equations
instance GroupCat.forget_reflects_isos :
.ReflectsIsomorphisms
Equations
.ReflectsIsomorphisms
Equations
instance CommGroupCat.forget_reflects_isos :
.ReflectsIsomorphisms
Equations
abbrev GroupCatMaxAux :
Type ((max u1 u2) + 1)

An alias for AddGroupCat.{max u v}, to deal around unification issues.

Equations
Instances For
@[reducible, inline]
abbrev GroupCatMax :
Type ((max u1 u2) + 1)

An alias for GroupCat.{max u v}, to deal around unification issues.

Equations
Instances For
@[reducible, inline]
Type ((max u1 u2) + 1)

An alias for AddGroupCat.{max u v}, to deal around unification issues.

Equations
Instances For
Type ((max u1 u2) + 1)

An alias for AddCommGroupCat.{max u v}, to deal around unification issues.

Equations
Instances For
@[reducible, inline]
abbrev CommGroupCatMax :
Type ((max u1 u2) + 1)

An alias for CommGroupCat.{max u v}, to deal around unification issues.

Equations
Instances For
@[reducible, inline]
An alias for AddCommGroupCat.{max u v}, to deal around unification issues.