# 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

Instances For
def GroupCat :
Type (u + 1)

The category of groups and group morphisms.

Instances For
FunLike (X Y) X fun x => Y
instance GroupCat.FunLike_instance (X : GroupCat) (Y : GroupCat) :
FunLike (X Y) X fun x => Y
@[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) :
().map 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.

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

Construct a bundled Group from the underlying type and typeclass.

Instances For
@[simp]
theorem AddGroupCat.coe_of (R : Type u) [] :
↑() = R
@[simp]
theorem GroupCat.coe_of (R : Type u) [] :
↑() = R
@[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.

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

Typecheck a MonoidHom as a morphism in GroupCat.

Instances For
@[simp]
theorem AddGroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [] [] (f : X →+ Y) (x : X) :
↑() x = f x
@[simp]
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 ↑()
instance GroupCat.ofUnique (G : Type u_1) [] [i : ] :
Unique ↑()
Type (u + 1)

The category of additive commutative groups and group morphisms.

Instances For
def CommGroupCat :
Type (u + 1)

The category of commutative groups and group morphisms.

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

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

Instances For
instance CommGroupCat.FunLike_instance (X : CommGroupCat) (Y : CommGroupCat) :
FunLike (X Y) X fun x => Y
@[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.

Instances For

Construct a bundled CommGroup from the underlying type and typeclass.

Instances For
theorem AddCommGroupCat.coe_of (R : Type u) [] :
↑() = R
theorem CommGroupCat.coe_of (R : Type u) [] :
↑() = R
instance AddCommGroupCat.ofUnique (G : Type u_1) [] [i : ] :
instance CommGroupCat.ofUnique (G : Type u_1) [] [i : ] :
@[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.

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

Typecheck a MonoidHom as a morphism in CommGroup.

Instances For
@[simp]
theorem AddCommGroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [] [] (f : X →+ Y) (x : 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.

Instances For
@[simp]
theorem AddCommGroupCat.asHom_apply {G : AddCommGroupCat} (g : G) (i : ) :
↑() 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.

Instances For
@[simp]
@[simp]
theorem MulEquiv.toGroupCatIso_inv {X : GroupCat} {Y : GroupCat} (e : X ≃* Y) :
@[simp]
theorem MulEquiv.toGroupCatIso_hom {X : GroupCat} {Y : GroupCat} (e : X ≃* Y) :
@[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.

Instances For

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

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

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

Instances For

Build an addEquiv from an isomorphism in the category AddGroup

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.

Instances For

Build an AddEquiv from an isomorphism in the category AddCommGroup.

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

Build a MulEquiv from an isomorphism in the category CommGroup.

Instances For
X ≃+ Y X Y

"additive equivalences between add_groups are the same as (isomorphic to) isomorphisms in AddGroup

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

Instances For

additive equivalences between AddCommGroups are the same as (isomorphic to) isomorphisms in AddCommGroup

Instances For

multiplicative equivalences between comm_groups are the same as (isomorphic to) isomorphisms in CommGroup

Instances For

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

Instances For

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

Instances For
abbrev GroupCatMaxAux :
Type ((max u1 u2) + 1)

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

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

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

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

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

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

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

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

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

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