mathlib documentation

algebra.category.Group.basic

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

We introduce the bundled categories:

def AddGroup  :
Type (u+1)

The category of additive groups and group morphisms

def Group  :
Type (u+1)

The category of groups and group morphisms.

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

Construct a bundled AddGroup from the underlying type and typeclass.

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

Construct a bundled Group from the underlying type and typeclass.

Equations
@[instance]
def Group.group (G : Group) :

Equations
@[instance]

@[simp]
theorem AddGroup.coe_of (R : Type u) [add_group R] :

@[simp]
theorem Group.coe_of (R : Type u) [group R] :

@[instance]

Equations
@[instance]

Equations
@[instance]

@[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) :
(∀ (x : G), f₁ x = f₂ x)f₁ = f₂

@[ext]
theorem AddGroup.ext (G H : AddGroup) (f₁ f₂ : G H) :
(∀ (x : G), f₁ x = f₂ x)f₁ = f₂

def AddCommGroup  :
Type (u+1)

The category of additive commutative groups and group morphisms.

def CommGroup  :
Type (u+1)

The category of commutative groups and group morphisms.

Equations
def Ab  :
Type (u_1+1)

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

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

Construct a bundled AddCommGroup from the underlying type and typeclass.

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

Construct a bundled CommGroup from the underlying type and typeclass.

Equations
@[simp]
theorem AddCommGroup.coe_of (R : Type u) [add_comm_group R] :

@[simp]
theorem CommGroup.coe_of (R : Type u) [comm_group R] :

@[instance]

@[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) :
(∀ (x : G), f₁ x = f₂ x)f₁ = f₂

@[ext]
theorem CommGroup.ext (G H : CommGroup) (f₁ f₂ : G H) :
(∀ (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) :
f 1 = g 1f = g

def mul_equiv.to_Group_iso {X Y : Type u} [group X] [group Y] :
X ≃* Y(Group.of X Group.of Y)

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

Equations
def add_equiv.to_AddGroup_iso {X Y : Type u} [add_group X] [add_group Y] :

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

def mul_equiv.to_CommGroup_iso {X Y : Type u} [comm_group X] [comm_group 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.

Build a mul_equiv from an isomorphism in the category Group.

Equations

Build an add_equiv from an isomorphism in the category AddGroup.

Build an add_equiv from an isomorphism in the category AddCommGroup.

Build a mul_equiv from an isomorphism in the category CommGroup.

Equations
def mul_equiv_iso_Group_iso {X Y : Type u} [group X] [group Y] :

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

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

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