@[instance]
Equations
- quotient_group.group N = {mul := quotient.map₂' has_mul.mul _, mul_assoc := _, one := ↑1, one_mul := _, mul_one := _, inv := λ (a : quotient_group.quotient N), quotient.lift_on' a (λ (a : G), ↑a⁻¹) _, mul_left_inv := _}
@[instance]
The group homomorphism from G to G/N.
Equations
The additive group homomorphism from G to G/N.
@[simp]
theorem
quotient_add_group.ker_mk
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal] :
(quotient_add_group.mk' N).ker = N
@[simp]
theorem
quotient_group.ker_mk
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal] :
(quotient_group.mk' N).ker = N
@[instance]
Equations
- quotient_group.comm_group N = {mul := group.mul (quotient_group.group N), mul_assoc := _, one := group.one (quotient_group.group N), one_mul := _, mul_one := _, inv := group.inv (quotient_group.group N), mul_left_inv := _, mul_comm := _}
@[instance]
@[simp]
theorem
quotient_add_group.coe_zero
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal] :
@[simp]
theorem
quotient_add_group.coe_neg
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(a : G) :
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) → quotient_add_group.quotient N →+ H
An add_group homomorphism φ : G →+ H with N ⊆ ker(φ)
descends (i.e. lifts) to a group homomorphism G/N →* H.
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) → quotient_group.quotient N →* H
A group homomorphism φ : G →* H with N ⊆ ker(φ) descends (i.e. lifts) to a
group homomorphism G/N →* H.
Equations
- quotient_group.lift N φ HN = monoid_hom.mk' (λ (q : quotient_group.quotient N), quotient.lift_on' q ⇑φ _) _
@[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) :
⇑(quotient_add_group.lift N φ 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) :
⇑(quotient_group.lift N φ HN) (quotient_group.mk 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) :
⇑(quotient_add_group.lift N φ HN) (quotient_add_group.mk 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) :
N ≤ subgroup.comap f M → quotient_group.quotient N →* quotient_group.quotient M
A group homomorphism f : G →* H induces a map G/N →* H/M if N ⊆ f⁻¹(M).
Equations
- quotient_group.map N M f h = quotient_group.lift N ((quotient_group.mk' M).comp f) _
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.
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) :
⇑(quotient_add_group.ker_lift φ) ↑g = ⇑φ g
@[simp]
theorem
quotient_group.ker_lift_mk
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H)
(g : G) :
⇑(quotient_group.ker_lift φ) ↑g = ⇑φ g
@[simp]
theorem
quotient_group.ker_lift_mk'
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H)
(g : G) :
⇑(quotient_group.ker_lift φ) (quotient_group.mk 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) :
⇑(quotient_add_group.ker_lift φ) (quotient_add_group.mk 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) :
quotient_group.quotient φ.ker →* ↥(φ.range)
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_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_injective
{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) :
theorem
quotient_group.range_ker_lift_surjective
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H) :
def
quotient_group.quotient_ker_equiv_range
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H) :
quotient_group.quotient φ.ker ≃* ↥(φ.range)
The first isomorphism theorem (a definition): the canonical isomorphism between
G/(ker φ) to range φ.
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.