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.

def AddGrp : Type (u + 1)

The category of additive groups and group morphisms

Equations

• AddGrp = CategoryTheory.Bundled AddGroup

def Grp : Type (u + 1)

The category of groups and group morphisms.

Equations

• Grp = CategoryTheory.Bundled Group

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

Equations

• AddGrp.instParentProjectionAddMonoidAddGroup = ⋯

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

Equations

• Grp.instParentProjectionMonoidGroup = ⋯

instance instAddGrpLargeCategory : CategoryTheory.LargeCategory AddGrp

Equations

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

instance AddGrp.concreteCategory : CategoryTheory.ConcreteCategory AddGrp

Equations

• AddGrp.concreteCategory = id inferInstance

instance Grp.concreteCategory : CategoryTheory.ConcreteCategory Grp

Equations

• Grp.concreteCategory = id inferInstance

instance AddGrp.instCoeSortType : CoeSort AddGrp (Type u_1)

Equations

• AddGrp.instCoeSortType = { coe := fun (X : AddGrp) => ↑X }

instance Grp.instCoeSortType : CoeSort Grp (Type u_1)

Equations

• Grp.instCoeSortType = { coe := fun (X : Grp) => ↑X }

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

Equations

• X.instGroupα = X.str

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

Equations

• X.instGroupα = X.str

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

Construct a bundled AddGroup from the underlying type and typeclass.

Equations

• AddGrp.of X = CategoryTheory.Bundled.of X

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

Construct a bundled Group from the underlying type and typeclass.

Equations

• Grp.of X = CategoryTheory.Bundled.of X

@[simp]

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

@[simp]

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

@[simp]

theorem AddGrp.coe_comp' {G : Type u_1} {H : Type u_1} {K : Type u_1} [AddGroup G] [AddGroup H] [AddGroup K] (f : G →+ H) (g : H →+ K) : ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f

@[simp]

theorem Grp.coe_comp' {G : Type u_1} {H : Type u_1} {K : Type u_1} [Group G] [Group H] [Group K] (f : G →* H) (g : H →* K) : ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f

@[simp]

theorem AddGrp.coe_id' {G : Type u_1} [AddGroup G] : ⇑(CategoryTheory.CategoryStruct.id (AddGrp.of G)) = id

@[simp]

theorem Grp.coe_id' {G : Type u_1} [Group G] : ⇑(CategoryTheory.CategoryStruct.id (Grp.of G)) = id

instance AddGrp.instInhabited : Inhabited AddGrp

Equations

• AddGrp.instInhabited = { default := AddGrp.of PUnit.{?u.1 + 1} }

instance Grp.instInhabited : Inhabited Grp

Equations

• Grp.instInhabited = { default := Grp.of PUnit.{?u.1 + 1} }

instance AddGrp.hasForgetToAddMonCat : CategoryTheory.HasForget₂ AddGrp AddMonCat

Equations

• AddGrp.hasForgetToAddMonCat = CategoryTheory.BundledHom.forget₂ AddMonCat.AssocAddMonoidHom fun {α : Type ?u.7} (h : AddGroup α) => SubNegMonoid.toAddMonoid

instance Grp.hasForgetToMonCat : CategoryTheory.HasForget₂ Grp MonCat

Equations

• Grp.hasForgetToMonCat = CategoryTheory.BundledHom.forget₂ MonCat.AssocMonoidHom fun {α : Type ?u.7} (h : Group α) => DivInvMonoid.toMonoid

instance AddGrp.instCoeMonCat : Coe AddGrp AddMonCat

Equations

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

instance Grp.instCoeMonCat : Coe Grp MonCat

Equations

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

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

Equations

• G.instZeroHom H = inferInstance

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

Equations

• G.instOneHom H = inferInstance

@[simp]

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

@[simp]

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

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

Typecheck an AddMonoidHom as a morphism in AddGroup.

Equations

• AddGrp.ofHom f = f

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

Typecheck a MonoidHom as a morphism in Grp.

Equations

• Grp.ofHom f = f

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

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

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

Equations

• AddGrp.ofUnique G = i

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

Equations

• Grp.ofUnique G = i

def AddGrp.uliftFunctor : CategoryTheory.Functor AddGrp AddGrp

Universe lift functor for additive groups.

Equations

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

theorem AddGrp.uliftFunctor.proof_2 {X : AddGrp} {Y : AddGrp} {Z : AddGrp} (f : X ⟶ Y) (g : Y ⟶ Z) : { obj := fun (X : AddGrp) => AddGrp.of (ULift.{u_2, u_1} ↑X), map := fun {X Y : AddGrp} (f : X ⟶ Y) => AddGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g) = { obj := fun (X : AddGrp) => AddGrp.of (ULift.{u_2, u_1} ↑X), map := fun {X Y : AddGrp} (f : X ⟶ Y) => AddGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g)

theorem AddGrp.uliftFunctor.proof_1 (X : AddGrp) : { obj := fun (X : AddGrp) => AddGrp.of (ULift.{u_2, u_1} ↑X), map := fun {X Y : AddGrp} (f : X ⟶ Y) => AddGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X) = { obj := fun (X : AddGrp) => AddGrp.of (ULift.{u_2, u_1} ↑X), map := fun {X Y : AddGrp} (f : X ⟶ Y) => AddGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X)

@[simp]

theorem AddGrp.uliftFunctor_map {X : AddGrp} {Y : AddGrp} (f : X ⟶ Y) : AddGrp.uliftFunctor.map f = AddGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom))

@[simp]

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

@[simp]

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

@[simp]

theorem Grp.uliftFunctor_map {X : Grp} {Y : Grp} (f : X ⟶ Y) : Grp.uliftFunctor.map f = Grp.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp (MonoidHom.comp f MulEquiv.ulift.toMonoidHom))

def Grp.uliftFunctor : CategoryTheory.Functor Grp Grp

Universe lift functor for groups.

Equations

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

def AddCommGrp : Type (u + 1)

The category of additive commutative groups and group morphisms.

Equations

• AddCommGrp = CategoryTheory.Bundled AddCommGroup

def CommGrp : Type (u + 1)

The category of commutative groups and group morphisms.

Equations

• CommGrp = CategoryTheory.Bundled CommGroup

@[reducible, inline]

abbrev Ab : Type (u_1 + 1)

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

Equations

• Ab = AddCommGrp

instance AddCommGrp.instParentProjectionAddGroupAddCommGroupToAddGroup : CategoryTheory.BundledHom.ParentProjection @AddCommGroup.toAddGroup

Equations

• AddCommGrp.instParentProjectionAddGroupAddCommGroupToAddGroup = ⋯

instance CommGrp.instParentProjectionGroupCommGroupToGroup : CategoryTheory.BundledHom.ParentProjection @CommGroup.toGroup

Equations

• CommGrp.instParentProjectionGroupCommGroupToGroup = ⋯

instance instAddCommGrpLargeCategory : CategoryTheory.LargeCategory AddCommGrp

Equations

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

instance AddCommGrp.concreteCategory : CategoryTheory.ConcreteCategory AddCommGrp

Equations

• AddCommGrp.concreteCategory = id inferInstance

instance CommGrp.concreteCategory : CategoryTheory.ConcreteCategory CommGrp

Equations

• CommGrp.concreteCategory = id inferInstance

instance AddCommGrp.instCoeSortType : CoeSort AddCommGrp (Type u_1)

Equations

• AddCommGrp.instCoeSortType = { coe := fun (X : AddCommGrp) => ↑X }

instance CommGrp.instCoeSortType : CoeSort CommGrp (Type u_1)

Equations

• CommGrp.instCoeSortType = { coe := fun (X : CommGrp) => ↑X }

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

Equations

• X.addCommGroupInstance = X.str

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

Equations

• X.commGroupInstance = X.str

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

Construct a bundled AddCommGroup from the underlying type and typeclass.

Equations

• AddCommGrp.of G = CategoryTheory.Bundled.of G

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

Construct a bundled CommGroup from the underlying type and typeclass.

Equations

• CommGrp.of G = CategoryTheory.Bundled.of G

instance AddCommGrp.instInhabited : Inhabited AddCommGrp

Equations

• AddCommGrp.instInhabited = { default := AddCommGrp.of PUnit.{?u.1 + 1} }

instance CommGrp.instInhabited : Inhabited CommGrp

Equations

• CommGrp.instInhabited = { default := CommGrp.of PUnit.{?u.1 + 1} }

@[simp]

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

@[simp]

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

@[simp]

theorem AddCommGrp.coe_comp' {G : Type u_1} {H : Type u_1} {K : Type u_1} [AddCommGroup G] [AddCommGroup H] [AddCommGroup K] (f : G →+ H) (g : H →+ K) : ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f

@[simp]

theorem CommGrp.coe_comp' {G : Type u_1} {H : Type u_1} {K : Type u_1} [CommGroup G] [CommGroup H] [CommGroup K] (f : G →* H) (g : H →* K) : ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f

@[simp]

theorem AddCommGrp.coe_id' {G : Type u_1} [AddCommGroup G] : ⇑(CategoryTheory.CategoryStruct.id (AddCommGrp.of G)) = id

@[simp]

theorem CommGrp.coe_id' {G : Type u_1} [CommGroup G] : ⇑(CategoryTheory.CategoryStruct.id (CommGrp.of G)) = id

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

Equations

• AddCommGrp.ofUnique G = i

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

Equations

• CommGrp.ofUnique G = i

instance AddCommGrp.hasForgetToAddGroup : CategoryTheory.HasForget₂ AddCommGrp AddGrp

Equations

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

instance CommGrp.hasForgetToGroup : CategoryTheory.HasForget₂ CommGrp Grp

Equations

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

instance AddCommGrp.instCoeAddGrp : Coe AddCommGrp AddGrp

Equations

• AddCommGrp.instCoeAddGrp = { coe := (CategoryTheory.forget₂ AddCommGrp AddGrp).obj }

instance CommGrp.instCoeGrp : Coe CommGrp Grp

Equations

• CommGrp.instCoeGrp = { coe := (CategoryTheory.forget₂ CommGrp Grp).obj }

instance AddCommGrp.hasForgetToAddCommMonCat : CategoryTheory.HasForget₂ AddCommGrp AddCommMonCat

Equations

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

instance CommGrp.hasForgetToCommMonCat : CategoryTheory.HasForget₂ CommGrp CommMonCat

Equations

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

instance AddCommGrp.instCoeCommMonCat : Coe AddCommGrp AddCommMonCat

Equations

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

instance CommGrp.instCoeCommMonCat : Coe CommGrp CommMonCat

Equations

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

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

Equations

• G.instZeroHom H = inferInstance

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

Equations

• G.instOneHom H = inferInstance

@[simp]

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

@[simp]

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

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

Typecheck an AddMonoidHom as a morphism in AddCommGroup.

Equations

• AddCommGrp.ofHom f = f

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

Typecheck a MonoidHom as a morphism in CommGroup.

Equations

• CommGrp.ofHom f = f

@[simp]

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

@[simp]

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

theorem AddCommGrp.uliftFunctor.proof_2 {X : AddCommGrp} {Y : AddCommGrp} {Z : AddCommGrp} (f : X ⟶ Y) (g : Y ⟶ Z) : { obj := fun (X : AddCommGrp) => AddCommGrp.of (ULift.{u_2, u_1} ↑X), map := fun {X Y : AddCommGrp} (f : X ⟶ Y) => AddCommGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g) = { obj := fun (X : AddCommGrp) => AddCommGrp.of (ULift.{u_2, u_1} ↑X), map := fun {X Y : AddCommGrp} (f : X ⟶ Y) => AddCommGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g)

theorem AddCommGrp.uliftFunctor.proof_1 (X : AddCommGrp) : { obj := fun (X : AddCommGrp) => AddCommGrp.of (ULift.{u_2, u_1} ↑X), map := fun {X Y : AddCommGrp} (f : X ⟶ Y) => AddCommGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X) = { obj := fun (X : AddCommGrp) => AddCommGrp.of (ULift.{u_2, u_1} ↑X), map := fun {X Y : AddCommGrp} (f : X ⟶ Y) => AddCommGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X)

def AddCommGrp.uliftFunctor : CategoryTheory.Functor AddCommGrp AddCommGrp

Universe lift functor for additive commutative groups.

Equations

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

@[simp]

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

@[simp]

theorem AddCommGrp.uliftFunctor_map {X : AddCommGrp} {Y : AddCommGrp} (f : X ⟶ Y) : AddCommGrp.uliftFunctor.map f = AddCommGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom))

@[simp]

theorem CommGrp.uliftFunctor_map {X : CommGrp} {Y : CommGrp} (f : X ⟶ Y) : CommGrp.uliftFunctor.map f = CommGrp.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp (MonoidHom.comp f MulEquiv.ulift.toMonoidHom))

@[simp]

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

def CommGrp.uliftFunctor : CategoryTheory.Functor CommGrp CommGrp

Universe lift functor for commutative groups.

Equations

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

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

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

Equations

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

@[simp]

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

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

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

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

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

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

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

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

Equations

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

Build an addEquiv from an isomorphism in the category AddGroup

Equations

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

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

Build a MulEquiv from an isomorphism in the category Grp.

Equations

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

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

Build an AddEquiv from an isomorphism in the category AddCommGroup.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Build a MulEquiv from an isomorphism in the category CommGroup.

Equations

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

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

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

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

Equations

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

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

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

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

Equations

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

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

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

Equations

• addEquivIsoAddCommGroupIso = { hom := fun (e : ↑X ≃+ ↑Y) => e.toAddCommGrpIso, inv := fun (i : X ≅ Y) => i.addCommGroupIsoToAddEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

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

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

Equations

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

def CategoryTheory.Aut.isoPerm {α : Type u} : Grp.of (CategoryTheory.Aut α) ≅ Grp.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 MulEquiv to the (unbundled) group of permutations.

Equations

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

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

Equations

• AddGrp.forget_reflects_isos = ⋯

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

Equations

• Grp.forget_reflects_isos = ⋯

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

Equations

• AddCommGrp.forget_reflects_isos = ⋯

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

Equations

• CommGrp.forget_reflects_isos = ⋯

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

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

Equations

• GrpMaxAux = AddGrp

@[reducible, inline]

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

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

Equations

• GrpMax = Grp

@[reducible, inline]

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

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

Equations

• AddGrpMax = AddGrp

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

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

Equations

• AddCommGrpMaxAux = AddCommGrp

@[reducible, inline]

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

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

Equations

• CommGrpMax = CommGrp

@[reducible, inline]

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

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

Equations

• AddCommGrpMax = AddCommGrp

@[simp] lemmas for MonoidHom.comp and categorical identities.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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