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.

source

def AddGroupCat :

Type (u + 1)

The category of additive groups and group morphisms

Instances For

source

def GroupCat :

Type (u + 1)

The category of groups and group morphisms.

Instances For

source

instance AddGroupCat.instParentProjectionTypeAddMonoidAddGroupToAddMonoidToSubNegAddMonoid :

CategoryTheory.BundledHom.ParentProjection fun {α} h => SubNegMonoid.toAddMonoid

source

theorem AddGroupCat.instParentProjectionTypeAddMonoidAddGroupToAddMonoidToSubNegAddMonoid.proof_1 :

CategoryTheory.BundledHom.ParentProjection fun {α} h => SubNegMonoid.toAddMonoid

source

instance GroupCat.instParentProjectionTypeMonoidGroupToMonoidToDivInvMonoid :

CategoryTheory.BundledHom.ParentProjection fun {α} h => DivInvMonoid.toMonoid

source

instance instAddGroupCatLargeCategory :

CategoryTheory.LargeCategory AddGroupCat

source

instance AddGroupCat.concreteCategory :

CategoryTheory.ConcreteCategory AddGroupCat

source

instance GroupCat.concreteCategory :

CategoryTheory.ConcreteCategory GroupCat

source

instance AddGroupCat.instCoeSortAddGroupCatType :

CoeSort AddGroupCat (Type u_1)

source

instance GroupCat.instCoeSortGroupCatType :

CoeSort GroupCat (Type u_1)

source

instance AddGroupCat.instGroupα (X : AddGroupCat) :

AddGroup ↑X

source

instance GroupCat.instGroupα (X : GroupCat) :

Group ↑X

source

instance AddGroupCat.instCoeFunHomAddGroupCatToQuiverToCategoryStructInstAddGroupCatLargeCategoryForAllαAddGroup {X : AddGroupCat} {Y : AddGroupCat} :

CoeFun (X ⟶ Y) fun x => ↑X → ↑Y

source

instance GroupCat.instCoeFunHomGroupCatToQuiverToCategoryStructInstGroupCatLargeCategoryForAllαGroup {X : GroupCat} {Y : GroupCat} :

CoeFun (X ⟶ Y) fun x => ↑X → ↑Y

source

instance AddGroupCat.FunLike_instance (X : AddGroupCat) (Y : AddGroupCat) :

FunLike (X ⟶ Y) ↑X fun x => ↑Y

source

instance GroupCat.FunLike_instance (X : GroupCat) (Y : GroupCat) :

FunLike (X ⟶ Y) ↑X fun x => ↑Y

source

@[simp]

theorem AddGroupCat.coe_id {X : AddGroupCat} :

↑(CategoryTheory.CategoryStruct.id X) = id

source

@[simp]

theorem GroupCat.coe_id {X : GroupCat} :

↑(CategoryTheory.CategoryStruct.id X) = id

source

@[simp]

theorem AddGroupCat.coe_comp {X : AddGroupCat} {Y : AddGroupCat} {Z : AddGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} :

↑(CategoryTheory.CategoryStruct.comp f g) = ↑g ∘ ↑f

source

@[simp]

theorem GroupCat.coe_comp {X : GroupCat} {Y : GroupCat} {Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} :

↑(CategoryTheory.CategoryStruct.comp f g) = ↑g ∘ ↑f

source

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

source

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

source

@[simp]

theorem GroupCat.forget_map {X : GroupCat} {Y : GroupCat} (f : X ⟶ Y) :

(CategoryTheory.forget GroupCat).map f = ↑f

source

theorem AddGroupCat.ext {X : AddGroupCat} {Y : AddGroupCat} {f : X ⟶ Y} {g : X ⟶ Y} (w : ∀ (x : ↑X), ↑f x = ↑g x) :

f = g

source

theorem GroupCat.ext {X : GroupCat} {Y : GroupCat} {f : X ⟶ Y} {g : X ⟶ Y} (w : ∀ (x : ↑X), ↑f x = ↑g x) :

f = g

source

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

AddGroupCat

Construct a bundled AddGroup from the underlying type and typeclass.

Instances For

source

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

GroupCat

Construct a bundled Group from the underlying type and typeclass.

Instances For

source

@[simp]

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

↑(AddGroupCat.of R) = R

source

@[simp]

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

↑(GroupCat.of R) = R

source

instance AddGroupCat.instInhabitedAddGroupCat :

Inhabited AddGroupCat

source

instance GroupCat.instInhabitedGroupCat :

Inhabited GroupCat

source

instance AddGroupCat.hasForgetToAddMonCat :

CategoryTheory.HasForget₂ AddGroupCat AddMonCat

source

instance GroupCat.hasForgetToMonCat :

CategoryTheory.HasForget₂ GroupCat MonCat

source

instance AddGroupCat.instCoeAddGroupCatMonCat :

Coe AddGroupCat AddMonCat

source

instance GroupCat.instCoeGroupCatMonCat :

Coe GroupCat MonCat

source

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

Zero (G ⟶ H)

source

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

One (G ⟶ H)

source

@[simp]

theorem AddGroupCat.zero_apply (G : AddGroupCat) (H : AddGroupCat) (g : ↑G) :

↑0 g = 0

source

@[simp]

theorem GroupCat.one_apply (G : GroupCat) (H : GroupCat) (g : ↑G) :

↑1 g = 1

source

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.

Instances For

source

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.

Instances For

source

@[simp]

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

source

@[simp]

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

source

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

Unique ↑(AddGroupCat.of G)

source

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

Unique ↑(GroupCat.of G)

source

def AddCommGroupCat :

Type (u + 1)

The category of additive commutative groups and group morphisms.

Instances For

source

def CommGroupCat :

Type (u + 1)

The category of commutative groups and group morphisms.

Instances For

source

@[inline, reducible]

abbrev Ab :

Type (u_1 + 1)

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

Instances For

source

instance AddCommGroupCat.instParentProjectionTypeAddGroupAddCommGroupToAddGroup :

CategoryTheory.BundledHom.ParentProjection @AddCommGroup.toAddGroup

source

theorem AddCommGroupCat.instParentProjectionTypeAddGroupAddCommGroupToAddGroup.proof_1 :

CategoryTheory.BundledHom.ParentProjection @AddCommGroup.toAddGroup

source

instance CommGroupCat.instParentProjectionTypeGroupCommGroupToGroup :

CategoryTheory.BundledHom.ParentProjection @CommGroup.toGroup

source

instance instAddCommGroupCatLargeCategory :

CategoryTheory.LargeCategory AddCommGroupCat

source

instance AddCommGroupCat.concreteCategory :

CategoryTheory.ConcreteCategory AddCommGroupCat

source

instance CommGroupCat.concreteCategory :

CategoryTheory.ConcreteCategory CommGroupCat

source

instance AddCommGroupCat.instCoeSortAddCommGroupCatType :

CoeSort AddCommGroupCat (Type u_1)

source

instance CommGroupCat.instCoeSortCommGroupCatType :

CoeSort CommGroupCat (Type u_1)

source

instance AddCommGroupCat.addCommGroupInstance (X : AddCommGroupCat) :

AddCommGroup ↑X

source

instance CommGroupCat.commGroupInstance (X : CommGroupCat) :

CommGroup ↑X

source

instance AddCommGroupCat.instCoeFunHomAddCommGroupCatToQuiverToCategoryStructInstAddCommGroupCatLargeCategoryForAllαAddCommGroup {X : AddCommGroupCat} {Y : AddCommGroupCat} :

CoeFun (X ⟶ Y) fun x => ↑X → ↑Y

source

instance CommGroupCat.instCoeFunHomCommGroupCatToQuiverToCategoryStructInstCommGroupCatLargeCategoryForAllαCommGroup {X : CommGroupCat} {Y : CommGroupCat} :

CoeFun (X ⟶ Y) fun x => ↑X → ↑Y

source

instance AddCommGroupCat.FunLike_instance (X : AddCommGroupCat) (Y : AddCommGroupCat) :

FunLike (X ⟶ Y) ↑X fun x => ↑Y

source

instance CommGroupCat.FunLike_instance (X : CommGroupCat) (Y : CommGroupCat) :

FunLike (X ⟶ Y) ↑X fun x => ↑Y

source

@[simp]

theorem AddCommGroupCat.coe_id {X : AddCommGroupCat} :

↑(CategoryTheory.CategoryStruct.id X) = id

source

@[simp]

theorem CommGroupCat.coe_id {X : CommGroupCat} :

↑(CategoryTheory.CategoryStruct.id X) = id

source

@[simp]

theorem AddCommGroupCat.coe_comp {X : AddCommGroupCat} {Y : AddCommGroupCat} {Z : AddCommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} :

↑(CategoryTheory.CategoryStruct.comp f g) = ↑g ∘ ↑f

source

@[simp]

theorem CommGroupCat.coe_comp {X : CommGroupCat} {Y : CommGroupCat} {Z : CommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} :

↑(CategoryTheory.CategoryStruct.comp f g) = ↑g ∘ ↑f

source

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

source

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

source

@[simp]

theorem AddCommGroupCat.forget_map {X : AddCommGroupCat} {Y : AddCommGroupCat} (f : X ⟶ Y) :

(CategoryTheory.forget AddCommGroupCat).map f = ↑f

source

@[simp]

theorem CommGroupCat.forget_map {X : CommGroupCat} {Y : CommGroupCat} (f : X ⟶ Y) :

(CategoryTheory.forget CommGroupCat).map f = ↑f

source

theorem AddCommGroupCat.ext {X : AddCommGroupCat} {Y : AddCommGroupCat} {f : X ⟶ Y} {g : X ⟶ Y} (w : ∀ (x : ↑X), ↑f x = ↑g x) :

f = g

source

theorem CommGroupCat.ext {X : CommGroupCat} {Y : CommGroupCat} {f : X ⟶ Y} {g : X ⟶ Y} (w : ∀ (x : ↑X), ↑f x = ↑g x) :

f = g

source

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

AddCommGroupCat

Construct a bundled AddCommGroup from the underlying type and typeclass.

Instances For

source

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

CommGroupCat

Construct a bundled CommGroup from the underlying type and typeclass.

Instances For

source

instance AddCommGroupCat.instInhabitedAddCommGroupCat :

Inhabited AddCommGroupCat

source

instance CommGroupCat.instInhabitedCommGroupCat :

Inhabited CommGroupCat

source

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

↑(AddCommGroupCat.of R) = R

source

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

↑(CommGroupCat.of R) = R

source

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

Unique ↑(AddCommGroupCat.of G)

source

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

Unique ↑(CommGroupCat.of G)

source

instance AddCommGroupCat.hasForgetToAddGroup :

CategoryTheory.HasForget₂ AddCommGroupCat AddGroupCat

source

instance CommGroupCat.hasForgetToGroup :

CategoryTheory.HasForget₂ CommGroupCat GroupCat

source

instance AddCommGroupCat.instCoeAddCommGroupCatAddGroupCat :

Coe AddCommGroupCat AddGroupCat

source

instance CommGroupCat.instCoeCommGroupCatGroupCat :

Coe CommGroupCat GroupCat

source

instance AddCommGroupCat.hasForgetToAddCommMonCat :

CategoryTheory.HasForget₂ AddCommGroupCat AddCommMonCat

source

instance CommGroupCat.hasForgetToCommMonCat :

CategoryTheory.HasForget₂ CommGroupCat CommMonCat

source

instance AddCommGroupCat.instCoeAddCommGroupCatCommMonCat :

Coe AddCommGroupCat AddCommMonCat

source

instance CommGroupCat.instCoeCommGroupCatCommMonCat :

Coe CommGroupCat CommMonCat

source

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

Zero (G ⟶ H)

source

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

One (G ⟶ H)

source

@[simp]

theorem AddCommGroupCat.zero_apply (G : AddCommGroupCat) (H : AddCommGroupCat) (g : ↑G) :

↑0 g = 0

source

@[simp]

theorem CommGroupCat.one_apply (G : CommGroupCat) (H : CommGroupCat) (g : ↑G) :

↑1 g = 1

source

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.

Instances For

source

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.

Instances For

source

@[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

source

@[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

source

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.

Instances For

source

@[simp]

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

↑(AddCommGroupCat.asHom g) i = i • g

source

theorem AddCommGroupCat.asHom_injective {G : AddCommGroupCat} :

Function.Injective AddCommGroupCat.asHom

source

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

f = g

source

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

Function.Injective ↑f

source

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

source

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

source

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

X ≅ Y

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

Instances For

source

@[simp]

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

(AddEquiv.toAddGroupCatIso e).hom = AddEquiv.toAddMonoidHom e

source

@[simp]

theorem MulEquiv.toGroupCatIso_inv {X : GroupCat} {Y : GroupCat} (e : ↑X ≃* ↑Y) :

(MulEquiv.toGroupCatIso e).inv = MulEquiv.toMonoidHom (MulEquiv.symm e)

source

@[simp]

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

(MulEquiv.toGroupCatIso e).hom = MulEquiv.toMonoidHom e

source

@[simp]

theorem AddEquiv.toAddGroupCatIso_inv {X : AddGroupCat} {Y : AddGroupCat} (e : ↑X ≃+ ↑Y) :

(AddEquiv.toAddGroupCatIso e).inv = AddEquiv.toAddMonoidHom (AddEquiv.symm e)

source

def MulEquiv.toGroupCatIso {X : GroupCat} {Y : GroupCat} (e : ↑X ≃* ↑Y) :

X ≅ Y

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

Instances For

source

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

source

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

X ≅ Y

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

Instances For

source

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

source

@[simp]

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

(MulEquiv.toCommGroupCatIso e).hom = MulEquiv.toMonoidHom e

source

@[simp]

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

(AddEquiv.toAddCommGroupCatIso e).hom = AddEquiv.toAddMonoidHom e

source

@[simp]

theorem MulEquiv.toCommGroupCatIso_inv {X : CommGroupCat} {Y : CommGroupCat} (e : ↑X ≃* ↑Y) :

(MulEquiv.toCommGroupCatIso e).inv = MulEquiv.toMonoidHom (MulEquiv.symm e)

source

@[simp]

theorem AddEquiv.toAddCommGroupCatIso_inv {X : AddCommGroupCat} {Y : AddCommGroupCat} (e : ↑X ≃+ ↑Y) :

(AddEquiv.toAddCommGroupCatIso e).inv = AddEquiv.toAddMonoidHom (AddEquiv.symm e)

source

def MulEquiv.toCommGroupCatIso {X : CommGroupCat} {Y : CommGroupCat} (e : ↑X ≃* ↑Y) :

X ≅ Y

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

Instances For

source

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

↑X ≃+ ↑Y

Build an addEquiv from an isomorphism in the category AddGroup

Instances For

source

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

↑X ≃* ↑Y

Build a MulEquiv from an isomorphism in the category GroupCat.

Instances For

source

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

↑X ≃+ ↑Y

Build an AddEquiv from an isomorphism in the category AddCommGroup.

Instances For

source

@[simp]

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

↑(CategoryTheory.Iso.addCommGroupIsoToAddEquiv i) a = ↑i.hom a

source

@[simp]

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

↑(CategoryTheory.Iso.commGroupIsoToMulEquiv i) a = ↑i.hom a

source

@[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

source

@[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

source

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

↑X ≃* ↑Y

Build a MulEquiv from an isomorphism in the category CommGroup.

Instances For

source

def addEquivIsoAddGroupIso {X : AddGroupCat} {Y : AddGroupCat} :

↑X ≃+ ↑Y ≅ X ≅ Y

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

Instances For

source

theorem addEquivIsoAddGroupIso.proof_2 {X : AddGroupCat} {Y : AddGroupCat} :

(CategoryTheory.CategoryStruct.comp (fun i => CategoryTheory.Iso.addGroupIsoToAddEquiv i) fun e => AddEquiv.toAddGroupCatIso e) = CategoryTheory.CategoryStruct.id (X ≅ Y)

source

theorem addEquivIsoAddGroupIso.proof_1 {X : AddGroupCat} {Y : AddGroupCat} :

(CategoryTheory.CategoryStruct.comp (fun e => AddEquiv.toAddGroupCatIso e) fun i => CategoryTheory.Iso.addGroupIsoToAddEquiv i) = CategoryTheory.CategoryStruct.id (↑X ≃+ ↑Y)

source

def mulEquivIsoGroupIso {X : GroupCat} {Y : GroupCat} :

↑X ≃* ↑Y ≅ X ≅ Y

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

Instances For

source

theorem addEquivIsoAddCommGroupIso.proof_1 {X : AddCommGroupCat} {Y : AddCommGroupCat} :

(CategoryTheory.CategoryStruct.comp (fun e => AddEquiv.toAddCommGroupCatIso e) fun i => CategoryTheory.Iso.addCommGroupIsoToAddEquiv i) = CategoryTheory.CategoryStruct.comp (fun e => AddEquiv.toAddCommGroupCatIso e) fun i => CategoryTheory.Iso.addCommGroupIsoToAddEquiv i

source

def addEquivIsoAddCommGroupIso {X : AddCommGroupCat} {Y : AddCommGroupCat} :

↑X ≃+ ↑Y ≅ X ≅ Y

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

Instances For

source

theorem addEquivIsoAddCommGroupIso.proof_2 {X : AddCommGroupCat} {Y : AddCommGroupCat} :

(CategoryTheory.CategoryStruct.comp (fun i => CategoryTheory.Iso.addCommGroupIsoToAddEquiv i) fun e => AddEquiv.toAddCommGroupCatIso e) = CategoryTheory.CategoryStruct.comp (fun i => CategoryTheory.Iso.addCommGroupIsoToAddEquiv i) fun e => AddEquiv.toAddCommGroupCatIso e

source

def mulEquivIsoCommGroupIso {X : CommGroupCat} {Y : CommGroupCat} :

↑X ≃* ↑Y ≅ X ≅ Y

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

Instances For

source

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.

Instances For

source

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.

Instances For

source

instance AddGroupCat.forget_reflects_isos :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget AddGroupCat)

source

theorem AddGroupCat.forget_reflects_isos.proof_1 :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget AddGroupCat)

source

instance GroupCat.forget_reflects_isos :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget GroupCat)

source

instance AddCommGroupCat.forget_reflects_isos :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget AddCommGroupCat)

source

theorem AddCommGroupCat.forget_reflects_isos.proof_1 :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget AddCommGroupCat)

source

instance CommGroupCat.forget_reflects_isos :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget CommGroupCat)

source

abbrev GroupCatMaxAux :

Type ((max u1 u2) + 1)

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

Instances For

source

@[inline, reducible]

abbrev GroupCatMax :

Type ((max u1 u2) + 1)

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

Instances For

source

@[inline, reducible]

abbrev AddGroupCatMax :

Type ((max u1 u2) + 1)

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

Instances For

source

abbrev AddCommGroupCatMaxAux :

Type ((max u1 u2) + 1)

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

Instances For

source

@[inline, reducible]

abbrev CommGroupCatMax :

Type ((max u1 u2) + 1)

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

Instances For

source

@[inline, reducible]

abbrev AddCommGroupCatMax :

Type ((max u1 u2) + 1)

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

Instances For