Category instances for Group, AddGroup, CommGroup, and AddCommGroup.

We introduce the bundled categories:

• Grp
• AddGrp
• CommGrp
• AddCommGrp

along with the relevant forgetful functors between them, and to the bundled monoid categories.

structure AddGrp : Type (u + 1)

The category of additive groups and group morphisms.

• carrier : Type u

  The underlying type.

• str : AddGroup ↑self

structure Grp : Type (u + 1)

The category of groups and group morphisms.

• carrier : Type u

  The underlying type.

• str : Group ↑self

instance Grp.instCoeSortType : CoeSort Grp (Type u)

instance AddGrp.instCoeSortType : CoeSort AddGrp (Type u)

@[reducible, inline]

abbrev Grp.of (M : Type u) [Group M] : Grp

Construct a bundled Grp from the underlying type and typeclass.

@[reducible, inline]

abbrev AddGrp.of (M : Type u) [AddGroup M] : AddGrp

Construct a bundled AddGrp from the underlying type and typeclass.

structure AddGrp.Hom (A B : AddGrp) : Type u

The type of morphisms in AddGrp R.

• hom' : ↑A →+ ↑B

  The underlying monoid homomorphism.

theorem AddGrp.Hom.ext_iff {A B : AddGrp} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

theorem AddGrp.Hom.ext {A B : AddGrp} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

structure Grp.Hom (A B : Grp) : Type u

The type of morphisms in Grp R.

• hom' : ↑A →* ↑B

  The underlying monoid homomorphism.

theorem Grp.Hom.ext {A B : Grp} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

theorem Grp.Hom.ext_iff {A B : Grp} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

instance Grp.instCategory : CategoryTheory.Category.{u, u + 1} Grp

instance AddGrp.instCategory : CategoryTheory.Category.{u, u + 1} AddGrp

instance Grp.instConcreteCategoryMonoidHomCarrier : CategoryTheory.ConcreteCategory Grp fun (x1 x2 : Grp) => ↑x1 →* ↑x2

instance AddGrp.instConcreteCategoryAddMonoidHomCarrier : CategoryTheory.ConcreteCategory AddGrp fun (x1 x2 : AddGrp) => ↑x1 →+ ↑x2

@[reducible, inline]

abbrev Grp.Hom.hom {X Y : Grp} (f : X.Hom Y) : ↑X →* ↑Y

Turn a morphism in Grp back into a MonoidHom.

@[reducible, inline]

abbrev AddGrp.Hom.hom {X Y : AddGrp} (f : X.Hom Y) : ↑X →+ ↑Y

Turn a morphism in AddGrp back into an AddMonoidHom.

@[reducible, inline]

abbrev Grp.ofHom {X Y : Type u} [Group X] [Group Y] (f : X →* Y) : of X ⟶ of Y

Typecheck a MonoidHom as a morphism in Grp.

@[reducible, inline]

abbrev AddGrp.ofHom {X Y : Type u} [AddGroup X] [AddGroup Y] (f : X →+ Y) : of X ⟶ of Y

Typecheck an AddMonoidHom as a morphism in AddGrp.

def Grp.Hom.Simps.hom (X Y : Grp) (f : X.Hom Y) : ↑X →* ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem Grp.coe_id {X : Grp} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem AddGrp.coe_id {X : AddGrp} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem Grp.coe_comp {X Y Z : Grp} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem AddGrp.coe_comp {X Y Z : AddGrp} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem Grp.forget_map {X Y : Grp} (f : X ⟶ Y) : (CategoryTheory.forget Grp).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem Grp.ext {X Y : Grp} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem AddGrp.ext {X Y : AddGrp} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem Grp.ext_iff {X Y : Grp} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

theorem AddGrp.ext_iff {X Y : AddGrp} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

theorem Grp.coe_of (R : Type u) [Group R] : ↑(of R) = R

theorem AddGrp.coe_of (R : Type u) [AddGroup R] : ↑(of R) = R

@[simp]

theorem Grp.hom_id {X : Grp} : Hom.hom (CategoryTheory.CategoryStruct.id X) = MonoidHom.id ↑X

@[simp]

theorem AddGrp.hom_id {X : AddGrp} : Hom.hom (CategoryTheory.CategoryStruct.id X) = AddMonoidHom.id ↑X

theorem Grp.id_apply (X : Grp) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

theorem AddGrp.id_apply (X : AddGrp) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

@[simp]

theorem Grp.hom_comp {X Y T : Grp} (f : X ⟶ Y) (g : Y ⟶ T) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

@[simp]

theorem AddGrp.hom_comp {X Y T : AddGrp} (f : X ⟶ Y) (g : Y ⟶ T) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem Grp.comp_apply {X Y T : Grp} (f : X ⟶ Y) (g : Y ⟶ T) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem AddGrp.comp_apply {X Y T : AddGrp} (f : X ⟶ Y) (g : Y ⟶ T) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem Grp.hom_ext {X Y : Grp} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

theorem AddGrp.hom_ext {X Y : AddGrp} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

theorem AddGrp.hom_ext_iff {X Y : AddGrp} {f g : X ⟶ Y} : f = g ↔ Hom.hom f = Hom.hom g

theorem Grp.hom_ext_iff {X Y : Grp} {f g : X ⟶ Y} : f = g ↔ Hom.hom f = Hom.hom g

@[simp]

theorem Grp.hom_ofHom {R S : Type u} [Group R] [Group S] (f : R →* S) : Hom.hom (ofHom f) = f

@[simp]

theorem AddGrp.hom_ofHom {R S : Type u} [AddGroup R] [AddGroup S] (f : R →+ S) : Hom.hom (ofHom f) = f

@[simp]

theorem Grp.ofHom_hom {X Y : Grp} (f : X ⟶ Y) : ofHom (Hom.hom f) = f

@[simp]

theorem AddGrp.ofHom_hom {X Y : AddGrp} (f : X ⟶ Y) : ofHom (Hom.hom f) = f

@[simp]

theorem Grp.ofHom_id {X : Type u} [Group X] : ofHom (MonoidHom.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem AddGrp.ofHom_id {X : Type u} [AddGroup X] : ofHom (AddMonoidHom.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem Grp.ofHom_comp {X Y Z : Type u} [Group X] [Group Y] [Group Z] (f : X →* Y) (g : Y →* Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

@[simp]

theorem AddGrp.ofHom_comp {X Y Z : Type u} [AddGroup X] [AddGroup Y] [AddGroup Z] (f : X →+ Y) (g : Y →+ Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem Grp.ofHom_apply {X Y : Type u} [Group X] [Group Y] (f : X →* Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem AddGrp.ofHom_apply {X Y : Type u} [AddGroup X] [AddGroup Y] (f : X →+ Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem Grp.inv_hom_apply {X Y : Grp} (e : X ≅ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem AddGrp.neg_hom_apply {X Y : AddGrp} (e : X ≅ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem Grp.hom_inv_apply {X Y : Grp} (e : X ≅ Y) (s : ↑Y) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

theorem AddGrp.hom_neg_apply {X Y : AddGrp} (e : X ≅ Y) (s : ↑Y) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

instance Grp.instInhabited : Inhabited Grp

instance AddGrp.instInhabited : Inhabited AddGrp

instance Grp.hasForgetToMonCat : CategoryTheory.HasForget₂ Grp MonCat

instance AddGrp.hasForgetToAddMonCat : CategoryTheory.HasForget₂ AddGrp AddMonCat

@[simp]

theorem Grp.forget₂_map_ofHom {X Y : Type u} [Group X] [Group Y] (f : X →* Y) : (CategoryTheory.forget₂ Grp MonCat).map (ofHom f) = MonCat.ofHom f

@[simp]

theorem AddGrp.forget₂_map_ofHom {X Y : Type u} [AddGroup X] [AddGroup Y] (f : X →+ Y) : (CategoryTheory.forget₂ AddGrp AddMonCat).map (ofHom f) = AddMonCat.ofHom f

instance Grp.instCoeMonCat : Coe Grp MonCat

instance AddGrp.instCoeMonCat : Coe AddGrp AddMonCat

instance Grp.instOneHom (G H : Grp) : One (G ⟶ H)

instance AddGrp.instZeroHom (G H : AddGrp) : Zero (G ⟶ H)

@[simp]

theorem Grp.one_apply (G H : Grp) (g : ↑G) : (CategoryTheory.ConcreteCategory.hom 1) g = 1

@[simp]

theorem AddGrp.zero_apply (G H : AddGrp) (g : ↑G) : (CategoryTheory.ConcreteCategory.hom 0) g = 0

theorem Grp.ofHom_injective {X Y : Type u} [Group X] [Group Y] : Function.Injective fun (f : X →* Y) => ofHom f

theorem AddGrp.ofHom_injective {X Y : Type u} [AddGroup X] [AddGroup Y] : Function.Injective fun (f : X →+ Y) => ofHom f

def Grp.fullyFaithfulForget₂ToMonCat : (CategoryTheory.forget₂ Grp MonCat).FullyFaithful

The forgetful functor from groups to monoids is fully faithful.

def AddGrp.fullyFaihtfulForget₂ToAddMonCat : (CategoryTheory.forget₂ AddGrp AddMonCat).FullyFaithful

The forgetful functor from additive groups to additive monoids is fully faithful.

instance Grp.instFullMonCatForget₂ : (CategoryTheory.forget₂ Grp MonCat).Full

instance AddGrp.instFullMonCatForget₂ : (CategoryTheory.forget₂ AddGrp AddMonCat).Full

def Grp.uliftFunctor : CategoryTheory.Functor Grp Grp

Universe lift functor for groups.

def AddGrp.uliftFunctor : CategoryTheory.Functor AddGrp AddGrp

Universe lift functor for additive groups.

@[simp]

theorem Grp.uliftFunctor_obj (X : Grp) : uliftFunctor.obj X = of (ULift.{u, v} ↑X)

@[simp]

theorem Grp.uliftFunctor_map {x✝ x✝¹ : Grp} (f : x✝ ⟶ x✝¹) : uliftFunctor.map f = ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom))

@[simp]

theorem AddGrp.uliftFunctor_obj (X : AddGrp) : uliftFunctor.obj X = of (ULift.{u, v} ↑X)

@[simp]

theorem AddGrp.uliftFunctor_map {x✝ x✝¹ : AddGrp} (f : x✝ ⟶ x✝¹) : uliftFunctor.map f = ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp ((Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom))

structure AddCommGrp : Type (u + 1)

The category of additive groups and group morphisms.

• carrier : Type u

  The underlying type.

• str : AddCommGroup ↑self

structure CommGrp : Type (u + 1)

The category of groups and group morphisms.

• carrier : Type u

  The underlying type.

• str : CommGroup ↑self

@[reducible, inline]

abbrev Ab : Type (u_1 + 1)

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

instance CommGrp.instCoeSortType : CoeSort CommGrp (Type u)

instance AddCommGrp.instCoeSortType : CoeSort AddCommGrp (Type u)

@[reducible, inline]

abbrev CommGrp.of (M : Type u) [CommGroup M] : CommGrp

Construct a bundled CommGrp from the underlying type and typeclass.

@[reducible, inline]

abbrev AddCommGrp.of (M : Type u) [AddCommGroup M] : AddCommGrp

Construct a bundled AddCommGrp from the underlying type and typeclass.

structure AddCommGrp.Hom (A B : AddCommGrp) : Type u

The type of morphisms in AddCommGrp R.

• hom' : ↑A →+ ↑B

  The underlying monoid homomorphism.

theorem AddCommGrp.Hom.ext_iff {A B : AddCommGrp} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

theorem AddCommGrp.Hom.ext {A B : AddCommGrp} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

structure CommGrp.Hom (A B : CommGrp) : Type u

The type of morphisms in CommGrp R.

• hom' : ↑A →* ↑B

  The underlying monoid homomorphism.

theorem CommGrp.Hom.ext {A B : CommGrp} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

theorem CommGrp.Hom.ext_iff {A B : CommGrp} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

instance CommGrp.instCategory : CategoryTheory.Category.{u, u + 1} CommGrp

instance AddCommGrp.instCategory : CategoryTheory.Category.{u, u + 1} AddCommGrp

instance CommGrp.instConcreteCategoryMonoidHomCarrier : CategoryTheory.ConcreteCategory CommGrp fun (x1 x2 : CommGrp) => ↑x1 →* ↑x2

instance AddCommGrp.instConcreteCategoryAddMonoidHomCarrier : CategoryTheory.ConcreteCategory AddCommGrp fun (x1 x2 : AddCommGrp) => ↑x1 →+ ↑x2

@[reducible, inline]

abbrev CommGrp.Hom.hom {X Y : CommGrp} (f : X.Hom Y) : ↑X →* ↑Y

Turn a morphism in CommGrp back into a MonoidHom.

@[reducible, inline]

abbrev AddCommGrp.Hom.hom {X Y : AddCommGrp} (f : X.Hom Y) : ↑X →+ ↑Y

Turn a morphism in AddCommGrp back into an AddMonoidHom.

@[reducible, inline]

abbrev CommGrp.ofHom {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) : of X ⟶ of Y

Typecheck a MonoidHom as a morphism in CommGrp.

@[reducible, inline]

abbrev AddCommGrp.ofHom {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] (f : X →+ Y) : of X ⟶ of Y

Typecheck an AddMonoidHom as a morphism in AddCommGrp.

def CommGrp.Hom.Simps.hom (X Y : CommGrp) (f : X.Hom Y) : ↑X →* ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

def AddCommGrp.Hom.Simps.hom (X Y : AddCommGrp) (f : X.Hom Y) : ↑X →+ ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem CommGrp.coe_id {X : CommGrp} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem AddCommGrp.coe_id {X : AddCommGrp} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem CommGrp.coe_comp {X Y Z : CommGrp} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem AddCommGrp.coe_comp {X Y Z : AddCommGrp} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem CommGrp.forget_map {X Y : CommGrp} (f : X ⟶ Y) : (CategoryTheory.forget CommGrp).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem AddCommGrp.forget_map {X Y : AddCommGrp} (f : X ⟶ Y) : (CategoryTheory.forget AddCommGrp).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem CommGrp.ext {X Y : CommGrp} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem AddCommGrp.ext {X Y : AddCommGrp} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem CommGrp.ext_iff {X Y : CommGrp} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

theorem AddCommGrp.ext_iff {X Y : AddCommGrp} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

instance CommGrp.instInhabited : Inhabited CommGrp

instance AddCommGrp.instInhabited : Inhabited AddCommGrp

theorem CommGrp.coe_of (R : Type u) [CommGroup R] : ↑(of R) = R

theorem AddCommGrp.coe_of (R : Type u) [AddCommGroup R] : ↑(of R) = R

@[simp]

theorem CommGrp.hom_id {X : CommGrp} : Hom.hom (CategoryTheory.CategoryStruct.id X) = MonoidHom.id ↑X

@[simp]

theorem AddCommGrp.hom_id {X : AddCommGrp} : Hom.hom (CategoryTheory.CategoryStruct.id X) = AddMonoidHom.id ↑X

theorem CommGrp.id_apply (X : CommGrp) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

theorem AddCommGrp.id_apply (X : AddCommGrp) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

@[simp]

theorem CommGrp.hom_comp {X Y T : CommGrp} (f : X ⟶ Y) (g : Y ⟶ T) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

@[simp]

theorem AddCommGrp.hom_comp {X Y T : AddCommGrp} (f : X ⟶ Y) (g : Y ⟶ T) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem CommGrp.comp_apply {X Y T : CommGrp} (f : X ⟶ Y) (g : Y ⟶ T) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem AddCommGrp.comp_apply {X Y T : AddCommGrp} (f : X ⟶ Y) (g : Y ⟶ T) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem CommGrp.hom_ext {X Y : CommGrp} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

theorem AddCommGrp.hom_ext {X Y : AddCommGrp} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

theorem CommGrp.hom_ext_iff {X Y : CommGrp} {f g : X ⟶ Y} : f = g ↔ Hom.hom f = Hom.hom g

theorem AddCommGrp.hom_ext_iff {X Y : AddCommGrp} {f g : X ⟶ Y} : f = g ↔ Hom.hom f = Hom.hom g

@[simp]

theorem CommGrp.hom_ofHom {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) : Hom.hom (ofHom f) = f

@[simp]

theorem AddCommGrp.hom_ofHom {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] (f : X →+ Y) : Hom.hom (ofHom f) = f

@[simp]

theorem CommGrp.ofHom_hom {X Y : CommGrp} (f : X ⟶ Y) : ofHom (Hom.hom f) = f

@[simp]

theorem AddCommGrp.ofHom_hom {X Y : AddCommGrp} (f : X ⟶ Y) : ofHom (Hom.hom f) = f

@[simp]

theorem CommGrp.ofHom_id {X : Type u} [CommGroup X] : ofHom (MonoidHom.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem AddCommGrp.ofHom_id {X : Type u} [AddCommGroup X] : ofHom (AddMonoidHom.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem CommGrp.ofHom_comp {X Y Z : Type u} [CommGroup X] [CommGroup Y] [CommGroup Z] (f : X →* Y) (g : Y →* Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

@[simp]

theorem AddCommGrp.ofHom_comp {X Y Z : Type u} [AddCommGroup X] [AddCommGroup Y] [AddCommGroup Z] (f : X →+ Y) (g : Y →+ Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem CommGrp.ofHom_apply {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem AddCommGrp.ofHom_apply {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] (f : X →+ Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem CommGrp.inv_hom_apply {X Y : CommGrp} (e : X ≅ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem AddCommGrp.neg_hom_apply {X Y : AddCommGrp} (e : X ≅ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem CommGrp.hom_inv_apply {X Y : CommGrp} (e : X ≅ Y) (s : ↑Y) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

theorem AddCommGrp.hom_neg_apply {X Y : AddCommGrp} (e : X ≅ Y) (s : ↑Y) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

instance CommGrp.hasForgetToGroup : CategoryTheory.HasForget₂ CommGrp Grp

instance AddCommGrp.hasForgetToAddGroup : CategoryTheory.HasForget₂ AddCommGrp AddGrp

@[simp]

theorem CommGrp.forget₂_grp_map_ofHom {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) : (CategoryTheory.forget₂ CommGrp Grp).map (ofHom f) = Grp.ofHom f

@[simp]

theorem AddCommGrp.forget₂_addGrp_map_ofHom {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] (f : X →+ Y) : (CategoryTheory.forget₂ AddCommGrp AddGrp).map (ofHom f) = AddGrp.ofHom f

instance CommGrp.instCoeGrp : Coe CommGrp Grp

instance AddCommGrp.instCoeAddGrp : Coe AddCommGrp AddGrp

def CommGrp.fullyFaithfulForget₂ToGrp : (CategoryTheory.forget₂ CommGrp Grp).FullyFaithful

The forgetful functor from commutative groups to groups is fully faithful.

def AddCommGrp.fullyFaihtfulForget₂ToAddGrp : (CategoryTheory.forget₂ AddCommGrp AddGrp).FullyFaithful

The forgetful functor from additive commutative groups to additive groups is fully faithful.

instance CommGrp.instFullGrpForget₂ : (CategoryTheory.forget₂ CommGrp Grp).Full

instance AddCommGrp.instFullAddGrpForget₂ : (CategoryTheory.forget₂ AddCommGrp AddGrp).Full

instance CommGrp.hasForgetToCommMonCat : CategoryTheory.HasForget₂ CommGrp CommMonCat

instance AddCommGrp.hasForgetToAddCommMonCat : CategoryTheory.HasForget₂ AddCommGrp AddCommMonCat

@[simp]

theorem CommGrp.forget₂_commMonCat_map_ofHom {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) : (CategoryTheory.forget₂ CommGrp CommMonCat).map (ofHom f) = CommMonCat.ofHom f

@[simp]

theorem AddCommGrp.forget₂_commMonCat_map_ofHom {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] (f : X →+ Y) : (CategoryTheory.forget₂ AddCommGrp AddCommMonCat).map (ofHom f) = AddCommMonCat.ofHom f

instance CommGrp.instCoeCommMonCat : Coe CommGrp CommMonCat

instance AddCommGrp.instCoeCommMonCat : Coe AddCommGrp AddCommMonCat

instance CommGrp.instOneHom (G H : CommGrp) : One (G ⟶ H)

instance AddCommGrp.instZeroHom (G H : AddCommGrp) : Zero (G ⟶ H)

@[simp]

theorem CommGrp.one_apply (G H : CommGrp) (g : ↑G) : (CategoryTheory.ConcreteCategory.hom 1) g = 1

@[simp]

theorem AddCommGrp.zero_apply (G H : AddCommGrp) (g : ↑G) : (CategoryTheory.ConcreteCategory.hom 0) g = 0

theorem CommGrp.ofHom_injective {X Y : Type u} [CommGroup X] [CommGroup Y] : Function.Injective fun (f : X →* Y) => ofHom f

theorem AddCommGrp.ofHom_injective {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] : Function.Injective fun (f : X →+ Y) => ofHom f

def CommGrp.uliftFunctor : CategoryTheory.Functor CommGrp CommGrp

Universe lift functor for commutative groups.

def AddCommGrp.uliftFunctor : CategoryTheory.Functor AddCommGrp AddCommGrp

Universe lift functor for additive commutative groups.

@[simp]

theorem CommGrp.uliftFunctor_map {x✝ x✝¹ : CommGrp} (f : x✝ ⟶ x✝¹) : uliftFunctor.map f = ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom))

@[simp]

theorem AddCommGrp.uliftFunctor_map {x✝ x✝¹ : AddCommGrp} (f : x✝ ⟶ x✝¹) : uliftFunctor.map f = ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp ((Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom))

@[simp]

theorem CommGrp.uliftFunctor_obj (X : CommGrp) : uliftFunctor.obj X = of (ULift.{u, v} ↑X)

@[simp]

theorem AddCommGrp.uliftFunctor_obj (X : AddCommGrp) : uliftFunctor.obj X = of (ULift.{u, v} ↑X)

def AddCommGrp.asHom {G : AddCommGrp} (g : ↑G) : of ℤ ⟶ G

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

@[simp]

theorem AddCommGrp.asHom_hom_apply {G : AddCommGrp} (g : ↑G) (n : ℤ) : (Hom.hom (asHom g)) n = n • g

theorem AddCommGrp.asHom_injective {G : AddCommGrp} : Function.Injective asHom

theorem AddCommGrp.int_hom_ext {G : AddCommGrp} (f g : of ℤ ⟶ G) (w : (CategoryTheory.ConcreteCategory.hom f) 1 = (CategoryTheory.ConcreteCategory.hom g) 1) : f = g

theorem AddCommGrp.int_hom_ext_iff {G : AddCommGrp} {f g : of ℤ ⟶ G} : f = g ↔ (CategoryTheory.ConcreteCategory.hom f) 1 = (CategoryTheory.ConcreteCategory.hom g) 1

theorem AddCommGrp.injective_of_mono {G H : AddCommGrp} (f : G ⟶ H) [CategoryTheory.Mono f] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)

def MulEquiv.toGrpIso {X Y : Grp} (e : ↑X ≃* ↑Y) : X ≅ Y

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

def AddEquiv.toAddGrpIso {X Y : AddGrp} (e : ↑X ≃+ ↑Y) : X ≅ Y

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

@[simp]

theorem MulEquiv.toGrpIso_hom {X Y : Grp} (e : ↑X ≃* ↑Y) : e.toGrpIso.hom = Grp.ofHom e.toMonoidHom

@[simp]

theorem AddEquiv.toAddGrpIso_inv {X Y : AddGrp} (e : ↑X ≃+ ↑Y) : e.toAddGrpIso.inv = AddGrp.ofHom e.symm.toAddMonoidHom

@[simp]

theorem MulEquiv.toGrpIso_inv {X Y : Grp} (e : ↑X ≃* ↑Y) : e.toGrpIso.inv = Grp.ofHom e.symm.toMonoidHom

@[simp]

theorem AddEquiv.toAddGrpIso_hom {X Y : AddGrp} (e : ↑X ≃+ ↑Y) : e.toAddGrpIso.hom = AddGrp.ofHom e.toAddMonoidHom

def MulEquiv.toCommGrpIso {X Y : CommGrp} (e : ↑X ≃* ↑Y) : X ≅ Y

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

def AddEquiv.toAddCommGrpIso {X Y : AddCommGrp} (e : ↑X ≃+ ↑Y) : X ≅ Y

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

@[simp]

theorem AddEquiv.toAddCommGrpIso_hom {X Y : AddCommGrp} (e : ↑X ≃+ ↑Y) : e.toAddCommGrpIso.hom = AddCommGrp.ofHom e.toAddMonoidHom

@[simp]

theorem AddEquiv.toAddCommGrpIso_inv {X Y : AddCommGrp} (e : ↑X ≃+ ↑Y) : e.toAddCommGrpIso.inv = AddCommGrp.ofHom e.symm.toAddMonoidHom

@[simp]

theorem MulEquiv.toCommGrpIso_inv {X Y : CommGrp} (e : ↑X ≃* ↑Y) : e.toCommGrpIso.inv = CommGrp.ofHom e.symm.toMonoidHom

@[simp]

theorem MulEquiv.toCommGrpIso_hom {X Y : CommGrp} (e : ↑X ≃* ↑Y) : e.toCommGrpIso.hom = CommGrp.ofHom e.toMonoidHom

def CategoryTheory.Iso.groupIsoToMulEquiv {X Y : Grp} (i : X ≅ Y) : ↑X ≃* ↑Y

Build a MulEquiv from an isomorphism in the category Grp.

def CategoryTheory.Iso.addGroupIsoToAddEquiv {X Y : AddGrp} (i : X ≅ Y) : ↑X ≃+ ↑Y

Build an addEquiv from an isomorphism in the category AddGroup

def CategoryTheory.Iso.commGroupIsoToMulEquiv {X Y : CommGrp} (i : X ≅ Y) : ↑X ≃* ↑Y

Build a MulEquiv from an isomorphism in the category CommGroup.

def CategoryTheory.Iso.addCommGroupIsoToAddEquiv {X Y : AddCommGrp} (i : X ≅ Y) : ↑X ≃+ ↑Y

Build an AddEquiv from an isomorphism in the category AddCommGroup.

@[simp]

theorem CategoryTheory.Iso.addCommGroupIsoToAddEquiv_symm_apply {X Y : AddCommGrp} (i : X ≅ Y) (a : ↑Y) : i.addCommGroupIsoToAddEquiv.symm a = (AddCommGrp.Hom.hom i.inv) a

@[simp]

theorem CategoryTheory.Iso.addCommGroupIsoToAddEquiv_apply {X Y : AddCommGrp} (i : X ≅ Y) (a : ↑X) : i.addCommGroupIsoToAddEquiv a = (AddCommGrp.Hom.hom i.hom) a

@[simp]

theorem CategoryTheory.Iso.commGroupIsoToMulEquiv_apply {X Y : CommGrp} (i : X ≅ Y) (a : ↑X) : i.commGroupIsoToMulEquiv a = (CommGrp.Hom.hom i.hom) a

@[simp]

theorem CategoryTheory.Iso.commGroupIsoToMulEquiv_symm_apply {X Y : CommGrp} (i : X ≅ Y) (a : ↑Y) : i.commGroupIsoToMulEquiv.symm a = (CommGrp.Hom.hom i.inv) a

def mulEquivIsoGroupIso {X Y : Grp} : ↑X ≃* ↑Y ≅ X ≅ Y

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

def addEquivIsoAddGroupIso {X Y : AddGrp} : ↑X ≃+ ↑Y ≅ X ≅ Y

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

def mulEquivIsoCommGroupIso {X Y : CommGrp} : ↑X ≃* ↑Y ≅ X ≅ Y

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

def addEquivIsoAddCommGroupIso {X Y : AddCommGrp} : ↑X ≃+ ↑Y ≅ X ≅ Y

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

def CategoryTheory.Aut.isoPerm {α : Type u} : Grp.of (Aut α) ≅ Grp.of (Equiv.Perm α)

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

def CategoryTheory.Aut.mulEquivPerm {α : Type u} : Aut α ≃* Equiv.Perm α

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

instance Grp.forget_reflects_isos : (CategoryTheory.forget Grp).ReflectsIsomorphisms

instance AddGrp.forget_reflects_isos : (CategoryTheory.forget AddGrp).ReflectsIsomorphisms

instance CommGrp.forget_reflects_isos : (CategoryTheory.forget CommGrp).ReflectsIsomorphisms

instance AddCommGrp.forget_reflects_isos : (CategoryTheory.forget AddCommGrp).ReflectsIsomorphisms

@[reducible, inline]

abbrev GrpMax : Type ((max u1 u2) + 1)

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

@[reducible, inline]

abbrev GrpMaxAux : Type ((max u1 u2) + 1)

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

@[reducible, inline]

abbrev AddGrpMax : Type ((max u1 u2) + 1)

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

@[reducible, inline]

abbrev CommGrpMax : Type ((max u1 u2) + 1)

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

@[reducible, inline]

abbrev AddCommGrpMaxAux : Type ((max u1 u2) + 1)

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

@[reducible, inline]

abbrev AddCommGrpMax : Type ((max u1 u2) + 1)

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

Deprecated lemmas for MonoidHom.comp and categorical identities.

@[deprecated "Proven by `simp only [Grp.hom_id, comp_id]`" (since := "2025-01-28")]

theorem MonoidHom.comp_id_grp {G : Grp} {H : Type u} [Monoid H] (f : ↑G →* H) : f.comp (Grp.Hom.hom (CategoryTheory.CategoryStruct.id G)) = f

@[deprecated "Proven by `simp only [Grp.hom_id, comp_id]`" (since := "2025-01-28")]

theorem AddMonoidHom.comp_id_addGrp {G : AddGrp} {H : Type u} [AddMonoid H] (f : ↑G →+ H) : f.comp (AddGrp.Hom.hom (CategoryTheory.CategoryStruct.id G)) = f

@[deprecated "Proven by `simp only [Grp.hom_id, id_comp]`" (since := "2025-01-28")]

theorem MonoidHom.id_grp_comp {G : Type u} [Monoid G] {H : Grp} (f : G →* ↑H) : (Grp.Hom.hom (CategoryTheory.CategoryStruct.id H)).comp f = f

@[deprecated "Proven by `simp only [Grp.hom_id, id_comp]`" (since := "2025-01-28")]

theorem AddMonoidHom.id_addGrp_comp {G : Type u} [AddMonoid G] {H : AddGrp} (f : G →+ ↑H) : (AddGrp.Hom.hom (CategoryTheory.CategoryStruct.id H)).comp f = f

@[deprecated "Proven by `simp only [CommGrp.hom_id, comp_id]`" (since := "2025-01-28")]

theorem MonoidHom.comp_id_commGrp {G : CommGrp} {H : Type u} [Monoid H] (f : ↑G →* H) : f.comp (CommGrp.Hom.hom (CategoryTheory.CategoryStruct.id G)) = f

@[deprecated "Proven by `simp only [CommGrp.hom_id, comp_id]`" (since := "2025-01-28")]

theorem AddMonoidHom.comp_id_addCommGrp {G : AddCommGrp} {H : Type u} [AddMonoid H] (f : ↑G →+ H) : f.comp (AddCommGrp.Hom.hom (CategoryTheory.CategoryStruct.id G)) = f

@[deprecated "Proven by `simp only [CommGrp.hom_id, id_comp]`" (since := "2025-01-28")]

theorem MonoidHom.id_commGrp_comp {G : Type u} [Monoid G] {H : CommGrp} (f : G →* ↑H) : (CommGrp.Hom.hom (CategoryTheory.CategoryStruct.id H)).comp f = f

@[deprecated "Proven by `simp only [CommGrp.hom_id, id_comp]`" (since := "2025-01-28")]

theorem AddMonoidHom.id_addCommGrp_comp {G : Type u} [AddMonoid G] {H : AddCommGrp} (f : G →+ ↑H) : (AddCommGrp.Hom.hom (CategoryTheory.CategoryStruct.id H)).comp f = f