quotient_group documented

quotient_group.lean

/-
Copyright (c) 2018 Kevin Buzzard and Patrick Massot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kevin Buzzard, Patrick Massot.

This file is to a certain extent based on `quotient_module.lean` by Johannes Hölzl.

Quotient groups
===============

Main definitions
----------------

This file provides the basic definition of quotient groups. In group_theory.coset we have
the construction of the coset space G/H for G a group and H a subgroup. The main
definition of this file is to show that if N is a normal subgroup of G then G/N also
inherits a group structure.


Summary of results:
-------------------

Say φ : G → H is a group homomorphism, and N ⊆ ker(φ).
Then quotient.lift : G/N → H is defined, and proved to be a group homomorphism.
The triangle G → G/N → H commutes. If M ⊆ H is normal and N ⊆ φ⁻¹(M) then there's
an induced map quotient.map : G/N → H/M. The first isomorphism theorem is proved.
All the results are also proved for additive groups.

Implementation notes
--------------------

`to_additive` is used constantly through the files, to automatically transfer
results from groups with group law * to add_groups with group law +

quotient.lift is the name used in Lean for the map G/N → H induced by a map
G → H with kernel containing N.

References
----------
https://www.google.com/search?q=quotient+groups

tags: groups, first isomorphism theorem, quotient groups,

-/
import group_theory.coset

universes u v

namespace quotient_group

variables {G : Type u} [group G] (N : set G) [normal_subgroup N] {H : Type v} [group H]

/-- The quotient of a group by a normal subgroup has a group structure -/
instance : group (quotient N) :=
{ one := (1 : G),
  mul := λ a b, quotient.lift_on₂' a b
    (λ a b, ((a * b : G) : quotient N))
  (λ a₁ a₂ b₁ b₂ hab₁ hab₂,
      quot.sound
    ((is_subgroup.mul_mem_cancel_left N (is_subgroup.inv_mem hab₂)).1
        (by rw [mul_inv_rev, mul_inv_rev, ← mul_assoc (a₂⁻¹ * a₁⁻¹),
          mul_assoc _ b₂, ← mul_assoc b₂, mul_inv_self, one_mul, mul_assoc (a₂⁻¹)];
          exact normal_subgroup.normal _ hab₁ _))),
  mul_assoc := λ a b c, quotient.induction_on₃' a b c
    (λ a b c, congr_arg mk (mul_assoc a b c)),
  one_mul := λ a, quotient.induction_on' a
    (λ a, congr_arg mk (one_mul a)),
  mul_one := λ a, quotient.induction_on' a
    (λ a, congr_arg mk (mul_one a)),
  inv := λ a, quotient.lift_on' a (λ a, ((a⁻¹ : G) : quotient N))
    (λ a b hab, quotient.sound' begin
      show a⁻¹⁻¹ * b⁻¹ ∈ N,
      rw ← mul_inv_rev,
      exact is_subgroup.inv_mem (is_subgroup.mem_norm_comm hab)
    end),
  mul_left_inv := λ a, quotient.induction_on' a
    (λ a, congr_arg mk (mul_left_inv a)) }

-- These lines are here for technical reasons, to make sure that Lean can
-- port proofs about groups with group law * to groups with group law +
-- There are many others throughout this file.
attribute [to_additive quotient_add_group.add_group._proof_6] quotient_group.group._proof_6
attribute [to_additive quotient_add_group.add_group._proof_5] quotient_group.group._proof_5
attribute [to_additive quotient_add_group.add_group._proof_4] quotient_group.group._proof_4
attribute [to_additive quotient_add_group.add_group._proof_3] quotient_group.group._proof_3
attribute [to_additive quotient_add_group.add_group._proof_2] quotient_group.group._proof_2
attribute [to_additive quotient_add_group.add_group._proof_1] quotient_group.group._proof_1
attribute [to_additive quotient_add_group.add_group] quotient_group.group
attribute [to_additive quotient_add_group.quotient.equations._eqn_1]
  quotient_group.quotient.equations._eqn_1
attribute [to_additive quotient_add_group.add_group.equations._eqn_1]
  quotient_group.group.equations._eqn_1

/-- The quotient map from G to G/N is a group homomorphism -/
instance : is_group_hom (mk : G → quotient N) := ⟨λ _ _, rfl⟩
attribute [to_additive quotient_add_group.is_add_group_hom] quotient_group.is_group_hom
attribute [to_additive quotient_add_group.is_add_group_hom.equations._eqn_1]
  quotient_group.is_group_hom.equations._eqn_1

/-- The kernel of the natural map `G → G/N` is `N` -/
@[simp] lemma ker_mk :
  is_group_hom.ker (quotient_group.mk : G → quotient_group.quotient N) = N :=
begin
  ext g,
  rw [is_group_hom.mem_ker, eq_comm],
  show (((1 : G) : quotient_group.quotient N)) = g ↔ _,
  rw [quotient_group.eq, one_inv, one_mul],
end
attribute [to_additive quotient_add_group.ker_mk] quotient_group.ker_mk

/-- If `G` is abelian and `s` is any subgroup then `G/s` is abelian -/
instance {G : Type*} [comm_group G] (s : set G) [is_subgroup s] : comm_group (quotient s) :=
{ mul_comm := λ a b, quotient.induction_on₂' a b
    (λ a b, congr_arg mk (mul_comm a b)),
  ..@quotient_group.group _ _ s (normal_subgroup_of_comm_group s) }
attribute [to_additive quotient_add_group.add_comm_group._proof_6]
  quotient_group.comm_group._proof_6
attribute [to_additive quotient_add_group.add_comm_group._proof_5]
  quotient_group.comm_group._proof_5
attribute [to_additive quotient_add_group.add_comm_group._proof_4]
  quotient_group.comm_group._proof_4
attribute [to_additive quotient_add_group.add_comm_group._proof_3]
  quotient_group.comm_group._proof_3
attribute [to_additive quotient_add_group.add_comm_group._proof_2]
  quotient_group.comm_group._proof_2
attribute [to_additive quotient_add_group.add_comm_group._proof_1]
  quotient_group.comm_group._proof_1
attribute [to_additive quotient_add_group.add_comm_group] quotient_group.comm_group
attribute [to_additive quotient_add_group.add_comm_group.equations._eqn_1]
  quotient_group.comm_group.equations._eqn_1

-- There is a coercion from `G` to `G/N`; these lemmata below prove that the coercion has
-- some natural properties.
@[simp] lemma coe_one : ((1 : G) : quotient N) = 1 := rfl
@[simp] lemma coe_mul (a b : G) : ((a * b : G) : quotient N) = a * b := rfl
@[simp] lemma coe_inv (a : G) : ((a⁻¹ : G) : quotient N) = a⁻¹ := rfl
@[simp] lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : quotient N) = a ^ n :=
@is_group_hom.map_pow _ _ _ _ mk _ a n

attribute [to_additive quotient_add_group.coe_zero] coe_one
attribute [to_additive quotient_add_group.coe_add] coe_mul
attribute [to_additive quotient_add_group.coe_neg] coe_inv

@[simp] lemma coe_gpow (a : G) (n : ℤ) : ((a ^ n : G) : quotient N) = a ^ n :=
@is_group_hom.map_gpow _ _ _ _ mk _ a n

local notation ` Q ` := quotient N

/-- The universal property of quotients. If `φ : G → H` is a group homomorphism
and `HN` is a proof that `N ⊆ ker(φ)`, then `φ` induces a map from `G/N` to `H`, and
this map is called `quotient_group.lift φ HN`. -/
def lift (φ : G → H) [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (q : Q) : H :=
q.lift_on' φ $ assume a b (hab : a⁻¹ * b ∈ N),
(calc φ a = φ a * 1           : by simp
...       = φ a * φ (a⁻¹ * b) : by rw HN (a⁻¹ * b) hab
...       = φ (a * (a⁻¹ * b)) : by rw is_group_hom.map_mul φ a (a⁻¹ * b)
...       = φ b               : by simp)
attribute [to_additive quotient_add_group.lift._proof_1] lift._proof_1
attribute [to_additive quotient_add_group.lift] lift
attribute [to_additive quotient_add_group.lift.equations._eqn_1] lift.equations._eqn_1

/-- The proof that quotient_group.lift composed with the map `G → G/N` is `φ` -/
@[simp] lemma lift_mk {φ : G → H} [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (g : G) :
  lift N φ HN (g : Q) = φ g := rfl
attribute [to_additive quotient_add_group.lift_mk] lift_mk

/-- The proof that quotient_group.lift composed with the map `G → G/N` is `φ` -/
@[simp] lemma lift_mk' {φ : G → H} [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (g : G) :
  lift N φ HN (mk g : Q) = φ g := rfl
attribute [to_additive quotient_add_group.lift_mk'] lift_mk'

/-- The construction of a map `quotient_group.map : G/N → H/M` for a
    group hom `f: G → H` such that `N ⊆ f^{-1}(M)` -/
def map (M : set H) [normal_subgroup M] (f : G → H) [is_group_hom f] (h : N ⊆ f ⁻¹' M) :
  quotient N → quotient M :=
begin
  haveI : is_group_hom ((mk : H → quotient M) ∘ f) := is_group_hom.comp _ _,
  refine quotient_group.lift N (mk ∘ f) _,
  assume x hx,
  refine quotient_group.eq.2 _,
  rw [mul_one, is_subgroup.inv_mem_iff],
  exact h hx,
end

attribute [to_additive quotient_add_group.map._proof_1] map._proof_1
attribute [to_additive quotient_add_group.map._proof_2] map._proof_2
attribute [to_additive quotient_add_group.map] map

variables (φ : G → H) [is_group_hom φ] (HN : ∀x∈N, φ x = 1)

/-- the proof that quotient_group.lift is a group homomorphism -/
instance is_group_hom_quotient_lift  :
  is_group_hom (lift N φ HN) :=
⟨λ q r, quotient.induction_on₂' q r $ λ a b,
  show φ (a * b) = φ a * φ b, from is_group_hom.map_mul φ a b⟩
attribute [to_additive quotient_add_group.is_add_group_hom_quotient_lift] quotient_group.is_group_hom_quotient_lift
attribute [to_additive quotient_add_group.is_add_group_hom_quotient_lift.equations._eqn_1] quotient_group.is_group_hom_quotient_lift.equations._eqn_1

/-- the proof that `quotient_group.map : G/N → H/M` -/
@[to_additive quotient_add_group.map_is_add_group_hom]
instance map_is_group_hom (M : set H) [normal_subgroup M]
(f : G → H) [is_group_hom f] (h : N ⊆ f ⁻¹' M) : is_group_hom (map N M f h) :=
quotient_group.is_group_hom_quotient_lift _ _ _

open function is_group_hom

/-- Given `φ : G → H`, `quotient_map.ker_lift` is the induced map `G/ker(φ) → H` -/
def ker_lift : quotient (ker φ) → H :=
lift _ φ $ λ g, (mem_ker φ).mp

attribute [to_additive quotient_add_group.ker_lift._proof_1] quotient_group.ker_lift._proof_1
attribute [to_additive quotient_add_group.ker_lift._proof_2] quotient_group.ker_lift._proof_2
attribute [to_additive quotient_add_group.ker_lift] quotient_group.ker_lift
attribute [to_additive quotient_add_group.ker_lift.equations._eqn_1] quotient_group.ker_lift.equations._eqn_1

/-- `G → G/ker(φ)` composed with `quotient_map.ker_lift` is just `φ` -/
@[simp, to_additive quotient_add_group.ker_lift_mk]
lemma ker_lift_mk (g : G) : (ker_lift φ) g = φ g :=
lift_mk _ _ _

/-- `G → G/ker(φ)` composed with `quotient_map.ker_lift` is just `φ` -/
@[simp, to_additive quotient_add_group.ker_lift_mk']
lemma ker_lift_mk' (g : G) : (ker_lift φ) (mk g) = φ g :=
lift_mk' _ _ _

/-- `quotient_map.ker_lift` is a group hom -/
@[to_additive quotient_add_group.ker_lift_is_add_group_hom]
instance ker_lift_is_group_hom : is_group_hom (ker_lift φ) :=
quotient_group.is_group_hom_quotient_lift _ _ _

/-- `quotient_map.ker_lift` is an injective map -/
@[to_additive quotient_add_group.injective_ker_lift]
lemma injective_ker_lift : injective (ker_lift φ) :=
assume a b, quotient.induction_on₂' a b $ assume a b (h : φ a = φ b), quotient.sound' $
show a⁻¹ * b ∈ ker φ, by rw [mem_ker φ,
  is_group_hom.map_mul φ, ← h, is_group_hom.map_inv φ, inv_mul_self]

/-- The first isomorphism theorem for groups under multiplication -/
noncomputable def quotient_ker_equiv_range : (quotient (ker φ)) ≃ set.range φ :=
@equiv.of_bijective _ (set.range φ) (λ x, ⟨lift (ker φ) φ
  (by simp [mem_ker]) x, by exact quotient.induction_on' x (λ x, ⟨x, rfl⟩)⟩)
⟨λ a b h, injective_ker_lift _ (subtype.mk.inj h),
  λ ⟨x, y, hy⟩, ⟨mk y, subtype.eq hy⟩⟩

--@[to_additive quotient_add_group.quotient_ker_equiv_range]

attribute [to_additive quotient_add_group.quotient_ker_equiv_range._proof_1]
  quotient_group.quotient_ker_equiv_range._proof_1
attribute [to_additive quotient_add_group.quotient_ker_equiv_range._proof_2]
  quotient_group.quotient_ker_equiv_range._proof_2
attribute [to_additive quotient_add_group.quotient_ker_equiv_range._proof_3]
  quotient_group.quotient_ker_equiv_range._proof_3
attribute [to_additive quotient_add_group.quotient_ker_equiv_range._proof_4]
  quotient_group.quotient_ker_equiv_range._proof_4
attribute [to_additive quotient_add_group.quotient_ker_equiv_range._match_1]
  quotient_group.quotient_ker_equiv_range._match_1
attribute [to_additive quotient_add_group.quotient_ker_equiv_range._proof_5]
  quotient_group.quotient_ker_equiv_range._proof_5
attribute [to_additive quotient_add_group.quotient_ker_equiv_range]
  quotient_group.quotient_ker_equiv_range

/-- If `φ : G → H` is a surjection then `G/ker(φ) ≅ H` -/
noncomputable def quotient_ker_equiv_of_surjective (hφ : function.surjective φ) :
  (quotient (ker φ)) ≃ H :=
calc (quotient_group.quotient (is_group_hom.ker φ)) ≃ set.range φ : quotient_ker_equiv_range _
... ≃ H : ⟨λ a, a.1, λ b, ⟨b, hφ b⟩, λ ⟨_, _⟩, rfl, λ _, rfl⟩

end quotient_group

namespace quotient_add_group
open is_add_group_hom

variables {G : Type u} [_root_.add_group G] (N : set G) [normal_add_subgroup N] {H : Type v} [_root_.add_group H]
variables (φ : G → H) [_root_.is_add_group_hom φ]

/-- If `φ : G → H` is a surjection of additive groups then `G/ker(φ) ≅ H` -/
noncomputable def quotient_ker_equiv_of_surjective (hφ : function.surjective φ) : (quotient (ker φ)) ≃ H :=
@quotient_group.quotient_ker_equiv_of_surjective (multiplicative G) _ (multiplicative H) _ φ _ hφ

attribute [to_additive quotient_add_group.quotient_ker_equiv_range] quotient_group.quotient_ker_equiv_range
attribute [to_additive quotient_add_group.quotient_ker_equiv_of_surjective] quotient_group.quotient_ker_equiv_of_surjective

end quotient_add_group