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

We introduce the bundled categories:

• GrpCat
• AddGrpCat
• CommGrpCat
• AddCommGrpCat

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

structure AddGrpCat : Type (u + 1)

The category of additive groups and group morphisms.

• carrier : Type u

  The underlying type.

• str : AddGroup ↑self

structure GrpCat : Type (u + 1)

The category of groups and group morphisms.

• carrier : Type u

  The underlying type.

• str : Group ↑self

@[instance_reducible]

instance GrpCat.instCoeSortType : CoeSort GrpCat (Type u)

Equations

• GrpCat.instCoeSortType = { coe := GrpCat.carrier }

@[instance_reducible]

instance AddGrpCat.instCoeSortType : CoeSort AddGrpCat (Type u)

Equations

• AddGrpCat.instCoeSortType = { coe := AddGrpCat.carrier }

@[reducible, inline]

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

Construct a bundled GrpCat from the underlying type and typeclass.

Equations

• ↧M = { carrier := M, str := inst✝ }

@[reducible, inline]

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

Construct a bundled AddGrpCat from the underlying type and typeclass.

Equations

• ↧M = { carrier := M, str := inst✝ }

def AddGrpCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prints AddGrpCat.of X as ↧X.

Equations

• AddGrpCat.delabOf = CategoryTheory.delabOf

def GrpCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prints GrpCat.of X as ↧X.

Equations

• GrpCat.delabOf = CategoryTheory.delabOf

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

The type of morphisms in AddGrpCat R.

• _mkInternal :: (
• hom' : ↑A →+ ↑B

  The underlying monoid homomorphism.

• )

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

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

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

The type of morphisms in GrpCat R.

• _mkInternal :: (
• hom' : ↑A →* ↑B

  The underlying monoid homomorphism.

• )

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

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[reducible, inline]

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

Turn a morphism in GrpCat back into a MonoidHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

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

Turn a morphism in AddGrpCat back into an AddMonoidHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

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

Typecheck a MonoidHom as a morphism in GrpCat.

Equations

• GrpCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

@[reducible, inline]

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

Typecheck an AddMonoidHom as a morphism in AddGrpCat.

Equations

• AddGrpCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

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

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

Equations

• GrpCat.Hom.Simps.hom X Y f = f.hom

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem GrpCat.coe_of (R : Type u) [Group R] : ↑↧R = R

theorem AddGrpCat.coe_of (R : Type u) [AddGroup R] : ↑↧R = R

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem GrpCat.comp_apply {X Y T : GrpCat} (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 AddGrpCat.comp_apply {X Y T : AddGrpCat} (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 GrpCat.hom_ext {X Y : GrpCat} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem GrpCat.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 AddGrpCat.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 GrpCat.ofHom_apply {X Y : Type u} [Group X] [Group Y] (f : X →* Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

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

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

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

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

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

@[instance_reducible]

instance GrpCat.instInhabited : Inhabited GrpCat

Equations

• GrpCat.instInhabited = { default := ↧PUnit.{?u.1 + 1} }

@[instance_reducible]

instance AddGrpCat.instInhabited : Inhabited AddGrpCat

Equations

• AddGrpCat.instInhabited = { default := ↧PUnit.{?u.1 + 1} }

@[instance_reducible]

instance GrpCat.hasForgetToMonCat : CategoryTheory.HasForget₂ GrpCat MonCat

Equations

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

@[instance_reducible]

instance AddGrpCat.hasForgetToAddMonCat : CategoryTheory.HasForget₂ AddGrpCat AddMonCat

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem GrpCat.forget₂_map {R S : GrpCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ GrpCat MonCat).obj R)) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ GrpCat MonCat).map f)) x = (CategoryTheory.ConcreteCategory.hom f) x

@[simp]

theorem AddGrpCat.forget₂_map {R S : AddGrpCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ AddGrpCat AddMonCat).obj R)) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ AddGrpCat AddMonCat).map f)) x = (CategoryTheory.ConcreteCategory.hom f) x

@[instance_reducible]

instance GrpCat.instCoeMonCat : Coe GrpCat MonCat

Equations

• GrpCat.instCoeMonCat = { coe := (CategoryTheory.forget₂ GrpCat MonCat).obj }

@[instance_reducible]

instance AddGrpCat.instCoeMonCat : Coe AddGrpCat AddMonCat

Equations

• AddGrpCat.instCoeMonCat = { coe := (CategoryTheory.forget₂ AddGrpCat AddMonCat).obj }

@[instance_reducible]

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

Equations

• G.instOneHom H = { one := GrpCat.ofHom 1 }

@[instance_reducible]

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

Equations

• G.instZeroHom H = { zero := AddGrpCat.ofHom 0 }

@[simp]

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

@[simp]

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

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

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

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

The forgetful functor from groups to monoids is fully faithful.

Equations

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

def AddGrpCat.fullyFaithfulForget₂ToAddMonCat : (CategoryTheory.forget₂ AddGrpCat AddMonCat).FullyFaithful

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

Equations

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

@[reducible, inline, deprecated AddGrpCat.fullyFaithfulForget₂ToAddMonCat (since := "2026-10-13")]

abbrev AddGrpCat.fullyFaihtfulForget₂ToAddMonCat : (CategoryTheory.forget₂ AddGrpCat AddMonCat).FullyFaithful

Deprecated alias for AddGrpCat.fullyFaithfulForget₂ToAddMonCat.

Equations

• AddGrpCat.fullyFaihtfulForget₂ToAddMonCat = AddGrpCat.fullyFaithfulForget₂ToAddMonCat

instance GrpCat.instFullMonCatForget₂MonoidHomCarrierCarrier : (CategoryTheory.forget₂ GrpCat MonCat).Full

instance AddGrpCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier : (CategoryTheory.forget₂ AddGrpCat AddMonCat).Full

def GrpCat.uliftFunctor : CategoryTheory.Functor GrpCat GrpCat

Universe lift functor for groups.

Equations

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

def AddGrpCat.uliftFunctor : CategoryTheory.Functor AddGrpCat AddGrpCat

Universe lift functor for additive groups.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

structure AddCommGrpCat : Type (u + 1)

The category of additive groups and group morphisms.

• carrier : Type u

  The underlying type.

• str : AddCommGroup ↑self

structure CommGrpCat : 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 AddCommGrpCat, for the sake of mathematicians' sanity.

Equations

• Ab = AddCommGrpCat

@[instance_reducible]

instance CommGrpCat.instCoeSortType : CoeSort CommGrpCat (Type u)

Equations

• CommGrpCat.instCoeSortType = { coe := CommGrpCat.carrier }

@[instance_reducible]

instance AddCommGrpCat.instCoeSortType : CoeSort AddCommGrpCat (Type u)

Equations

• AddCommGrpCat.instCoeSortType = { coe := AddCommGrpCat.carrier }

@[reducible, inline]

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

Construct a bundled CommGrpCat from the underlying type and typeclass.

Equations

• ↧M = { carrier := M, str := inst✝ }

@[reducible, inline]

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

Construct a bundled AddCommGrpCat from the underlying type and typeclass.

Equations

• ↧M = { carrier := M, str := inst✝ }

def AddCommGrpCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prints AddCommGrpCat.of X as ↧X.

Equations

• AddCommGrpCat.delabOf = CategoryTheory.delabOf

def CommGrpCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prints CommGrpCat.of X as ↧X.

Equations

• CommGrpCat.delabOf = CategoryTheory.delabOf

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

The type of morphisms in AddCommGrpCat R.

• _mkInternal :: (
• hom' : ↑A →+ ↑B

  The underlying monoid homomorphism.

• )

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

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

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

The type of morphisms in CommGrpCat R.

• _mkInternal :: (
• hom' : ↑A →* ↑B

  The underlying monoid homomorphism.

• )

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

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[reducible, inline]

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

Turn a morphism in CommGrpCat back into a MonoidHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

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

Turn a morphism in AddCommGrpCat back into an AddMonoidHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

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

Typecheck a MonoidHom as a morphism in CommGrpCat.

Equations

• CommGrpCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

@[reducible, inline]

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

Typecheck an AddMonoidHom as a morphism in AddCommGrpCat.

Equations

• AddCommGrpCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

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

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

Equations

• CommGrpCat.Hom.Simps.hom X Y f = f.hom

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

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

Equations

• AddCommGrpCat.Hom.Simps.hom X Y f = f.hom

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[instance_reducible]

instance CommGrpCat.instInhabited : Inhabited CommGrpCat

Equations

• CommGrpCat.instInhabited = { default := ↧PUnit.{?u.1 + 1} }

@[instance_reducible]

instance AddCommGrpCat.instInhabited : Inhabited AddCommGrpCat

Equations

• AddCommGrpCat.instInhabited = { default := ↧PUnit.{?u.1 + 1} }

theorem CommGrpCat.coe_of (R : Type u) [CommGroup R] : ↑↧R = R

theorem AddCommGrpCat.coe_of (R : Type u) [AddCommGroup R] : ↑↧R = R

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem CommGrpCat.comp_apply {X Y T : CommGrpCat} (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 AddCommGrpCat.comp_apply {X Y T : AddCommGrpCat} (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 CommGrpCat.hom_ext {X Y : CommGrpCat} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CommGrpCat.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 AddCommGrpCat.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 CommGrpCat.ofHom_apply {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

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

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

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

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

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

@[instance_reducible]

instance CommGrpCat.hasForgetToGroup : CategoryTheory.HasForget₂ CommGrpCat GrpCat

Equations

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

@[instance_reducible]

instance AddCommGrpCat.hasForgetToAddGroup : CategoryTheory.HasForget₂ AddCommGrpCat AddGrpCat

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem CommGrpCat.forget₂_map {R S : CommGrpCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ CommGrpCat GrpCat).obj R)) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ CommGrpCat GrpCat).map f)) x = (CategoryTheory.ConcreteCategory.hom f) x

@[simp]

theorem AddCommGrpCat.forget₂_map {R S : AddCommGrpCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).obj R)) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).map f)) x = (CategoryTheory.ConcreteCategory.hom f) x

@[instance_reducible]

instance CommGrpCat.instCoeGrpCat : Coe CommGrpCat GrpCat

Equations

• CommGrpCat.instCoeGrpCat = { coe := (CategoryTheory.forget₂ CommGrpCat GrpCat).obj }

@[instance_reducible]

instance AddCommGrpCat.instCoeAddGrpCat : Coe AddCommGrpCat AddGrpCat

Equations

• AddCommGrpCat.instCoeAddGrpCat = { coe := (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).obj }

def CommGrpCat.fullyFaithfulForget₂ToGrp : (CategoryTheory.forget₂ CommGrpCat GrpCat).FullyFaithful

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

Equations

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

def AddCommGrpCat.fullyFaithfulForget₂ToAddGrp : (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).FullyFaithful

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

Equations

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

@[reducible, inline, deprecated AddCommGrpCat.fullyFaithfulForget₂ToAddGrp (since := "2026-10-13")]

abbrev AddCommGrpCat.fullyFaihtfulForget₂ToAddGrp : (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).FullyFaithful

Deprecated alias for AddCommGrpCat.fullyFaithfulForget₂ToAddGrp.

Equations

• AddCommGrpCat.fullyFaihtfulForget₂ToAddGrp = AddCommGrpCat.fullyFaithfulForget₂ToAddGrp

instance CommGrpCat.instFullGrpCatForget₂MonoidHomCarrierCarrier : (CategoryTheory.forget₂ CommGrpCat GrpCat).Full

instance AddCommGrpCat.instFullAddGrpCatForget₂AddMonoidHomCarrierCarrier : (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).Full

@[instance_reducible]

instance CommGrpCat.hasForgetToCommMonCat : CategoryTheory.HasForget₂ CommGrpCat CommMonCat

Equations

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

@[instance_reducible]

instance AddCommGrpCat.hasForgetToAddCommMonCat : CategoryTheory.HasForget₂ AddCommGrpCat AddCommMonCat

Equations

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

@[simp]

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

@[simp]

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

@[instance_reducible]

instance CommGrpCat.instCoeCommMonCat : Coe CommGrpCat CommMonCat

Equations

• CommGrpCat.instCoeCommMonCat = { coe := (CategoryTheory.forget₂ CommGrpCat CommMonCat).obj }

@[instance_reducible]

instance AddCommGrpCat.instCoeCommMonCat : Coe AddCommGrpCat AddCommMonCat

Equations

• AddCommGrpCat.instCoeCommMonCat = { coe := (CategoryTheory.forget₂ AddCommGrpCat AddCommMonCat).obj }

@[instance_reducible]

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

Equations

• G.instOneHom H = { one := CommGrpCat.ofHom 1 }

@[instance_reducible]

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

Equations

• G.instZeroHom H = { zero := AddCommGrpCat.ofHom 0 }

@[simp]

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

@[simp]

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

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

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

def CommGrpCat.uliftFunctor : CategoryTheory.Functor CommGrpCat CommGrpCat

Universe lift functor for commutative groups.

Equations

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

def AddCommGrpCat.uliftFunctor : CategoryTheory.Functor AddCommGrpCat AddCommGrpCat

Universe lift functor for additive commutative groups.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def AddCommGrpCat.asHom {G : AddCommGrpCat} (g : ↑G) : ↧ℤ ⟶ G

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

Equations

• AddCommGrpCat.asHom g = AddCommGrpCat.ofHom ((zmultiplesHom ↑G) g)

@[simp]

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

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

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

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

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

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

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

Equations

• e.toGrpIso = { hom := GrpCat.ofHom e.toMonoidHom, inv := GrpCat.ofHom e.symm.toMonoidHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

Equations

• e.toAddGrpIso = { hom := AddGrpCat.ofHom e.toAddMonoidHom, inv := AddGrpCat.ofHom e.symm.toAddMonoidHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• e.toCommGrpIso = { hom := CommGrpCat.ofHom e.toMonoidHom, inv := CommGrpCat.ofHom e.symm.toMonoidHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

Equations

• e.toAddCommGrpIso = { hom := AddCommGrpCat.ofHom e.toAddMonoidHom, inv := AddCommGrpCat.ofHom e.symm.toAddMonoidHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Build a MulEquiv from an isomorphism in the category GrpCat.

Equations

• i.groupIsoToMulEquiv = (GrpCat.Hom.hom i.hom).toMulEquiv (GrpCat.Hom.hom i.inv) ⋯ ⋯

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

Build an addEquiv from an isomorphism in the category AddGrpCat

Equations

• i.addGroupIsoToAddEquiv = (AddGrpCat.Hom.hom i.hom).toAddEquiv (AddGrpCat.Hom.hom i.inv) ⋯ ⋯

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

Build a MulEquiv from an isomorphism in the category CommGrpCat.

Equations

• i.commGroupIsoToMulEquiv = (CommGrpCat.Hom.hom i.hom).toMulEquiv (CommGrpCat.Hom.hom i.inv) ⋯ ⋯

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

Build an AddEquiv from an isomorphism in the category AddCommGrpCat.

Equations

• i.addCommGroupIsoToAddEquiv = (AddCommGrpCat.Hom.hom i.hom).toAddEquiv (AddCommGrpCat.Hom.hom i.inv) ⋯ ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• mulEquivIsoGroupIso = { hom := TypeCat.ofHom fun (e : ↑X ≃* ↑Y) => e.toGrpIso, inv := TypeCat.ofHom fun (i : X ≅ Y) => i.groupIsoToMulEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

Equations

• addEquivIsoAddGroupIso = { hom := TypeCat.ofHom fun (e : ↑X ≃+ ↑Y) => e.toAddGrpIso, inv := TypeCat.ofHom fun (i : X ≅ Y) => i.addGroupIsoToAddEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

Equations

• mulEquivIsoCommGroupIso = { hom := TypeCat.ofHom fun (e : ↑X ≃* ↑Y) => e.toCommGrpIso, inv := TypeCat.ofHom fun (i : X ≅ Y) => i.commGroupIsoToMulEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

Equations

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

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

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.

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.

Equations

• CategoryTheory.Aut.mulEquivPerm = CategoryTheory.Aut.isoPerm.groupIsoToMulEquiv

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

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

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

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

@[reducible, inline]

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

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

Equations

• GrpMax = GrpCat

@[reducible, inline]

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

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

Equations

• GrpMaxAux = AddGrpCat

@[reducible, inline]

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

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

Equations

• AddGrpMax = AddGrpCat

@[reducible, inline]

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

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

Equations

• CommGrpMax = CommGrpCat

@[reducible, inline]

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

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

Equations

• AddCommGrpMaxAux = AddCommGrpCat

@[reducible, inline]

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

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

Equations

• AddCommGrpMax = AddCommGrpCat