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

We introduce the bundled categories:

• GroupCat
• AddGroupCat
• CommGroupCat
• AddCommGroupCat along with the relevant forgetful functors between them, and to the bundled monoid categories.

def AddGroupCat : Type (u + 1)

The category of additive groups and group morphisms

Equations

• AddGroupCat = CategoryTheory.Bundled AddGroup

def GroupCat : Type (u + 1)

The category of groups and group morphisms.

Equations

• GroupCat = CategoryTheory.Bundled Group

instance AddGroupCat.instParentProjectionTypeAddMonoidAddGroupToAddMonoidToSubNegAddMonoid : CategoryTheory.BundledHom.ParentProjection fun {α : Type u_1} (h : AddGroup α) => SubNegMonoid.toAddMonoid

Equations

• AddGroupCat.instParentProjectionTypeAddMonoidAddGroupToAddMonoidToSubNegAddMonoid = ⋯

instance GroupCat.instParentProjectionTypeMonoidGroupToMonoidToDivInvMonoid : CategoryTheory.BundledHom.ParentProjection fun {α : Type u_1} (h : Group α) => DivInvMonoid.toMonoid

Equations

• GroupCat.instParentProjectionTypeMonoidGroupToMonoidToDivInvMonoid = ⋯

instance instAddGroupCatLargeCategory : CategoryTheory.LargeCategory AddGroupCat

Equations

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

instance AddGroupCat.concreteCategory : CategoryTheory.ConcreteCategory AddGroupCat

Equations

• AddGroupCat.concreteCategory = id inferInstance

instance GroupCat.concreteCategory : CategoryTheory.ConcreteCategory GroupCat

Equations

• GroupCat.concreteCategory = id inferInstance

instance AddGroupCat.instCoeSortAddGroupCatType : CoeSort AddGroupCat (Type u_1)

Equations

• AddGroupCat.instCoeSortAddGroupCatType = { coe := fun (X : AddGroupCat) => ↑X }

instance GroupCat.instCoeSortGroupCatType : CoeSort GroupCat (Type u_1)

Equations

• GroupCat.instCoeSortGroupCatType = { coe := fun (X : GroupCat) => ↑X }

instance AddGroupCat.instGroupα (X : AddGroupCat) : AddGroup ↑X

Equations

• AddGroupCat.instGroupα X = X.str

instance GroupCat.instGroupα (X : GroupCat) : Group ↑X

Equations

• GroupCat.instGroupα X = X.str

instance AddGroupCat.instCoeFunHomAddGroupCatToQuiverToCategoryStructInstAddGroupCatLargeCategoryForAllαAddGroup {X : AddGroupCat} {Y : AddGroupCat} : CoeFun (X ⟶ Y) fun (x : X ⟶ Y) => ↑X → ↑Y

Equations

• AddGroupCat.instCoeFunHomAddGroupCatToQuiverToCategoryStructInstAddGroupCatLargeCategoryForAllαAddGroup = { coe := fun (f : ↑X →+ ↑Y) => ⇑f }

instance GroupCat.instCoeFunHomGroupCatToQuiverToCategoryStructInstGroupCatLargeCategoryForAllαGroup {X : GroupCat} {Y : GroupCat} : CoeFun (X ⟶ Y) fun (x : X ⟶ Y) => ↑X → ↑Y

Equations

• GroupCat.instCoeFunHomGroupCatToQuiverToCategoryStructInstGroupCatLargeCategoryForAllαGroup = { coe := fun (f : ↑X →* ↑Y) => ⇑f }

instance AddGroupCat.instFunLike (X : AddGroupCat) (Y : AddGroupCat) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• AddGroupCat.instFunLike X Y = let_fun this := inferInstance; this

instance GroupCat.instFunLike (X : GroupCat) (Y : GroupCat) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• GroupCat.instFunLike X Y = let_fun this := inferInstance; this

@[simp]

theorem AddGroupCat.coe_id {X : AddGroupCat} : ⇑(CategoryTheory.CategoryStruct.id X) = id

@[simp]

theorem GroupCat.coe_id {X : GroupCat} : ⇑(CategoryTheory.CategoryStruct.id X) = id

@[simp]

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

@[simp]

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

theorem AddGroupCat.comp_def {X : AddGroupCat} {Y : AddGroupCat} {Z : AddGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : CategoryTheory.CategoryStruct.comp f g = AddMonoidHom.comp g f

theorem GroupCat.comp_def {X : GroupCat} {Y : GroupCat} {Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : CategoryTheory.CategoryStruct.comp f g = MonoidHom.comp g f

@[simp]

theorem GroupCat.forget_map {X : GroupCat} {Y : GroupCat} (f : X ⟶ Y) : (CategoryTheory.forget GroupCat).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

def AddGroupCat.of (X : Type u) [AddGroup X] : AddGroupCat

Construct a bundled AddGroup from the underlying type and typeclass.

Equations

• AddGroupCat.of X = CategoryTheory.Bundled.of X

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

Construct a bundled Group from the underlying type and typeclass.

Equations

• GroupCat.of X = CategoryTheory.Bundled.of X

@[simp]

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

@[simp]

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

instance AddGroupCat.instInhabitedAddGroupCat : Inhabited AddGroupCat

Equations

• AddGroupCat.instInhabitedAddGroupCat = { default := AddGroupCat.of PUnit.{u_1 + 1} }

instance GroupCat.instInhabitedGroupCat : Inhabited GroupCat

Equations

• GroupCat.instInhabitedGroupCat = { default := GroupCat.of PUnit.{u_1 + 1} }

instance AddGroupCat.hasForgetToAddMonCat : CategoryTheory.HasForget₂ AddGroupCat AddMonCat

Equations

• AddGroupCat.hasForgetToAddMonCat = CategoryTheory.BundledHom.forget₂ AddMonCat.AssocAddMonoidHom fun {α : Type u_1} (h : AddGroup α) => SubNegMonoid.toAddMonoid

instance GroupCat.hasForgetToMonCat : CategoryTheory.HasForget₂ GroupCat MonCat

Equations

• GroupCat.hasForgetToMonCat = CategoryTheory.BundledHom.forget₂ MonCat.AssocMonoidHom fun {α : Type u_1} (h : Group α) => DivInvMonoid.toMonoid

instance AddGroupCat.instCoeAddGroupCatMonCat : Coe AddGroupCat AddMonCat

Equations

• AddGroupCat.instCoeAddGroupCatMonCat = { coe := (CategoryTheory.forget₂ AddGroupCat AddMonCat).obj }

instance GroupCat.instCoeGroupCatMonCat : Coe GroupCat MonCat

Equations

• GroupCat.instCoeGroupCatMonCat = { coe := (CategoryTheory.forget₂ GroupCat MonCat).obj }

instance AddGroupCat.instZeroHomAddGroupCatToQuiverToCategoryStructInstAddGroupCatLargeCategory (G : AddGroupCat) (H : AddGroupCat) : Zero (G ⟶ H)

Equations

• AddGroupCat.instZeroHomAddGroupCatToQuiverToCategoryStructInstAddGroupCatLargeCategory G H = inferInstance

instance GroupCat.instOneHomGroupCatToQuiverToCategoryStructInstGroupCatLargeCategory (G : GroupCat) (H : GroupCat) : One (G ⟶ H)

Equations

• GroupCat.instOneHomGroupCatToQuiverToCategoryStructInstGroupCatLargeCategory G H = inferInstance

@[simp]

theorem AddGroupCat.zero_apply (G : AddGroupCat) (H : AddGroupCat) (g : ↑G) : 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} [AddGroup X] [AddGroup Y] (f : X →+ Y) : AddGroupCat.of X ⟶ AddGroupCat.of Y

Typecheck an AddMonoidHom as a morphism in AddGroup.

Equations

• AddGroupCat.ofHom f = f

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

Typecheck a MonoidHom as a morphism in GroupCat.

Equations

• GroupCat.ofHom f = f

theorem AddGroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [AddGroup X] [AddGroup Y] (f : X →+ Y) (x : X) : (AddGroupCat.ofHom f) x = f x

theorem GroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [Group X] [Group Y] (f : X →* Y) (x : X) : (GroupCat.ofHom f) x = f x

instance AddGroupCat.ofUnique (G : Type u_1) [AddGroup G] [i : Unique G] : Unique ↑(AddGroupCat.of G)

Equations

• AddGroupCat.ofUnique G = i

instance GroupCat.ofUnique (G : Type u_1) [Group G] [i : Unique G] : Unique ↑(GroupCat.of G)

Equations

• GroupCat.ofUnique G = i

def AddCommGroupCat : Type (u + 1)

The category of additive commutative groups and group morphisms.

Equations

• AddCommGroupCat = CategoryTheory.Bundled AddCommGroup

def CommGroupCat : Type (u + 1)

The category of commutative groups and group morphisms.

Equations

• CommGroupCat = CategoryTheory.Bundled CommGroup

@[inline, reducible]

abbrev Ab : Type (u_1 + 1)

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

Equations

• Ab = AddCommGroupCat

instance AddCommGroupCat.instParentProjectionTypeAddGroupAddCommGroupToAddGroup : CategoryTheory.BundledHom.ParentProjection @AddCommGroup.toAddGroup

Equations

• AddCommGroupCat.instParentProjectionTypeAddGroupAddCommGroupToAddGroup = ⋯

instance CommGroupCat.instParentProjectionTypeGroupCommGroupToGroup : CategoryTheory.BundledHom.ParentProjection @CommGroup.toGroup

Equations

• CommGroupCat.instParentProjectionTypeGroupCommGroupToGroup = ⋯

instance instAddCommGroupCatLargeCategory : CategoryTheory.LargeCategory AddCommGroupCat

Equations

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

instance AddCommGroupCat.concreteCategory : CategoryTheory.ConcreteCategory AddCommGroupCat

Equations

• AddCommGroupCat.concreteCategory = id inferInstance

instance CommGroupCat.concreteCategory : CategoryTheory.ConcreteCategory CommGroupCat

Equations

• CommGroupCat.concreteCategory = id inferInstance

instance AddCommGroupCat.instCoeSortAddCommGroupCatType : CoeSort AddCommGroupCat (Type u_1)

Equations

• AddCommGroupCat.instCoeSortAddCommGroupCatType = { coe := fun (X : AddCommGroupCat) => ↑X }

instance CommGroupCat.instCoeSortCommGroupCatType : CoeSort CommGroupCat (Type u_1)

Equations

• CommGroupCat.instCoeSortCommGroupCatType = { coe := fun (X : CommGroupCat) => ↑X }

instance AddCommGroupCat.addCommGroupInstance (X : AddCommGroupCat) : AddCommGroup ↑X

Equations

• AddCommGroupCat.addCommGroupInstance X = X.str

instance CommGroupCat.commGroupInstance (X : CommGroupCat) : CommGroup ↑X

Equations

• CommGroupCat.commGroupInstance X = X.str

instance AddCommGroupCat.instCoeFunHomAddCommGroupCatToQuiverToCategoryStructInstAddCommGroupCatLargeCategoryForAllαAddCommGroup {X : AddCommGroupCat} {Y : AddCommGroupCat} : CoeFun (X ⟶ Y) fun (x : X ⟶ Y) => ↑X → ↑Y

Equations

• AddCommGroupCat.instCoeFunHomAddCommGroupCatToQuiverToCategoryStructInstAddCommGroupCatLargeCategoryForAllαAddCommGroup = { coe := fun (f : ↑X →+ ↑Y) => ⇑f }

instance CommGroupCat.instCoeFunHomCommGroupCatToQuiverToCategoryStructInstCommGroupCatLargeCategoryForAllαCommGroup {X : CommGroupCat} {Y : CommGroupCat} : CoeFun (X ⟶ Y) fun (x : X ⟶ Y) => ↑X → ↑Y

Equations

• CommGroupCat.instCoeFunHomCommGroupCatToQuiverToCategoryStructInstCommGroupCatLargeCategoryForAllαCommGroup = { coe := fun (f : ↑X →* ↑Y) => ⇑f }

instance AddCommGroupCat.instFunLike (X : AddCommGroupCat) (Y : AddCommGroupCat) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• AddCommGroupCat.instFunLike X Y = let_fun this := inferInstance; this

instance CommGroupCat.instFunLike (X : CommGroupCat) (Y : CommGroupCat) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• CommGroupCat.instFunLike X Y = let_fun this := inferInstance; this

@[simp]

theorem AddCommGroupCat.coe_id {X : AddCommGroupCat} : ⇑(CategoryTheory.CategoryStruct.id X) = id

@[simp]

theorem CommGroupCat.coe_id {X : CommGroupCat} : ⇑(CategoryTheory.CategoryStruct.id X) = id

@[simp]

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

@[simp]

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

theorem AddCommGroupCat.comp_def {X : AddCommGroupCat} {Y : AddCommGroupCat} {Z : AddCommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : CategoryTheory.CategoryStruct.comp f g = AddMonoidHom.comp g f

theorem CommGroupCat.comp_def {X : CommGroupCat} {Y : CommGroupCat} {Z : CommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : CategoryTheory.CategoryStruct.comp f g = MonoidHom.comp g f

@[simp]

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

@[simp]

theorem CommGroupCat.forget_map {X : CommGroupCat} {Y : CommGroupCat} (f : X ⟶ Y) : (CategoryTheory.forget CommGroupCat).map f = ⇑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

def AddCommGroupCat.of (G : Type u) [AddCommGroup G] : AddCommGroupCat

Construct a bundled AddCommGroup from the underlying type and typeclass.

Equations

• AddCommGroupCat.of G = CategoryTheory.Bundled.of G

def CommGroupCat.of (G : Type u) [CommGroup G] : CommGroupCat

Construct a bundled CommGroup from the underlying type and typeclass.

Equations

• CommGroupCat.of G = CategoryTheory.Bundled.of G

instance AddCommGroupCat.instInhabitedAddCommGroupCat : Inhabited AddCommGroupCat

Equations

• AddCommGroupCat.instInhabitedAddCommGroupCat = { default := AddCommGroupCat.of PUnit.{u_1 + 1} }

instance CommGroupCat.instInhabitedCommGroupCat : Inhabited CommGroupCat

Equations

• CommGroupCat.instInhabitedCommGroupCat = { default := CommGroupCat.of PUnit.{u_1 + 1} }

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

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

instance AddCommGroupCat.ofUnique (G : Type u_1) [AddCommGroup G] [i : Unique G] : Unique ↑(AddCommGroupCat.of G)

Equations

• AddCommGroupCat.ofUnique G = i

instance CommGroupCat.ofUnique (G : Type u_1) [CommGroup G] [i : Unique G] : Unique ↑(CommGroupCat.of G)

Equations

• CommGroupCat.ofUnique G = i

instance AddCommGroupCat.hasForgetToAddGroup : CategoryTheory.HasForget₂ AddCommGroupCat AddGroupCat

Equations

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

instance CommGroupCat.hasForgetToGroup : CategoryTheory.HasForget₂ CommGroupCat GroupCat

Equations

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

instance AddCommGroupCat.instCoeAddCommGroupCatAddGroupCat : Coe AddCommGroupCat AddGroupCat

Equations

• AddCommGroupCat.instCoeAddCommGroupCatAddGroupCat = { coe := (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat).obj }

instance CommGroupCat.instCoeCommGroupCatGroupCat : Coe CommGroupCat GroupCat

Equations

• CommGroupCat.instCoeCommGroupCatGroupCat = { coe := (CategoryTheory.forget₂ CommGroupCat GroupCat).obj }

instance AddCommGroupCat.hasForgetToAddCommMonCat : CategoryTheory.HasForget₂ AddCommGroupCat AddCommMonCat

Equations

• AddCommGroupCat.hasForgetToAddCommMonCat = CategoryTheory.InducedCategory.hasForget₂ fun (G : AddCommGroupCat) => AddCommMonCat.of ↑G

instance CommGroupCat.hasForgetToCommMonCat : CategoryTheory.HasForget₂ CommGroupCat CommMonCat

Equations

• CommGroupCat.hasForgetToCommMonCat = CategoryTheory.InducedCategory.hasForget₂ fun (G : CommGroupCat) => CommMonCat.of ↑G

instance AddCommGroupCat.instCoeAddCommGroupCatCommMonCat : Coe AddCommGroupCat AddCommMonCat

Equations

• AddCommGroupCat.instCoeAddCommGroupCatCommMonCat = { coe := (CategoryTheory.forget₂ AddCommGroupCat AddCommMonCat).obj }

instance CommGroupCat.instCoeCommGroupCatCommMonCat : Coe CommGroupCat CommMonCat

Equations

• CommGroupCat.instCoeCommGroupCatCommMonCat = { coe := (CategoryTheory.forget₂ CommGroupCat CommMonCat).obj }

instance AddCommGroupCat.instZeroHomAddCommGroupCatToQuiverToCategoryStructInstAddCommGroupCatLargeCategory (G : AddCommGroupCat) (H : AddCommGroupCat) : Zero (G ⟶ H)

Equations

• AddCommGroupCat.instZeroHomAddCommGroupCatToQuiverToCategoryStructInstAddCommGroupCatLargeCategory G H = inferInstance

instance CommGroupCat.instOneHomCommGroupCatToQuiverToCategoryStructInstCommGroupCatLargeCategory (G : CommGroupCat) (H : CommGroupCat) : One (G ⟶ H)

Equations

• CommGroupCat.instOneHomCommGroupCatToQuiverToCategoryStructInstCommGroupCatLargeCategory G H = inferInstance

@[simp]

theorem AddCommGroupCat.zero_apply (G : AddCommGroupCat) (H : AddCommGroupCat) (g : ↑G) : 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} [AddCommGroup X] [AddCommGroup Y] (f : X →+ Y) : AddCommGroupCat.of X ⟶ AddCommGroupCat.of Y

Typecheck an AddMonoidHom as a morphism in AddCommGroup.

Equations

• AddCommGroupCat.ofHom f = f

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

Typecheck a MonoidHom as a morphism in CommGroup.

Equations

• CommGroupCat.ofHom f = f

@[simp]

theorem AddCommGroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [AddCommGroup X] [AddCommGroup Y] (f : X →+ Y) (x : X) : (AddCommGroupCat.ofHom f) x = f x

@[simp]

theorem CommGroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [CommGroup X] [CommGroup Y] (f : X →* Y) (x : X) : (CommGroupCat.ofHom f) x = f x

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

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

Equations

• AddCommGroupCat.asHom g = (zmultiplesHom ↑G) g

@[simp]

theorem AddCommGroupCat.asHom_apply {G : AddCommGroupCat} (g : ↑G) (i : ℤ) : (AddCommGroupCat.asHom g) i = i • g

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

theorem AddCommGroupCat.int_hom_ext {G : AddCommGroupCat} (f : AddCommGroupCat.of ℤ ⟶ G) (g : AddCommGroupCat.of ℤ ⟶ G) (w : f 1 = g 1) : f = g

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

theorem AddEquiv.toAddGroupCatIso.proof_1 {X : AddGroupCat} {Y : AddGroupCat} (e : ↑X ≃+ ↑Y) : CategoryTheory.CategoryStruct.comp (AddEquiv.toAddMonoidHom e) (AddEquiv.toAddMonoidHom (AddEquiv.symm e)) = CategoryTheory.CategoryStruct.id X

def AddEquiv.toAddGroupCatIso {X : AddGroupCat} {Y : AddGroupCat} (e : ↑X ≃+ ↑Y) : X ≅ Y

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

Equations

• AddEquiv.toAddGroupCatIso e = { hom := AddEquiv.toAddMonoidHom e, inv := AddEquiv.toAddMonoidHom (AddEquiv.symm e), hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem AddEquiv.toAddGroupCatIso.proof_2 {X : AddGroupCat} {Y : AddGroupCat} (e : ↑X ≃+ ↑Y) : CategoryTheory.CategoryStruct.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm e)) (AddEquiv.toAddMonoidHom e) = CategoryTheory.CategoryStruct.id Y

@[simp]

theorem AddEquiv.toAddGroupCatIso_inv {X : AddGroupCat} {Y : AddGroupCat} (e : ↑X ≃+ ↑Y) : (AddEquiv.toAddGroupCatIso e).inv = AddEquiv.toAddMonoidHom (AddEquiv.symm e)

@[simp]

theorem AddEquiv.toAddGroupCatIso_hom {X : AddGroupCat} {Y : AddGroupCat} (e : ↑X ≃+ ↑Y) : (AddEquiv.toAddGroupCatIso e).hom = AddEquiv.toAddMonoidHom e

@[simp]

theorem MulEquiv.toGroupCatIso_hom {X : GroupCat} {Y : GroupCat} (e : ↑X ≃* ↑Y) : (MulEquiv.toGroupCatIso e).hom = MulEquiv.toMonoidHom e

@[simp]

theorem MulEquiv.toGroupCatIso_inv {X : GroupCat} {Y : GroupCat} (e : ↑X ≃* ↑Y) : (MulEquiv.toGroupCatIso e).inv = MulEquiv.toMonoidHom (MulEquiv.symm e)

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

• MulEquiv.toGroupCatIso e = { hom := MulEquiv.toMonoidHom e, inv := MulEquiv.toMonoidHom (MulEquiv.symm e), hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem AddEquiv.toAddCommGroupCatIso.proof_1 {X : AddCommGroupCat} {Y : AddCommGroupCat} (e : ↑X ≃+ ↑Y) : CategoryTheory.CategoryStruct.comp (AddEquiv.toAddMonoidHom e) (AddEquiv.toAddMonoidHom (AddEquiv.symm e)) = CategoryTheory.CategoryStruct.id X

theorem AddEquiv.toAddCommGroupCatIso.proof_2 {X : AddCommGroupCat} {Y : AddCommGroupCat} (e : ↑X ≃+ ↑Y) : CategoryTheory.CategoryStruct.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm e)) (AddEquiv.toAddMonoidHom e) = CategoryTheory.CategoryStruct.id Y

def AddEquiv.toAddCommGroupCatIso {X : AddCommGroupCat} {Y : AddCommGroupCat} (e : ↑X ≃+ ↑Y) : X ≅ Y

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

Equations

• AddEquiv.toAddCommGroupCatIso e = { hom := AddEquiv.toAddMonoidHom e, inv := AddEquiv.toAddMonoidHom (AddEquiv.symm e), hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem MulEquiv.toCommGroupCatIso_inv {X : CommGroupCat} {Y : CommGroupCat} (e : ↑X ≃* ↑Y) : (MulEquiv.toCommGroupCatIso e).inv = MulEquiv.toMonoidHom (MulEquiv.symm e)

@[simp]

theorem AddEquiv.toAddCommGroupCatIso_hom {X : AddCommGroupCat} {Y : AddCommGroupCat} (e : ↑X ≃+ ↑Y) : (AddEquiv.toAddCommGroupCatIso e).hom = AddEquiv.toAddMonoidHom e

@[simp]

theorem MulEquiv.toCommGroupCatIso_hom {X : CommGroupCat} {Y : CommGroupCat} (e : ↑X ≃* ↑Y) : (MulEquiv.toCommGroupCatIso e).hom = MulEquiv.toMonoidHom e

@[simp]

theorem AddEquiv.toAddCommGroupCatIso_inv {X : AddCommGroupCat} {Y : AddCommGroupCat} (e : ↑X ≃+ ↑Y) : (AddEquiv.toAddCommGroupCatIso e).inv = AddEquiv.toAddMonoidHom (AddEquiv.symm e)

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

• MulEquiv.toCommGroupCatIso e = { hom := MulEquiv.toMonoidHom e, inv := MulEquiv.toMonoidHom (MulEquiv.symm e), hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

Build an addEquiv from an isomorphism in the category AddGroup

Equations

• CategoryTheory.Iso.addGroupIsoToAddEquiv i = AddMonoidHom.toAddEquiv i.hom i.inv ⋯ ⋯

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

Build a MulEquiv from an isomorphism in the category GroupCat.

Equations

• CategoryTheory.Iso.groupIsoToMulEquiv i = MonoidHom.toMulEquiv i.hom i.inv ⋯ ⋯

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

Build an AddEquiv from an isomorphism in the category AddCommGroup.

Equations

• CategoryTheory.Iso.addCommGroupIsoToAddEquiv i = AddMonoidHom.toAddEquiv i.hom i.inv ⋯ ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Build a MulEquiv from an isomorphism in the category CommGroup.

Equations

• CategoryTheory.Iso.commGroupIsoToMulEquiv i = MonoidHom.toMulEquiv i.hom i.inv ⋯ ⋯

theorem addEquivIsoAddGroupIso.proof_1 {X : AddGroupCat} {Y : AddGroupCat} : (CategoryTheory.CategoryStruct.comp (fun (e : ↑X ≃+ ↑Y) => AddEquiv.toAddGroupCatIso e) fun (i : X ≅ Y) => CategoryTheory.Iso.addGroupIsoToAddEquiv i) = CategoryTheory.CategoryStruct.id (↑X ≃+ ↑Y)

theorem addEquivIsoAddGroupIso.proof_2 {X : AddGroupCat} {Y : AddGroupCat} : (CategoryTheory.CategoryStruct.comp (fun (i : X ≅ Y) => CategoryTheory.Iso.addGroupIsoToAddEquiv i) fun (e : ↑X ≃+ ↑Y) => AddEquiv.toAddGroupCatIso e) = CategoryTheory.CategoryStruct.id (X ≅ Y)

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

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

Equations

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

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) => MulEquiv.toGroupCatIso e, inv := fun (i : X ≅ Y) => CategoryTheory.Iso.groupIsoToMulEquiv i, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem addEquivIsoAddCommGroupIso.proof_2 {X : AddCommGroupCat} {Y : AddCommGroupCat} : (CategoryTheory.CategoryStruct.comp (fun (i : X ≅ Y) => CategoryTheory.Iso.addCommGroupIsoToAddEquiv i) fun (e : ↑X ≃+ ↑Y) => AddEquiv.toAddCommGroupCatIso e) = CategoryTheory.CategoryStruct.comp (fun (i : X ≅ Y) => CategoryTheory.Iso.addCommGroupIsoToAddEquiv i) fun (e : ↑X ≃+ ↑Y) => AddEquiv.toAddCommGroupCatIso e

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

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

Equations

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

theorem addEquivIsoAddCommGroupIso.proof_1 {X : AddCommGroupCat} {Y : AddCommGroupCat} : (CategoryTheory.CategoryStruct.comp (fun (e : ↑X ≃+ ↑Y) => AddEquiv.toAddCommGroupCatIso e) fun (i : X ≅ Y) => CategoryTheory.Iso.addCommGroupIsoToAddEquiv i) = CategoryTheory.CategoryStruct.comp (fun (e : ↑X ≃+ ↑Y) => AddEquiv.toAddCommGroupCatIso e) fun (i : X ≅ Y) => CategoryTheory.Iso.addCommGroupIsoToAddEquiv i

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

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

Equations

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

def CategoryTheory.Aut.isoPerm {α : Type u} : GroupCat.of (CategoryTheory.Aut α) ≅ GroupCat.of (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} : CategoryTheory.Aut α ≃* Equiv.Perm α

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

Equations

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

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

Equations

• AddGroupCat.forget_reflects_isos = ⋯

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

Equations

• GroupCat.forget_reflects_isos = ⋯

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

Equations

• AddCommGroupCat.forget_reflects_isos = ⋯

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

Equations

• CommGroupCat.forget_reflects_isos = ⋯

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

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

Equations

• GroupCatMaxAux = AddGroupCat

@[inline, reducible]

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

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

Equations

• GroupCatMax = GroupCat

@[inline, reducible]

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

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

Equations

• AddGroupCatMax = AddGroupCat

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

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

Equations

• AddCommGroupCatMaxAux = AddCommGroupCat

@[inline, reducible]

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

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

Equations

• CommGroupCatMax = CommGroupCat

@[inline, reducible]

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

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

Equations

• AddCommGroupCatMax = AddCommGroupCat