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

Equations

AddGroupCat = CategoryTheory.Bundled AddGroup

Instances For

source

def GroupCat :

Type (u + 1)

The category of groups and group morphisms.

Equations

GroupCat = CategoryTheory.Bundled Group

Instances For

source

instance AddGroupCat.instParentProjectionTypeAddMonoidAddGroupToAddMonoidToSubNegAddMonoid :

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

Equations

AddGroupCat.instParentProjectionTypeAddMonoidAddGroupToAddMonoidToSubNegAddMonoid = AddGroupCat.instParentProjectionTypeAddMonoidAddGroupToAddMonoidToSubNegAddMonoid.proof_1

source

theorem AddGroupCat.instParentProjectionTypeAddMonoidAddGroupToAddMonoidToSubNegAddMonoid.proof_1 :

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

source

instance GroupCat.instParentProjectionTypeMonoidGroupToMonoidToDivInvMonoid :

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

Equations

GroupCat.instParentProjectionTypeMonoidGroupToMonoidToDivInvMonoid = GroupCat.instParentProjectionTypeMonoidGroupToMonoidToDivInvMonoid.proof_1

source

instance instAddGroupCatLargeCategory :

CategoryTheory.LargeCategory AddGroupCat

Equations

instAddGroupCatLargeCategory = CategoryTheory.BundledHom.category (CategoryTheory.BundledHom.MapHom AddMonCat.AssocAddMonoidHom fun {α} h => SubNegMonoid.toAddMonoid)

source

instance AddGroupCat.concreteCategory :

CategoryTheory.ConcreteCategory AddGroupCat

Equations

AddGroupCat.concreteCategory = id inferInstance

source

instance GroupCat.concreteCategory :

CategoryTheory.ConcreteCategory GroupCat

Equations

GroupCat.concreteCategory = id inferInstance

source

instance AddGroupCat.instCoeSortAddGroupCatType :

CoeSort AddGroupCat (Type u_1)

Equations

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

source

instance GroupCat.instCoeSortGroupCatType :

CoeSort GroupCat (Type u_1)

Equations

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

source

instance AddGroupCat.instGroupα (X : AddGroupCat) :

AddGroup ↑X

Equations

AddGroupCat.instGroupα X = X.str

source

instance GroupCat.instGroupα (X : GroupCat) :

Group ↑X

Equations

GroupCat.instGroupα X = X.str

source

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

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

Equations

AddGroupCat.instCoeFunHomAddGroupCatToQuiverToCategoryStructInstAddGroupCatLargeCategoryForAllαAddGroup = { coe := fun f => ↑f }

source

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

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

Equations

GroupCat.instCoeFunHomGroupCatToQuiverToCategoryStructInstGroupCatLargeCategoryForAllαGroup = { coe := fun f => ↑f }

source

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

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

Equations

AddGroupCat.FunLike_instance X Y = let_fun this := inferInstance; this

source

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

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

Equations

GroupCat.FunLike_instance X Y = let_fun this := inferInstance; this

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.

Equations

AddGroupCat.of X = CategoryTheory.Bundled.of X

Instances For

source

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

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

Equations

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

source

instance GroupCat.instInhabitedGroupCat :

Inhabited GroupCat

Equations

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

source

instance AddGroupCat.hasForgetToAddMonCat :

CategoryTheory.HasForget₂ AddGroupCat AddMonCat

Equations

AddGroupCat.hasForgetToAddMonCat = CategoryTheory.BundledHom.forget₂ AddMonCat.AssocAddMonoidHom fun {α} h => SubNegMonoid.toAddMonoid

source

instance GroupCat.hasForgetToMonCat :

CategoryTheory.HasForget₂ GroupCat MonCat

Equations

GroupCat.hasForgetToMonCat = CategoryTheory.BundledHom.forget₂ MonCat.AssocMonoidHom fun {α} h => DivInvMonoid.toMonoid

source

instance AddGroupCat.instCoeAddGroupCatMonCat :

Coe AddGroupCat AddMonCat

Equations

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

source

instance GroupCat.instCoeGroupCatMonCat :

Coe GroupCat MonCat

Equations

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

source

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

Zero (G ⟶ H)

Equations

AddGroupCat.instZeroHomAddGroupCatToQuiverToCategoryStructInstAddGroupCatLargeCategory G H = inferInstance

source

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

One (G ⟶ H)

Equations

GroupCat.instOneHomGroupCatToQuiverToCategoryStructInstGroupCatLargeCategory G H = inferInstance

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.

Equations

AddGroupCat.ofHom f = f

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.

Equations

GroupCat.ofHom f = f

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)

Equations

AddGroupCat.ofUnique G = i

source

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

Unique ↑(GroupCat.of G)

Equations

GroupCat.ofUnique G = i

source

def AddCommGroupCat :

Type (u + 1)

The category of additive commutative groups and group morphisms.

Equations

AddCommGroupCat = CategoryTheory.Bundled AddCommGroup

Instances For

source

def CommGroupCat :

Type (u + 1)

The category of commutative groups and group morphisms.

Equations

CommGroupCat = CategoryTheory.Bundled CommGroup

Instances For

source

@[inline, reducible]

abbrev Ab :

Type (u_1 + 1)

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

Equations

Ab = AddCommGroupCat

Instances For

source

instance AddCommGroupCat.instParentProjectionTypeAddGroupAddCommGroupToAddGroup :

CategoryTheory.BundledHom.ParentProjection @AddCommGroup.toAddGroup

Equations

AddCommGroupCat.instParentProjectionTypeAddGroupAddCommGroupToAddGroup = AddCommGroupCat.instParentProjectionTypeAddGroupAddCommGroupToAddGroup.proof_1

source

theorem AddCommGroupCat.instParentProjectionTypeAddGroupAddCommGroupToAddGroup.proof_1 :

CategoryTheory.BundledHom.ParentProjection @AddCommGroup.toAddGroup

source

instance CommGroupCat.instParentProjectionTypeGroupCommGroupToGroup :

CategoryTheory.BundledHom.ParentProjection @CommGroup.toGroup

Equations

CommGroupCat.instParentProjectionTypeGroupCommGroupToGroup = CommGroupCat.instParentProjectionTypeGroupCommGroupToGroup.proof_1

source

instance instAddCommGroupCatLargeCategory :

CategoryTheory.LargeCategory AddCommGroupCat

Equations

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

source

instance AddCommGroupCat.concreteCategory :

CategoryTheory.ConcreteCategory AddCommGroupCat

Equations

AddCommGroupCat.concreteCategory = id inferInstance

source

instance CommGroupCat.concreteCategory :

CategoryTheory.ConcreteCategory CommGroupCat

Equations

CommGroupCat.concreteCategory = id inferInstance

source

instance AddCommGroupCat.instCoeSortAddCommGroupCatType :

CoeSort AddCommGroupCat (Type u_1)

Equations

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

source

instance CommGroupCat.instCoeSortCommGroupCatType :

CoeSort CommGroupCat (Type u_1)

Equations

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

source

instance AddCommGroupCat.addCommGroupInstance (X : AddCommGroupCat) :

AddCommGroup ↑X

Equations

AddCommGroupCat.addCommGroupInstance X = X.str

source

instance CommGroupCat.commGroupInstance (X : CommGroupCat) :

CommGroup ↑X

Equations

CommGroupCat.commGroupInstance X = X.str

source

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

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

Equations

AddCommGroupCat.instCoeFunHomAddCommGroupCatToQuiverToCategoryStructInstAddCommGroupCatLargeCategoryForAllαAddCommGroup = { coe := fun f => ↑f }

source

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

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

Equations

CommGroupCat.instCoeFunHomCommGroupCatToQuiverToCategoryStructInstCommGroupCatLargeCategoryForAllαCommGroup = { coe := fun f => ↑f }

source

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

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

Equations

AddCommGroupCat.FunLike_instance X Y = let_fun this := inferInstance; this

source

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

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

Equations

CommGroupCat.FunLike_instance X Y = let_fun this := inferInstance; this

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.

Equations

AddCommGroupCat.of G = CategoryTheory.Bundled.of G

Instances For

source

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

Instances For

source

instance AddCommGroupCat.instInhabitedAddCommGroupCat :

Inhabited AddCommGroupCat

Equations

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

source

instance CommGroupCat.instInhabitedCommGroupCat :

Inhabited CommGroupCat

Equations

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

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)

Equations

AddCommGroupCat.ofUnique G = i

source

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

Unique ↑(CommGroupCat.of G)

Equations

CommGroupCat.ofUnique G = i

source

instance AddCommGroupCat.hasForgetToAddGroup :

CategoryTheory.HasForget₂ AddCommGroupCat AddGroupCat

Equations

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

source

instance CommGroupCat.hasForgetToGroup :

CategoryTheory.HasForget₂ CommGroupCat GroupCat

Equations

CommGroupCat.hasForgetToGroup = CategoryTheory.BundledHom.forget₂ (CategoryTheory.BundledHom.MapHom MonCat.AssocMonoidHom fun {α} h => DivInvMonoid.toMonoid) @CommGroup.toGroup

source

instance AddCommGroupCat.instCoeAddCommGroupCatAddGroupCat :

Coe AddCommGroupCat AddGroupCat

Equations

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

source

instance CommGroupCat.instCoeCommGroupCatGroupCat :

Coe CommGroupCat GroupCat

Equations

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

source

instance AddCommGroupCat.hasForgetToAddCommMonCat :

CategoryTheory.HasForget₂ AddCommGroupCat AddCommMonCat

Equations

AddCommGroupCat.hasForgetToAddCommMonCat = CategoryTheory.InducedCategory.hasForget₂ fun G => AddCommMonCat.of ↑G

source

instance CommGroupCat.hasForgetToCommMonCat :

CategoryTheory.HasForget₂ CommGroupCat CommMonCat

Equations

CommGroupCat.hasForgetToCommMonCat = CategoryTheory.InducedCategory.hasForget₂ fun G => CommMonCat.of ↑G

source

instance AddCommGroupCat.instCoeAddCommGroupCatCommMonCat :

Coe AddCommGroupCat AddCommMonCat

Equations

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

source

instance CommGroupCat.instCoeCommGroupCatCommMonCat :

Coe CommGroupCat CommMonCat

Equations

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

source

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

Zero (G ⟶ H)

Equations

AddCommGroupCat.instZeroHomAddCommGroupCatToQuiverToCategoryStructInstAddCommGroupCatLargeCategory G H = inferInstance

source

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

One (G ⟶ H)

Equations

CommGroupCat.instOneHomCommGroupCatToQuiverToCategoryStructInstCommGroupCatLargeCategory G H = inferInstance

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.

Equations

AddCommGroupCat.ofHom f = f

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.

Equations

CommGroupCat.ofHom f = f

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.

Equations

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

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.

Equations

AddEquiv.toAddGroupCatIso e = CategoryTheory.Iso.mk (AddEquiv.toAddMonoidHom e) (AddEquiv.toAddMonoidHom (AddEquiv.symm e))

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.

Equations

MulEquiv.toGroupCatIso e = CategoryTheory.Iso.mk (MulEquiv.toMonoidHom e) (MulEquiv.toMonoidHom (MulEquiv.symm e))

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.

Equations

AddEquiv.toAddCommGroupCatIso e = CategoryTheory.Iso.mk (AddEquiv.toAddMonoidHom e) (AddEquiv.toAddMonoidHom (AddEquiv.symm e))

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.

Equations

MulEquiv.toCommGroupCatIso e = CategoryTheory.Iso.mk (MulEquiv.toMonoidHom e) (MulEquiv.toMonoidHom (MulEquiv.symm e))

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

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

addEquivIsoAddGroupIso = CategoryTheory.Iso.mk (fun e => AddEquiv.toAddGroupCatIso e) fun i => CategoryTheory.Iso.addGroupIsoToAddEquiv i

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

Equations

mulEquivIsoGroupIso = CategoryTheory.Iso.mk (fun e => MulEquiv.toGroupCatIso e) fun i => CategoryTheory.Iso.groupIsoToMulEquiv i

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

Equations

addEquivIsoAddCommGroupIso = CategoryTheory.Iso.mk (fun e => AddEquiv.toAddCommGroupCatIso e) fun i => CategoryTheory.Iso.addCommGroupIsoToAddEquiv i

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

Equations

mulEquivIsoCommGroupIso = CategoryTheory.Iso.mk (fun e => MulEquiv.toCommGroupCatIso e) fun i => CategoryTheory.Iso.commGroupIsoToMulEquiv i

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.

Equations

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

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.

Equations

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

Instances For

source

instance AddGroupCat.forget_reflects_isos :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget AddGroupCat)

Equations

AddGroupCat.forget_reflects_isos = AddGroupCat.forget_reflects_isos.proof_1

source

theorem AddGroupCat.forget_reflects_isos.proof_1 :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget AddGroupCat)

source

instance GroupCat.forget_reflects_isos :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget GroupCat)

Equations

GroupCat.forget_reflects_isos = GroupCat.forget_reflects_isos.proof_1

source

instance AddCommGroupCat.forget_reflects_isos :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget AddCommGroupCat)

Equations

AddCommGroupCat.forget_reflects_isos = AddCommGroupCat.forget_reflects_isos.proof_1

source

theorem AddCommGroupCat.forget_reflects_isos.proof_1 :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget AddCommGroupCat)

source

instance CommGroupCat.forget_reflects_isos :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget CommGroupCat)

Equations

CommGroupCat.forget_reflects_isos = CommGroupCat.forget_reflects_isos.proof_1

source

abbrev GroupCatMaxAux :

Type ((max u1 u2) + 1)

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

Equations

GroupCatMaxAux = AddGroupCat

Instances For

source

@[inline, reducible]

abbrev GroupCatMax :

Type ((max u1 u2) + 1)

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

Equations

GroupCatMax = GroupCat

Instances For

source

@[inline, reducible]

abbrev AddGroupCatMax :

Type ((max u1 u2) + 1)

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

Equations

AddGroupCatMax = AddGroupCat

Instances For

source

abbrev AddCommGroupCatMaxAux :

Type ((max u1 u2) + 1)

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

Equations

AddCommGroupCatMaxAux = AddCommGroupCat

Instances For

source

@[inline, reducible]

abbrev CommGroupCatMax :

Type ((max u1 u2) + 1)

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

Equations

CommGroupCatMax = CommGroupCat

Instances For

source

@[inline, reducible]

abbrev AddCommGroupCatMax :

Type ((max u1 u2) + 1)

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

Equations

AddCommGroupCatMax = AddCommGroupCat

Instances For