Documentation

Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup

Equivalence between Group and AddGroup #

This file contains two equivalences:

The functor GrpAddGrp by sending X ↦ Additive X and f ↦ f.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Grp.toAddGrp_map {x✝ x✝¹ : Grp} (f : x✝ x✝¹) :
@[simp]
theorem Grp.toAddGrp_obj_coe (X : Grp) :
(toAddGrp.obj X) = Additive X

The functor CommGrpAddCommGrp by sending X ↦ Additive X and f ↦ f.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]

The functor AddGrpGrp by sending X ↦ Multiplicative Y and f ↦ f.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
@[simp]
theorem AddGrp.toGrp_map {x✝ x✝¹ : AddGrp} (f : x✝ x✝¹) :

The functor AddCommGrpCommGrp by sending X ↦ Multiplicative Y and f ↦ f.

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

The equivalence of categories between Grp and AddGrp

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

The equivalence of categories between CommGrp and AddCommGrp.

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