mathlib3 documentation

algebra.category.Group.basic

Category instances for group, add_group, comm_group, and add_comm_group. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We introduce the bundled categories:

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

Construct a bundled AddGroup from the underlying type and typeclass.

Equations
Instances for AddGroup.of
def Group.of (X : Type u) [group X] :

Construct a bundled Group from the underlying type and typeclass.

Equations
Instances for Group.of
def AddGroup.of_hom {X Y : Type u} [add_group X] [add_group Y] (f : X →+ Y) :

Typecheck a add_monoid_hom as a morphism in AddGroup.

Equations
def Group.of_hom {X Y : Type u} [group X] [group Y] (f : X →* Y) :

Typecheck a monoid_hom as a morphism in Group.

Equations
@[simp]
theorem AddGroup.of_hom_apply {X Y : Type u_1} [add_group X] [add_group Y] (f : X →+ Y) (x : X) :
@[simp]
theorem Group.of_hom_apply {X Y : Type u_1} [group X] [group Y] (f : X →* Y) (x : X) :
@[protected, instance]
def Group.group (G : Group) :
Equations
@[protected, instance]
Equations
@[simp]
theorem AddGroup.coe_of (R : Type u) [add_group R] :
@[simp]
theorem Group.coe_of (R : Type u) [group R] :
@[protected, instance]
def AddGroup.of_unique (G : Type u_1) [add_group G] [i : unique G] :
Equations
@[protected, instance]
def Group.of_unique (G : Type u_1) [group G] [i : unique G] :
Equations
@[simp]
theorem AddGroup.zero_apply (G H : AddGroup) (g : G) :
0 g = 0
@[simp]
theorem Group.one_apply (G H : Group) (g : G) :
1 g = 1
@[ext]
theorem Group.ext (G H : Group) (f₁ f₂ : G H) (w : (x : G), f₁ x = f₂ x) :
f₁ = f₂
@[ext]
theorem AddGroup.ext (G H : AddGroup) (f₁ f₂ : G H) (w : (x : G), f₁ x = f₂ x) :
f₁ = f₂
@[reducible]
def Ab  :
Type (u_1+1)

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

Construct a bundled AddCommGroup from the underlying type and typeclass.

Equations
Instances for AddCommGroup.of
def CommGroup.of (G : Type u) [comm_group G] :

Construct a bundled CommGroup from the underlying type and typeclass.

Equations
Instances for CommGroup.of
def CommGroup.of_hom {X Y : Type u} [comm_group X] [comm_group Y] (f : X →* Y) :

Typecheck a monoid_hom as a morphism in CommGroup.

Equations

Typecheck a add_monoid_hom as a morphism in AddCommGroup.

Equations
@[simp]
theorem AddCommGroup.of_hom_apply {X Y : Type u_1} [add_comm_group X] [add_comm_group Y] (f : X →+ Y) (x : X) :
@[simp]
theorem CommGroup.of_hom_apply {X Y : Type u_1} [comm_group X] [comm_group Y] (f : X →* Y) (x : X) :
@[protected, instance]
Equations
@[simp]
@[simp]
theorem CommGroup.coe_of (R : Type u) [comm_group R] :
@[protected, instance]
def CommGroup.of_unique (G : Type u_1) [comm_group G] [i : unique G] :
Equations
@[protected, instance]
Equations
@[simp]
theorem CommGroup.one_apply (G H : CommGroup) (g : G) :
1 g = 1
@[simp]
theorem AddCommGroup.zero_apply (G H : AddCommGroup) (g : G) :
0 g = 0
@[ext]
theorem AddCommGroup.ext (G H : AddCommGroup) (f₁ f₂ : G H) (w : (x : G), f₁ x = f₂ x) :
f₁ = f₂
@[ext]
theorem CommGroup.ext (G H : CommGroup) (f₁ f₂ : G H) (w : (x : G), f₁ x = f₂ x) :
f₁ = f₂

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

Equations
@[simp]
theorem AddCommGroup.as_hom_apply {G : AddCommGroup} (g : G) (i : ) :
@[ext]
theorem AddCommGroup.int_hom_ext {G : AddCommGroup} (f g : AddCommGroup.of G) (w : f 1 = g 1) :
f = g
def mul_equiv.to_Group_iso {X Y : Group} (e : X ≃* Y) :
X Y

Build an isomorphism in the category Group from a mul_equiv between groups.

Equations
def add_equiv.to_AddGroup_iso {X Y : AddGroup} (e : X ≃+ Y) :
X Y

Build an isomorphism in the category AddGroup from an add_equiv between add_groups.

Equations
def mul_equiv.to_CommGroup_iso {X Y : CommGroup} (e : X ≃* Y) :
X Y

Build an isomorphism in the category CommGroup from a mul_equiv between comm_groups.

Equations

Build an isomorphism in the category AddCommGroup from a add_equiv between add_comm_groups.

Equations

Build a mul_equiv from an isomorphism in the category Group.

Equations
@[simp]
theorem category_theory.iso.Group_iso_to_mul_equiv_apply {X Y : Group} (i : X Y) (ᾰ : X) :

Build an add_equiv from an isomorphism in the category AddGroup.

Equations
@[simp]
@[simp]

Build a mul_equiv from an isomorphism in the category CommGroup.

Equations

multiplicative equivalences between groups are the same as (isomorphic to) isomorphisms in Group

Equations

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

Equations

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

Equations

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

Equations

The (bundled) group of automorphisms of a type is isomorphic to the (bundled) group of permutations.

Equations

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

Equations