-
Notifications
You must be signed in to change notification settings - Fork 298
/
abelianization.lean
97 lines (75 loc) · 2.47 KB
/
abelianization.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
/-
Copyright (c) 2018 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Michael Howes
The functor Grp → Ab which is the left adjoint
of the forgetful functor Ab → Grp.
-/
import group_theory.quotient_group
import tactic.group
universes u v
-- let G be a group
variables (G : Type u) [group G]
/-- The commutator subgroup of a group G is the normal subgroup
generated by the commutators [p,q]=`p*q*p⁻¹*q⁻¹` -/
@[derive subgroup.normal]
def commutator : subgroup G :=
subgroup.normal_closure {x | ∃ p q, p * q * p⁻¹ * q⁻¹ = x}
/-- The abelianization of G is the quotient of G by its commutator subgroup -/
def abelianization : Type u :=
quotient_group.quotient (commutator G)
namespace abelianization
local attribute [instance] quotient_group.left_rel
instance : comm_group (abelianization G) :=
{ mul_comm := λ x y, quotient.induction_on₂' x y $ λ a b,
begin
apply quotient.sound,
apply subgroup.subset_normal_closure,
use b⁻¹, use a⁻¹,
group,
end,
.. quotient_group.group _ }
instance : inhabited (abelianization G) := ⟨1⟩
variable {G}
/-- `of` is the canonical projection from G to its abelianization. -/
def of : G →* abelianization G :=
{ to_fun := quotient_group.mk,
map_one' := rfl,
map_mul' := λ x y, rfl }
section lift
-- so far -- built Gᵃᵇ and proved it's an abelian group.
-- defined `of : G → Gᵃᵇ`
-- let A be an abelian group and let f be a group hom from G to A
variables {A : Type v} [comm_group A] (f : G →* A)
lemma commutator_subset_ker : commutator G ≤ f.ker :=
begin
apply subgroup.normal_closure_le_normal,
-- FIXME why is the apply_instance needed?
{ apply_instance },
{ rintros x ⟨p, q, rfl⟩,
simp [monoid_hom.mem_ker, mul_right_comm (f p) (f q)] }
end
def lift : abelianization G →* A :=
quotient_group.lift _ f (λ x h, f.mem_ker.2 $ commutator_subset_ker _ h)
@[simp] lemma lift.of (x : G) : lift f (of x) = f x :=
rfl
theorem lift.unique
(φ : abelianization G →* A)
-- hφ : φ agrees with f on the image of G in Gᵃᵇ
(hφ : ∀ (x : G), φ (of x) = f x)
{x : abelianization G} :
φ x = lift f x :=
quotient_group.induction_on x hφ
end lift
variables {A : Type v} [monoid A]
theorem hom_ext (φ ψ : abelianization G →* A)
(h : φ.comp of = ψ.comp of) : φ = ψ :=
begin
ext x,
apply quotient_group.induction_on x,
intro z,
show φ.comp of z = _,
rw h,
refl,
end
end abelianization