# mathlibdocumentation

group_theory.quotient_group

@[instance]
def quotient_group.group {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :

Equations
@[instance]

def quotient_group.mk' {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :

The group homomorphism from G to G/N.

Equations

The additive group homomorphism from G to G/N.

@[simp]

@[simp]
theorem quotient_group.ker_mk {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :
= N

@[instance]
def quotient_group.comm_group {G : Type u_1} [comm_group G] (N : subgroup G) :

Equations
@[instance]

@[simp]
theorem quotient_group.coe_one {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :
1 = 1

@[simp]
0 = 0

@[simp]
theorem quotient_group.coe_mul {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (a b : G) :
a * b = (a) * b

@[simp]
(a + b) = a + b

@[simp]
theorem quotient_add_group.coe_neg {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] (a : G) :

@[simp]
theorem quotient_group.coe_inv {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (a : G) :

@[simp]
theorem quotient_group.coe_pow {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (a : G) (n : ) :
(a ^ n) = a ^ n

@[simp]
theorem quotient_group.coe_gpow {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (a : G) (n : ) :
(a ^ n) = a ^ n

def quotient_group.lift {G : Type u} [group G] (N : subgroup G) [nN : N.normal] {H : Type v} [group H] (φ : G →* H) :
(∀ (x : G), x Nφ x = 1)

A group homomorphism φ : G →* H with N ⊆ ker(φ) descends (i.e. lifts) to a group homomorphism G/N →* H.

Equations
def quotient_add_group.lift {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] {H : Type v} [add_group H] (φ : G →+ H) :
(∀ (x : G), x Nφ x = 0)

An add_group homomorphism φ : G →+ H with N ⊆ ker(φ) descends (i.e. lifts) to a group homomorphism G/N →* H.

@[simp]
theorem quotient_add_group.lift_mk {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] {H : Type v} [add_group H] {φ : G →+ H} (HN : ∀ (x : G), x Nφ x = 0) (g : G) :
HN) g = φ g

@[simp]
theorem quotient_group.lift_mk {G : Type u} [group G] (N : subgroup G) [nN : N.normal] {H : Type v} [group H] {φ : G →* H} (HN : ∀ (x : G), x Nφ x = 1) (g : G) :
HN) g = φ g

@[simp]
theorem quotient_add_group.lift_mk' {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] {H : Type v} [add_group H] {φ : G →+ H} (HN : ∀ (x : G), x Nφ x = 0) (g : G) :
HN) = φ g

@[simp]
theorem quotient_group.lift_mk' {G : Type u} [group G] (N : subgroup G) [nN : N.normal] {H : Type v} [group H] {φ : G →* H} (HN : ∀ (x : G), x Nφ x = 1) (g : G) :
HN) = φ g

@[simp]
theorem quotient_group.lift_quot_mk {G : Type u} [group G] (N : subgroup G) [nN : N.normal] {H : Type v} [group H] {φ : G →* H} (HN : ∀ (x : G), x Nφ x = 1) (g : G) :
HN) (quot.mk setoid.r g) = φ g

@[simp]
theorem quotient_add_group.lift_quot_mk {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] {H : Type v} [add_group H] {φ : G →+ H} (HN : ∀ (x : G), x Nφ x = 0) (g : G) :
HN) (quot.mk setoid.r g) = φ g

def quotient_add_group.map {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] {H : Type v} [add_group H] (M : add_subgroup H) [M.normal] (f : G →+ H) :

An add_group homomorphism f : G →+ H induces a map G/N →+ H/M if N ⊆ f⁻¹(M).

def quotient_group.map {G : Type u} [group G] (N : subgroup G) [nN : N.normal] {H : Type v} [group H] (M : subgroup H) [M.normal] (f : G →* H) :

A group homomorphism f : G →* H induces a map G/N →* H/M if N ⊆ f⁻¹(M).

Equations
def quotient_add_group.ker_lift {G : Type u} [add_group G] {H : Type v} [add_group H] (φ : G →+ H) :

The induced map from the quotient by the kernel to the codomain.

def quotient_group.ker_lift {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) :

The induced map from the quotient by the kernel to the codomain.

Equations
@[simp]
theorem quotient_add_group.ker_lift_mk {G : Type u} [add_group G] {H : Type v} [add_group H] (φ : G →+ H) (g : G) :
= φ g

@[simp]
theorem quotient_group.ker_lift_mk {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) (g : G) :
= φ g

@[simp]
theorem quotient_group.ker_lift_mk' {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) (g : G) :
= φ g

@[simp]
theorem quotient_add_group.ker_lift_mk' {G : Type u} [add_group G] {H : Type v} [add_group H] (φ : G →+ H) (g : G) :

theorem quotient_group.ker_lift_injective {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) :

theorem quotient_add_group.injective_ker_lift {G : Type u} [add_group G] {H : Type v} [add_group H] (φ : G →+ H) :

def quotient_group.range_ker_lift {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) :

The induced map from the quotient by the kernel to the range.

Equations
def quotient_add_group.range_ker_lift {G : Type u} [add_group G] {H : Type v} [add_group H] (φ : G →+ H) :

The induced map from the quotient by the kernel to the range.

theorem quotient_group.range_ker_lift_injective {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) :

theorem quotient_add_group.range_ker_lift_injective {G : Type u} [add_group G] {H : Type v} [add_group H] (φ : G →+ H) :

theorem quotient_group.range_ker_lift_surjective {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) :

theorem quotient_add_group.range_ker_lift_surjective {G : Type u} [add_group G] {H : Type v} [add_group H] (φ : G →+ H) :

def quotient_group.quotient_ker_equiv_range {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) :

The first isomorphism theorem (a definition): the canonical isomorphism between G/(ker φ) to range φ.

Equations
def quotient_add_group.quotient_ker_equiv_range {G : Type u} [add_group G] {H : Type v} [add_group H] (φ : G →+ H) :

The first isomorphism theorem (a definition): the canonical isomorphism between G/(ker φ) to range φ.

def quotient_add_group.quotient_ker_equiv_of_surjective {G : Type u} [add_group G] {H : Type v} [add_group H] (φ : G →+ H) :

The canonical isomorphism G/(ker φ) ≃+ H induced by a surjection φ : G →+ H.

def quotient_group.quotient_ker_equiv_of_surjective {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) :

The canonical isomorphism G/(ker φ) ≃* H induced by a surjection φ : G →* H.

Equations