split group_constructions into several files
This commit is contained in:
Egbert Rijke
parent
258671578d
commit
038bbb8be3
6 changed files with 707 additions and 629 deletions
33
algebra/direct_sum.hlean
Normal file
33
algebra/direct_sum.hlean
Normal file
|
|
@ -0,0 +1,33 @@
|
||||||
|
/-
|
||||||
|
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||||
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
Authors: Floris van Doorn, Egbert Rijke
|
||||||
|
|
||||||
|
Constructions with groups
|
||||||
|
-/
|
||||||
|
|
||||||
|
import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group .product_group .free_group .free_commutative_group
|
||||||
|
|
||||||
|
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
|
||||||
|
equiv
|
||||||
|
namespace group
|
||||||
|
|
||||||
|
variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
|
||||||
|
{A B : CommGroup}
|
||||||
|
|
||||||
|
variables (X : Set) {l l' : list (X ⊎ X)}
|
||||||
|
|
||||||
|
section
|
||||||
|
|
||||||
|
parameters {I : Set} (Y : I → CommGroup)
|
||||||
|
|
||||||
|
definition dirsum_carrier : CommGroup := free_comm_group (trunctype.mk (Σi, Y i) _)
|
||||||
|
local abbreviation ι := @free_comm_group_inclusion
|
||||||
|
inductive dirsum_rel : dirsum_carrier → Type :=
|
||||||
|
| rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹)
|
||||||
|
|
||||||
|
definition direct_sum : CommGroup := quotient_comm_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
end group
|
||||||
194
algebra/free_commutative_group.hlean
Normal file
194
algebra/free_commutative_group.hlean
Normal file
|
|
@ -0,0 +1,194 @@
|
||||||
|
/-
|
||||||
|
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||||
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
Authors: Floris van Doorn, Egbert Rijke
|
||||||
|
|
||||||
|
Constructions with groups
|
||||||
|
-/
|
||||||
|
|
||||||
|
import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group .product_group .free_group
|
||||||
|
|
||||||
|
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
|
||||||
|
equiv
|
||||||
|
namespace group
|
||||||
|
|
||||||
|
variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
|
||||||
|
{A B : CommGroup}
|
||||||
|
|
||||||
|
variables (X : Set) {l l' : list (X ⊎ X)}
|
||||||
|
|
||||||
|
/- Free Commutative Group of a set -/
|
||||||
|
namespace free_comm_group
|
||||||
|
|
||||||
|
inductive fcg_rel : list (X ⊎ X) → list (X ⊎ X) → Type :=
|
||||||
|
| rrefl : Πl, fcg_rel l l
|
||||||
|
| cancel1 : Πx, fcg_rel [inl x, inr x] []
|
||||||
|
| cancel2 : Πx, fcg_rel [inr x, inl x] []
|
||||||
|
| rflip : Πx y, fcg_rel [x, y] [y, x]
|
||||||
|
| resp_append : Π{l₁ l₂ l₃ l₄}, fcg_rel l₁ l₂ → fcg_rel l₃ l₄ →
|
||||||
|
fcg_rel (l₁ ++ l₃) (l₂ ++ l₄)
|
||||||
|
| rtrans : Π{l₁ l₂ l₃}, fcg_rel l₁ l₂ → fcg_rel l₂ l₃ →
|
||||||
|
fcg_rel l₁ l₃
|
||||||
|
|
||||||
|
open fcg_rel
|
||||||
|
local abbreviation R [reducible] := fcg_rel
|
||||||
|
attribute fcg_rel.rrefl [refl]
|
||||||
|
attribute fcg_rel.rtrans [trans]
|
||||||
|
|
||||||
|
definition fcg_carrier [reducible] : Type := set_quotient (λx y, ∥R X x y∥)
|
||||||
|
local abbreviation FG := fcg_carrier
|
||||||
|
|
||||||
|
definition is_reflexive_R : is_reflexive (λx y, ∥R X x y∥) :=
|
||||||
|
begin constructor, intro s, apply tr, unfold R end
|
||||||
|
local attribute is_reflexive_R [instance]
|
||||||
|
|
||||||
|
variable {X}
|
||||||
|
theorem rel_respect_flip (r : R X l l') : R X (map sum.flip l) (map sum.flip l') :=
|
||||||
|
begin
|
||||||
|
induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂,
|
||||||
|
{ reflexivity},
|
||||||
|
{ repeat esimp [map], exact cancel2 x},
|
||||||
|
{ repeat esimp [map], exact cancel1 x},
|
||||||
|
{ repeat esimp [map], apply rflip},
|
||||||
|
{ rewrite [+map_append], exact resp_append IH₁ IH₂},
|
||||||
|
{ exact rtrans IH₁ IH₂}
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem rel_respect_reverse (r : R X l l') : R X (reverse l) (reverse l') :=
|
||||||
|
begin
|
||||||
|
induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂,
|
||||||
|
{ reflexivity},
|
||||||
|
{ repeat esimp [map], exact cancel2 x},
|
||||||
|
{ repeat esimp [map], exact cancel1 x},
|
||||||
|
{ repeat esimp [map], apply rflip},
|
||||||
|
{ rewrite [+reverse_append], exact resp_append IH₂ IH₁},
|
||||||
|
{ exact rtrans IH₁ IH₂}
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem rel_cons_concat (l s) : R X (s :: l) (concat s l) :=
|
||||||
|
begin
|
||||||
|
induction l with t l IH,
|
||||||
|
{ reflexivity},
|
||||||
|
{ rewrite [concat_cons], transitivity (t :: s :: l),
|
||||||
|
{ exact resp_append !rflip !rrefl},
|
||||||
|
{ exact resp_append (rrefl [t]) IH}}
|
||||||
|
end
|
||||||
|
|
||||||
|
definition fcg_one [constructor] : FG X := class_of []
|
||||||
|
definition fcg_inv [unfold 3] : FG X → FG X :=
|
||||||
|
quotient_unary_map (reverse ∘ map sum.flip)
|
||||||
|
(λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip))
|
||||||
|
definition fcg_mul [unfold 3 4] : FG X → FG X → FG X :=
|
||||||
|
quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s))))
|
||||||
|
|
||||||
|
section
|
||||||
|
local notation 1 := fcg_one
|
||||||
|
local postfix ⁻¹ := fcg_inv
|
||||||
|
local infix * := fcg_mul
|
||||||
|
|
||||||
|
theorem fcg_mul_assoc (g₁ g₂ g₃ : FG X) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g₁,
|
||||||
|
refine set_quotient.rec_prop _ g₂,
|
||||||
|
refine set_quotient.rec_prop _ g₃,
|
||||||
|
clear g₁ g₂ g₃, intro g₁ g₂ g₃,
|
||||||
|
exact ap class_of !append.assoc
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem fcg_one_mul (g : FG X) : 1 * g = g :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g, clear g, intro g,
|
||||||
|
exact ap class_of !append_nil_left
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem fcg_mul_one (g : FG X) : g * 1 = g :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g, clear g, intro g,
|
||||||
|
exact ap class_of !append_nil_right
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem fcg_mul_left_inv (g : FG X) : g⁻¹ * g = 1 :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g, clear g, intro g,
|
||||||
|
apply eq_of_rel, apply tr,
|
||||||
|
induction g with s l IH,
|
||||||
|
{ reflexivity},
|
||||||
|
{ rewrite [▸*, map_cons, reverse_cons, concat_append],
|
||||||
|
refine rtrans _ IH,
|
||||||
|
apply resp_append, reflexivity,
|
||||||
|
change R X ([flip s, s] ++ l) ([] ++ l),
|
||||||
|
apply resp_append,
|
||||||
|
induction s, apply cancel2, apply cancel1,
|
||||||
|
reflexivity}
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem fcg_mul_comm (g h : FG X) : g * h = h * g :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g, clear g, intro g,
|
||||||
|
refine set_quotient.rec_prop _ h, clear h, intro h,
|
||||||
|
apply eq_of_rel, apply tr,
|
||||||
|
revert h, induction g with s l IH: intro h,
|
||||||
|
{ rewrite [append_nil_left, append_nil_right]},
|
||||||
|
{ rewrite [append_cons,-concat_append],
|
||||||
|
transitivity concat s (l ++ h), apply rel_cons_concat,
|
||||||
|
rewrite [-append_concat], apply IH}
|
||||||
|
end
|
||||||
|
end
|
||||||
|
end free_comm_group open free_comm_group
|
||||||
|
|
||||||
|
variables (X)
|
||||||
|
definition group_free_comm_group [constructor] : comm_group (fcg_carrier X) :=
|
||||||
|
comm_group.mk fcg_mul _ fcg_mul_assoc fcg_one fcg_one_mul fcg_mul_one
|
||||||
|
fcg_inv fcg_mul_left_inv fcg_mul_comm
|
||||||
|
|
||||||
|
definition free_comm_group [constructor] : CommGroup :=
|
||||||
|
CommGroup.mk _ (group_free_comm_group X)
|
||||||
|
|
||||||
|
/- The universal property of the free commutative group -/
|
||||||
|
variables {X A}
|
||||||
|
definition free_comm_group_inclusion [constructor] (x : X) : free_comm_group X :=
|
||||||
|
class_of [inl x]
|
||||||
|
|
||||||
|
theorem fgh_helper_respect_comm_rel (f : X → A) (r : fcg_rel X l l')
|
||||||
|
: Π(g : A), foldl (fgh_helper f) g l = foldl (fgh_helper f) g l' :=
|
||||||
|
begin
|
||||||
|
induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂: intro g,
|
||||||
|
{ reflexivity},
|
||||||
|
{ unfold [foldl], apply mul_inv_cancel_right},
|
||||||
|
{ unfold [foldl], apply inv_mul_cancel_right},
|
||||||
|
{ unfold [foldl, fgh_helper], apply mul.right_comm},
|
||||||
|
{ rewrite [+foldl_append, IH₁, IH₂]},
|
||||||
|
{ exact !IH₁ ⬝ !IH₂}
|
||||||
|
end
|
||||||
|
|
||||||
|
definition free_comm_group_hom [constructor] (f : X → A) : free_comm_group X →g A :=
|
||||||
|
begin
|
||||||
|
fapply homomorphism.mk,
|
||||||
|
{ intro g, refine set_quotient.elim _ _ g,
|
||||||
|
{ intro l, exact foldl (fgh_helper f) 1 l},
|
||||||
|
{ intro l l' r, esimp at *, refine trunc.rec _ r, clear r, intro r,
|
||||||
|
exact fgh_helper_respect_comm_rel f r 1}},
|
||||||
|
{ refine set_quotient.rec_prop _, intro l, refine set_quotient.rec_prop _, intro l',
|
||||||
|
esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul}
|
||||||
|
end
|
||||||
|
|
||||||
|
definition fn_of_free_comm_group_hom [unfold_full] (φ : free_comm_group X →g A) : X → A :=
|
||||||
|
φ ∘ free_comm_group_inclusion
|
||||||
|
|
||||||
|
variables (X A)
|
||||||
|
definition free_comm_group_hom_equiv_fn : (free_comm_group X →g A) ≃ (X → A) :=
|
||||||
|
begin
|
||||||
|
fapply equiv.MK,
|
||||||
|
{ exact fn_of_free_comm_group_hom},
|
||||||
|
{ exact free_comm_group_hom},
|
||||||
|
{ intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul},
|
||||||
|
{ intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp,
|
||||||
|
induction l with s l IH,
|
||||||
|
{ esimp [foldl], symmetry, exact to_respect_one φ},
|
||||||
|
{ rewrite [foldl_cons, fgh_helper_mul],
|
||||||
|
refine _ ⬝ (to_respect_mul φ (class_of [s]) (class_of l))⁻¹,
|
||||||
|
rewrite [▸*,IH], induction s: rewrite [▸*, one_mul], apply ap (λx, x * _),
|
||||||
|
exact !to_respect_inv⁻¹}}
|
||||||
|
end
|
||||||
|
|
||||||
|
end group
|
||||||
179
algebra/free_group.hlean
Normal file
179
algebra/free_group.hlean
Normal file
|
|
@ -0,0 +1,179 @@
|
||||||
|
/-
|
||||||
|
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||||
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
Authors: Floris van Doorn, Egbert Rijke
|
||||||
|
|
||||||
|
Constructions with groups
|
||||||
|
-/
|
||||||
|
|
||||||
|
import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group .product_group
|
||||||
|
|
||||||
|
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
|
||||||
|
equiv
|
||||||
|
namespace group
|
||||||
|
|
||||||
|
variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
|
||||||
|
{A B : CommGroup}
|
||||||
|
|
||||||
|
/- Free Group of a set -/
|
||||||
|
variables (X : Set) {l l' : list (X ⊎ X)}
|
||||||
|
namespace free_group
|
||||||
|
|
||||||
|
inductive free_group_rel : list (X ⊎ X) → list (X ⊎ X) → Type :=
|
||||||
|
| rrefl : Πl, free_group_rel l l
|
||||||
|
| cancel1 : Πx, free_group_rel [inl x, inr x] []
|
||||||
|
| cancel2 : Πx, free_group_rel [inr x, inl x] []
|
||||||
|
| resp_append : Π{l₁ l₂ l₃ l₄}, free_group_rel l₁ l₂ → free_group_rel l₃ l₄ →
|
||||||
|
free_group_rel (l₁ ++ l₃) (l₂ ++ l₄)
|
||||||
|
| rtrans : Π{l₁ l₂ l₃}, free_group_rel l₁ l₂ → free_group_rel l₂ l₃ →
|
||||||
|
free_group_rel l₁ l₃
|
||||||
|
|
||||||
|
open free_group_rel
|
||||||
|
local abbreviation R [reducible] := free_group_rel
|
||||||
|
attribute free_group_rel.rrefl [refl]
|
||||||
|
|
||||||
|
definition free_group_carrier [reducible] : Type := set_quotient (λx y, ∥R X x y∥)
|
||||||
|
local abbreviation FG := free_group_carrier
|
||||||
|
|
||||||
|
definition is_reflexive_R : is_reflexive (λx y, ∥R X x y∥) :=
|
||||||
|
begin constructor, intro s, apply tr, unfold R end
|
||||||
|
local attribute is_reflexive_R [instance]
|
||||||
|
|
||||||
|
variable {X}
|
||||||
|
theorem rel_respect_flip (r : R X l l') : R X (map sum.flip l) (map sum.flip l') :=
|
||||||
|
begin
|
||||||
|
induction r with l x x l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂,
|
||||||
|
{ reflexivity},
|
||||||
|
{ repeat esimp [map], exact cancel2 x},
|
||||||
|
{ repeat esimp [map], exact cancel1 x},
|
||||||
|
{ rewrite [+map_append], exact resp_append IH₁ IH₂},
|
||||||
|
{ exact rtrans IH₁ IH₂}
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem rel_respect_reverse (r : R X l l') : R X (reverse l) (reverse l') :=
|
||||||
|
begin
|
||||||
|
induction r with l x x l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂,
|
||||||
|
{ reflexivity},
|
||||||
|
{ repeat esimp [map], exact cancel2 x},
|
||||||
|
{ repeat esimp [map], exact cancel1 x},
|
||||||
|
{ rewrite [+reverse_append], exact resp_append IH₂ IH₁},
|
||||||
|
{ exact rtrans IH₁ IH₂}
|
||||||
|
end
|
||||||
|
|
||||||
|
definition free_group_one [constructor] : FG X := class_of []
|
||||||
|
definition free_group_inv [unfold 3] : FG X → FG X :=
|
||||||
|
quotient_unary_map (reverse ∘ map sum.flip)
|
||||||
|
(λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip))
|
||||||
|
definition free_group_mul [unfold 3 4] : FG X → FG X → FG X :=
|
||||||
|
quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s))))
|
||||||
|
|
||||||
|
section
|
||||||
|
local notation 1 := free_group_one
|
||||||
|
local postfix ⁻¹ := free_group_inv
|
||||||
|
local infix * := free_group_mul
|
||||||
|
|
||||||
|
theorem free_group_mul_assoc (g₁ g₂ g₃ : FG X) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g₁,
|
||||||
|
refine set_quotient.rec_prop _ g₂,
|
||||||
|
refine set_quotient.rec_prop _ g₃,
|
||||||
|
clear g₁ g₂ g₃, intro g₁ g₂ g₃,
|
||||||
|
exact ap class_of !append.assoc
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem free_group_one_mul (g : FG X) : 1 * g = g :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g, clear g, intro g,
|
||||||
|
exact ap class_of !append_nil_left
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem free_group_mul_one (g : FG X) : g * 1 = g :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g, clear g, intro g,
|
||||||
|
exact ap class_of !append_nil_right
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem free_group_mul_left_inv (g : FG X) : g⁻¹ * g = 1 :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g, clear g, intro g,
|
||||||
|
apply eq_of_rel, apply tr,
|
||||||
|
induction g with s l IH,
|
||||||
|
{ reflexivity},
|
||||||
|
{ rewrite [▸*, map_cons, reverse_cons, concat_append],
|
||||||
|
refine rtrans _ IH,
|
||||||
|
apply resp_append, reflexivity,
|
||||||
|
change R X ([flip s, s] ++ l) ([] ++ l),
|
||||||
|
apply resp_append,
|
||||||
|
induction s, apply cancel2, apply cancel1,
|
||||||
|
reflexivity}
|
||||||
|
end
|
||||||
|
|
||||||
|
end
|
||||||
|
end free_group open free_group
|
||||||
|
-- export [reduce_hints] free_group
|
||||||
|
variables (X)
|
||||||
|
definition group_free_group [constructor] : group (free_group_carrier X) :=
|
||||||
|
group.mk free_group_mul _ free_group_mul_assoc free_group_one free_group_one_mul free_group_mul_one
|
||||||
|
free_group_inv free_group_mul_left_inv
|
||||||
|
|
||||||
|
definition free_group [constructor] : Group :=
|
||||||
|
Group.mk _ (group_free_group X)
|
||||||
|
|
||||||
|
/- The universal property of the free group -/
|
||||||
|
variables {X G}
|
||||||
|
definition free_group_inclusion [constructor] (x : X) : free_group X :=
|
||||||
|
class_of [inl x]
|
||||||
|
|
||||||
|
definition fgh_helper [unfold 5] (f : X → G) (g : G) (x : X + X) : G :=
|
||||||
|
g * sum.rec (λx, f x) (λx, (f x)⁻¹) x
|
||||||
|
|
||||||
|
theorem fgh_helper_respect_rel (f : X → G) (r : free_group_rel X l l')
|
||||||
|
: Π(g : G), foldl (fgh_helper f) g l = foldl (fgh_helper f) g l' :=
|
||||||
|
begin
|
||||||
|
induction r with l x x l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂: intro g,
|
||||||
|
{ reflexivity},
|
||||||
|
{ unfold [foldl], apply mul_inv_cancel_right},
|
||||||
|
{ unfold [foldl], apply inv_mul_cancel_right},
|
||||||
|
{ rewrite [+foldl_append, IH₁, IH₂]},
|
||||||
|
{ exact !IH₁ ⬝ !IH₂}
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem fgh_helper_mul (f : X → G) (l)
|
||||||
|
: Π(g : G), foldl (fgh_helper f) g l = g * foldl (fgh_helper f) 1 l :=
|
||||||
|
begin
|
||||||
|
induction l with s l IH: intro g,
|
||||||
|
{ unfold [foldl], exact !mul_one⁻¹},
|
||||||
|
{ rewrite [+foldl_cons, IH], refine _ ⬝ (ap (λx, g * x) !IH⁻¹),
|
||||||
|
rewrite [-mul.assoc, ↑fgh_helper, one_mul]}
|
||||||
|
end
|
||||||
|
|
||||||
|
definition free_group_hom [constructor] (f : X → G) : free_group X →g G :=
|
||||||
|
begin
|
||||||
|
fapply homomorphism.mk,
|
||||||
|
{ intro g, refine set_quotient.elim _ _ g,
|
||||||
|
{ intro l, exact foldl (fgh_helper f) 1 l},
|
||||||
|
{ intro l l' r, esimp at *, refine trunc.rec _ r, clear r, intro r,
|
||||||
|
exact fgh_helper_respect_rel f r 1}},
|
||||||
|
{ refine set_quotient.rec_prop _, intro l, refine set_quotient.rec_prop _, intro l',
|
||||||
|
esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul}
|
||||||
|
end
|
||||||
|
|
||||||
|
definition fn_of_free_group_hom [unfold_full] (φ : free_group X →g G) : X → G :=
|
||||||
|
φ ∘ free_group_inclusion
|
||||||
|
|
||||||
|
variables (X G)
|
||||||
|
definition free_group_hom_equiv_fn : (free_group X →g G) ≃ (X → G) :=
|
||||||
|
begin
|
||||||
|
fapply equiv.MK,
|
||||||
|
{ exact fn_of_free_group_hom},
|
||||||
|
{ exact free_group_hom},
|
||||||
|
{ intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul},
|
||||||
|
{ intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp,
|
||||||
|
induction l with s l IH,
|
||||||
|
{ esimp [foldl], exact (respect_one φ)⁻¹},
|
||||||
|
{ rewrite [foldl_cons, fgh_helper_mul],
|
||||||
|
refine _ ⬝ (respect_mul φ (class_of [s]) (class_of l))⁻¹,
|
||||||
|
rewrite [IH], induction s: rewrite [▸*, one_mul], rewrite [-respect_inv φ]}}
|
||||||
|
end
|
||||||
|
|
||||||
|
end group
|
||||||
|
|
@ -6,644 +6,16 @@ Authors: Floris van Doorn, Egbert Rijke
|
||||||
Constructions with groups
|
Constructions with groups
|
||||||
-/
|
-/
|
||||||
|
|
||||||
import algebra.group_theory hit.set_quotient types.list types.sum .subgroup
|
import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group .product_group .free_group .free_commutative_group .direct_sum
|
||||||
|
|
||||||
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
|
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
|
||||||
equiv
|
equiv
|
||||||
namespace group
|
namespace group
|
||||||
|
|
||||||
definition aut.{u} (G : Group.{u}) : Group.{u} :=
|
|
||||||
begin
|
|
||||||
fapply Group.mk,
|
|
||||||
exact (G ≃g G),
|
|
||||||
fapply group.mk,
|
|
||||||
{ intros e f, fapply isomorphism.mk, exact f ∘g e, exact is_equiv.is_equiv_compose f e},
|
|
||||||
{ /-is_set G ≃g G-/ exact sorry},
|
|
||||||
{ /-associativity-/ intros e f g, exact sorry},
|
|
||||||
{ /-identity-/ fapply isomorphism.mk, exact sorry, exact sorry},
|
|
||||||
{ /-identity is left unit-/ exact sorry},
|
|
||||||
{ /-identity is right unit-/ exact sorry},
|
|
||||||
{ /-inverses-/ exact sorry},
|
|
||||||
{ /-inverse is right inverse?-/ exact sorry},
|
|
||||||
end
|
|
||||||
|
|
||||||
-- definition inner_aut (G : Group) : G →g (G ≃g G) := sorry /-- h ↦ h * g * h⁻¹ --/
|
|
||||||
|
|
||||||
|
|
||||||
variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
|
variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
|
||||||
{A B : CommGroup}
|
{A B : CommGroup}
|
||||||
|
|
||||||
/- Quotient Group -/
|
|
||||||
|
|
||||||
definition quotient_rel (g h : G) : Prop := N (g * h⁻¹)
|
|
||||||
|
|
||||||
variable {N}
|
|
||||||
|
|
||||||
-- We prove that quotient_rel is an equivalence relation
|
|
||||||
theorem quotient_rel_refl (g : G) : quotient_rel N g g :=
|
|
||||||
transport (λx, N x) !mul.right_inv⁻¹ (subgroup_has_one N)
|
|
||||||
|
|
||||||
theorem quotient_rel_symm (r : quotient_rel N g h) : quotient_rel N h g :=
|
|
||||||
transport (λx, N x) (!mul_inv ⬝ ap (λx, x * _) !inv_inv) (subgroup_respect_inv N r)
|
|
||||||
|
|
||||||
theorem quotient_rel_trans (r : quotient_rel N g h) (s : quotient_rel N h k)
|
|
||||||
: quotient_rel N g k :=
|
|
||||||
have H1 : N ((g * h⁻¹) * (h * k⁻¹)), from subgroup_respect_mul N r s,
|
|
||||||
have H2 : (g * h⁻¹) * (h * k⁻¹) = g * k⁻¹, from calc
|
|
||||||
(g * h⁻¹) * (h * k⁻¹) = ((g * h⁻¹) * h) * k⁻¹ : by rewrite [mul.assoc (g * h⁻¹)]
|
|
||||||
... = g * k⁻¹ : by rewrite inv_mul_cancel_right,
|
|
||||||
show N (g * k⁻¹), from H2 ▸ H1
|
|
||||||
|
|
||||||
theorem is_equivalence_quotient_rel : is_equivalence (quotient_rel N) :=
|
|
||||||
is_equivalence.mk quotient_rel_refl
|
|
||||||
(λg h, quotient_rel_symm)
|
|
||||||
(λg h k, quotient_rel_trans)
|
|
||||||
|
|
||||||
-- We prove that quotient_rel respects inverses and multiplication, so
|
|
||||||
-- it is a congruence relation
|
|
||||||
theorem quotient_rel_resp_inv (r : quotient_rel N g h) : quotient_rel N g⁻¹ h⁻¹ :=
|
|
||||||
have H1 : N (g⁻¹ * (h * g⁻¹) * g), from
|
|
||||||
is_normal_subgroup' N g (quotient_rel_symm r),
|
|
||||||
have H2 : g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h⁻¹⁻¹, from calc
|
|
||||||
g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h * g⁻¹ * g : by rewrite -mul.assoc
|
|
||||||
... = g⁻¹ * h : inv_mul_cancel_right
|
|
||||||
... = g⁻¹ * h⁻¹⁻¹ : by rewrite algebra.inv_inv,
|
|
||||||
show N (g⁻¹ * h⁻¹⁻¹), from H2 ▸ H1
|
|
||||||
|
|
||||||
theorem quotient_rel_resp_mul (r : quotient_rel N g h) (r' : quotient_rel N g' h')
|
|
||||||
: quotient_rel N (g * g') (h * h') :=
|
|
||||||
have H1 : N (g * ((g' * h'⁻¹) * h⁻¹)), from
|
|
||||||
normal_subgroup_insert N r' r,
|
|
||||||
have H2 : g * ((g' * h'⁻¹) * h⁻¹) = (g * g') * (h * h')⁻¹, from calc
|
|
||||||
g * ((g' * h'⁻¹) * h⁻¹) = g * (g' * (h'⁻¹ * h⁻¹)) : by rewrite [mul.assoc]
|
|
||||||
... = (g * g') * (h'⁻¹ * h⁻¹) : mul.assoc
|
|
||||||
... = (g * g') * (h * h')⁻¹ : by rewrite [mul_inv],
|
|
||||||
show N ((g * g') * (h * h')⁻¹), from transport (λx, N x) H2 H1
|
|
||||||
|
|
||||||
local attribute is_equivalence_quotient_rel [instance]
|
|
||||||
|
|
||||||
variable (N)
|
|
||||||
|
|
||||||
definition qg : Type := set_quotient (quotient_rel N)
|
|
||||||
|
|
||||||
variable {N}
|
|
||||||
|
|
||||||
local attribute qg [reducible]
|
|
||||||
|
|
||||||
definition quotient_one [constructor] : qg N := class_of one
|
|
||||||
definition quotient_inv [unfold 3] : qg N → qg N :=
|
|
||||||
quotient_unary_map has_inv.inv (λg g' r, quotient_rel_resp_inv r)
|
|
||||||
definition quotient_mul [unfold 3 4] : qg N → qg N → qg N :=
|
|
||||||
quotient_binary_map has_mul.mul (λg g' r h h' r', quotient_rel_resp_mul r r')
|
|
||||||
|
|
||||||
section
|
|
||||||
local notation 1 := quotient_one
|
|
||||||
local postfix ⁻¹ := quotient_inv
|
|
||||||
local infix * := quotient_mul
|
|
||||||
|
|
||||||
theorem quotient_mul_assoc (g₁ g₂ g₃ : qg N) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g₁,
|
|
||||||
refine set_quotient.rec_prop _ g₂,
|
|
||||||
refine set_quotient.rec_prop _ g₃,
|
|
||||||
clear g₁ g₂ g₃, intro g₁ g₂ g₃,
|
|
||||||
exact ap class_of !mul.assoc
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem quotient_one_mul (g : qg N) : 1 * g = g :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g, clear g, intro g,
|
|
||||||
exact ap class_of !one_mul
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem quotient_mul_one (g : qg N) : g * 1 = g :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g, clear g, intro g,
|
|
||||||
exact ap class_of !mul_one
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem quotient_mul_left_inv (g : qg N) : g⁻¹ * g = 1 :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g, clear g, intro g,
|
|
||||||
exact ap class_of !mul.left_inv
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem quotient_mul_comm {G : CommGroup} {N : normal_subgroup_rel G} (g h : qg N)
|
|
||||||
: g * h = h * g :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g, clear g, intro g,
|
|
||||||
refine set_quotient.rec_prop _ h, clear h, intro h,
|
|
||||||
apply ap class_of, esimp, apply mul.comm
|
|
||||||
end
|
|
||||||
|
|
||||||
end
|
|
||||||
|
|
||||||
variable (N)
|
|
||||||
definition group_qg [constructor] : group (qg N) :=
|
|
||||||
group.mk quotient_mul _ quotient_mul_assoc quotient_one quotient_one_mul quotient_mul_one
|
|
||||||
quotient_inv quotient_mul_left_inv
|
|
||||||
|
|
||||||
definition quotient_group [constructor] : Group :=
|
|
||||||
Group.mk _ (group_qg N)
|
|
||||||
|
|
||||||
definition comm_group_qg [constructor] {G : CommGroup} (N : normal_subgroup_rel G)
|
|
||||||
: comm_group (qg N) :=
|
|
||||||
⦃comm_group, group_qg N, mul_comm := quotient_mul_comm⦄
|
|
||||||
|
|
||||||
definition quotient_comm_group [constructor] {G : CommGroup} (N : subgroup_rel G)
|
|
||||||
: CommGroup :=
|
|
||||||
CommGroup.mk _ (comm_group_qg (normal_subgroup_rel_comm N))
|
|
||||||
|
|
||||||
definition gq_map : G →g quotient_group N :=
|
|
||||||
homomorphism.mk class_of (λ g h, idp)
|
|
||||||
|
|
||||||
namespace quotient
|
|
||||||
notation `⟦`:max a `⟧`:0 := gq_map a _
|
|
||||||
end quotient
|
|
||||||
|
|
||||||
open quotient
|
|
||||||
variable {N}
|
|
||||||
|
|
||||||
definition gq_map_eq_one (g : G) (H : N g) : gq_map N g = 1 :=
|
|
||||||
begin
|
|
||||||
apply eq_of_rel,
|
|
||||||
have e : (g * 1⁻¹ = g),
|
|
||||||
from calc
|
|
||||||
g * 1⁻¹ = g * 1 : one_inv
|
|
||||||
... = g : mul_one,
|
|
||||||
unfold quotient_rel, rewrite e, exact H
|
|
||||||
end
|
|
||||||
|
|
||||||
definition rel_of_gq_map_eq_one (g : G) (H : gq_map N g = 1) : N g :=
|
|
||||||
begin
|
|
||||||
have e : (g * 1⁻¹ = g),
|
|
||||||
from calc
|
|
||||||
g * 1⁻¹ = g * 1 : one_inv
|
|
||||||
... = g : mul_one,
|
|
||||||
rewrite (inverse e),
|
|
||||||
apply rel_of_eq _ H
|
|
||||||
end
|
|
||||||
|
|
||||||
definition quotient_group_elim (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' :=
|
|
||||||
begin
|
|
||||||
fapply homomorphism.mk,
|
|
||||||
-- define function
|
|
||||||
{ apply set_quotient.elim f,
|
|
||||||
intro g h K,
|
|
||||||
apply eq_of_mul_inv_eq_one,
|
|
||||||
have e : f (g * h⁻¹) = f g * (f h)⁻¹,
|
|
||||||
from calc
|
|
||||||
f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul
|
|
||||||
... = f g * (f h)⁻¹ : to_respect_inv,
|
|
||||||
rewrite (inverse e),
|
|
||||||
apply H, exact K},
|
|
||||||
{ intro g h, induction g using set_quotient.rec_prop with g,
|
|
||||||
induction h using set_quotient.rec_prop with h,
|
|
||||||
krewrite (inverse (to_respect_mul (gq_map N) g h)),
|
|
||||||
unfold gq_map, esimp, exact to_respect_mul f g h }
|
|
||||||
end
|
|
||||||
|
|
||||||
definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group_elim f H ∘g gq_map N ~ f :=
|
|
||||||
begin
|
|
||||||
intro g, reflexivity
|
|
||||||
end
|
|
||||||
|
|
||||||
definition glift_unique (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (k : quotient_group N →g G')
|
|
||||||
: ( k ∘g gq_map N ~ f ) → k ~ quotient_group_elim f H :=
|
|
||||||
begin
|
|
||||||
intro K cg, induction cg using set_quotient.rec_prop with g,
|
|
||||||
krewrite (quotient_group_compute f),
|
|
||||||
exact K g
|
|
||||||
end
|
|
||||||
|
|
||||||
definition gq_universal_property (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) :
|
|
||||||
is_contr (Σ(g : quotient_group N →g G'), g ∘g gq_map N = f) :=
|
|
||||||
sorry
|
|
||||||
|
|
||||||
/- Binary products (direct product) of Groups -/
|
|
||||||
definition product_one [constructor] : G × G' := (one, one)
|
|
||||||
definition product_inv [unfold 3] : G × G' → G × G' :=
|
|
||||||
λv, (v.1⁻¹, v.2⁻¹)
|
|
||||||
definition product_mul [unfold 3 4] : G × G' → G × G' → G × G' :=
|
|
||||||
λv w, (v.1 * w.1, v.2 * w.2)
|
|
||||||
|
|
||||||
section
|
|
||||||
local notation 1 := product_one
|
|
||||||
local postfix ⁻¹ := product_inv
|
|
||||||
local infix * := product_mul
|
|
||||||
|
|
||||||
theorem product_mul_assoc (g₁ g₂ g₃ : G × G') : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
|
|
||||||
prod_eq !mul.assoc !mul.assoc
|
|
||||||
|
|
||||||
theorem product_one_mul (g : G × G') : 1 * g = g :=
|
|
||||||
prod_eq !one_mul !one_mul
|
|
||||||
|
|
||||||
theorem product_mul_one (g : G × G') : g * 1 = g :=
|
|
||||||
prod_eq !mul_one !mul_one
|
|
||||||
|
|
||||||
theorem product_mul_left_inv (g : G × G') : g⁻¹ * g = 1 :=
|
|
||||||
prod_eq !mul.left_inv !mul.left_inv
|
|
||||||
|
|
||||||
theorem product_mul_comm {G G' : CommGroup} (g h : G × G') : g * h = h * g :=
|
|
||||||
prod_eq !mul.comm !mul.comm
|
|
||||||
|
|
||||||
end
|
|
||||||
|
|
||||||
variables (G G')
|
|
||||||
definition group_prod [constructor] : group (G × G') :=
|
|
||||||
group.mk product_mul _ product_mul_assoc product_one product_one_mul product_mul_one
|
|
||||||
product_inv product_mul_left_inv
|
|
||||||
|
|
||||||
definition product [constructor] : Group :=
|
|
||||||
Group.mk _ (group_prod G G')
|
|
||||||
|
|
||||||
definition comm_group_prod [constructor] (G G' : CommGroup) : comm_group (G × G') :=
|
|
||||||
⦃comm_group, group_prod G G', mul_comm := product_mul_comm⦄
|
|
||||||
|
|
||||||
definition comm_product [constructor] (G G' : CommGroup) : CommGroup :=
|
|
||||||
CommGroup.mk _ (comm_group_prod G G')
|
|
||||||
|
|
||||||
infix ` ×g `:30 := group.product
|
|
||||||
|
|
||||||
/- Free Group of a set -/
|
|
||||||
variables (X : Set) {l l' : list (X ⊎ X)}
|
variables (X : Set) {l l' : list (X ⊎ X)}
|
||||||
namespace free_group
|
|
||||||
|
|
||||||
inductive free_group_rel : list (X ⊎ X) → list (X ⊎ X) → Type :=
|
|
||||||
| rrefl : Πl, free_group_rel l l
|
|
||||||
| cancel1 : Πx, free_group_rel [inl x, inr x] []
|
|
||||||
| cancel2 : Πx, free_group_rel [inr x, inl x] []
|
|
||||||
| resp_append : Π{l₁ l₂ l₃ l₄}, free_group_rel l₁ l₂ → free_group_rel l₃ l₄ →
|
|
||||||
free_group_rel (l₁ ++ l₃) (l₂ ++ l₄)
|
|
||||||
| rtrans : Π{l₁ l₂ l₃}, free_group_rel l₁ l₂ → free_group_rel l₂ l₃ →
|
|
||||||
free_group_rel l₁ l₃
|
|
||||||
|
|
||||||
open free_group_rel
|
|
||||||
local abbreviation R [reducible] := free_group_rel
|
|
||||||
attribute free_group_rel.rrefl [refl]
|
|
||||||
|
|
||||||
definition free_group_carrier [reducible] : Type := set_quotient (λx y, ∥R X x y∥)
|
|
||||||
local abbreviation FG := free_group_carrier
|
|
||||||
|
|
||||||
definition is_reflexive_R : is_reflexive (λx y, ∥R X x y∥) :=
|
|
||||||
begin constructor, intro s, apply tr, unfold R end
|
|
||||||
local attribute is_reflexive_R [instance]
|
|
||||||
|
|
||||||
variable {X}
|
|
||||||
theorem rel_respect_flip (r : R X l l') : R X (map sum.flip l) (map sum.flip l') :=
|
|
||||||
begin
|
|
||||||
induction r with l x x l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂,
|
|
||||||
{ reflexivity},
|
|
||||||
{ repeat esimp [map], exact cancel2 x},
|
|
||||||
{ repeat esimp [map], exact cancel1 x},
|
|
||||||
{ rewrite [+map_append], exact resp_append IH₁ IH₂},
|
|
||||||
{ exact rtrans IH₁ IH₂}
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem rel_respect_reverse (r : R X l l') : R X (reverse l) (reverse l') :=
|
|
||||||
begin
|
|
||||||
induction r with l x x l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂,
|
|
||||||
{ reflexivity},
|
|
||||||
{ repeat esimp [map], exact cancel2 x},
|
|
||||||
{ repeat esimp [map], exact cancel1 x},
|
|
||||||
{ rewrite [+reverse_append], exact resp_append IH₂ IH₁},
|
|
||||||
{ exact rtrans IH₁ IH₂}
|
|
||||||
end
|
|
||||||
|
|
||||||
definition free_group_one [constructor] : FG X := class_of []
|
|
||||||
definition free_group_inv [unfold 3] : FG X → FG X :=
|
|
||||||
quotient_unary_map (reverse ∘ map sum.flip)
|
|
||||||
(λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip))
|
|
||||||
definition free_group_mul [unfold 3 4] : FG X → FG X → FG X :=
|
|
||||||
quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s))))
|
|
||||||
|
|
||||||
section
|
|
||||||
local notation 1 := free_group_one
|
|
||||||
local postfix ⁻¹ := free_group_inv
|
|
||||||
local infix * := free_group_mul
|
|
||||||
|
|
||||||
theorem free_group_mul_assoc (g₁ g₂ g₃ : FG X) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g₁,
|
|
||||||
refine set_quotient.rec_prop _ g₂,
|
|
||||||
refine set_quotient.rec_prop _ g₃,
|
|
||||||
clear g₁ g₂ g₃, intro g₁ g₂ g₃,
|
|
||||||
exact ap class_of !append.assoc
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem free_group_one_mul (g : FG X) : 1 * g = g :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g, clear g, intro g,
|
|
||||||
exact ap class_of !append_nil_left
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem free_group_mul_one (g : FG X) : g * 1 = g :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g, clear g, intro g,
|
|
||||||
exact ap class_of !append_nil_right
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem free_group_mul_left_inv (g : FG X) : g⁻¹ * g = 1 :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g, clear g, intro g,
|
|
||||||
apply eq_of_rel, apply tr,
|
|
||||||
induction g with s l IH,
|
|
||||||
{ reflexivity},
|
|
||||||
{ rewrite [▸*, map_cons, reverse_cons, concat_append],
|
|
||||||
refine rtrans _ IH,
|
|
||||||
apply resp_append, reflexivity,
|
|
||||||
change R X ([flip s, s] ++ l) ([] ++ l),
|
|
||||||
apply resp_append,
|
|
||||||
induction s, apply cancel2, apply cancel1,
|
|
||||||
reflexivity}
|
|
||||||
end
|
|
||||||
|
|
||||||
end
|
|
||||||
end free_group open free_group
|
|
||||||
-- export [reduce_hints] free_group
|
|
||||||
variables (X)
|
|
||||||
definition group_free_group [constructor] : group (free_group_carrier X) :=
|
|
||||||
group.mk free_group_mul _ free_group_mul_assoc free_group_one free_group_one_mul free_group_mul_one
|
|
||||||
free_group_inv free_group_mul_left_inv
|
|
||||||
|
|
||||||
definition free_group [constructor] : Group :=
|
|
||||||
Group.mk _ (group_free_group X)
|
|
||||||
|
|
||||||
/- The universal property of the free group -/
|
|
||||||
variables {X G}
|
|
||||||
definition free_group_inclusion [constructor] (x : X) : free_group X :=
|
|
||||||
class_of [inl x]
|
|
||||||
|
|
||||||
definition fgh_helper [unfold 5] (f : X → G) (g : G) (x : X + X) : G :=
|
|
||||||
g * sum.rec (λx, f x) (λx, (f x)⁻¹) x
|
|
||||||
|
|
||||||
theorem fgh_helper_respect_rel (f : X → G) (r : free_group_rel X l l')
|
|
||||||
: Π(g : G), foldl (fgh_helper f) g l = foldl (fgh_helper f) g l' :=
|
|
||||||
begin
|
|
||||||
induction r with l x x l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂: intro g,
|
|
||||||
{ reflexivity},
|
|
||||||
{ unfold [foldl], apply mul_inv_cancel_right},
|
|
||||||
{ unfold [foldl], apply inv_mul_cancel_right},
|
|
||||||
{ rewrite [+foldl_append, IH₁, IH₂]},
|
|
||||||
{ exact !IH₁ ⬝ !IH₂}
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem fgh_helper_mul (f : X → G) (l)
|
|
||||||
: Π(g : G), foldl (fgh_helper f) g l = g * foldl (fgh_helper f) 1 l :=
|
|
||||||
begin
|
|
||||||
induction l with s l IH: intro g,
|
|
||||||
{ unfold [foldl], exact !mul_one⁻¹},
|
|
||||||
{ rewrite [+foldl_cons, IH], refine _ ⬝ (ap (λx, g * x) !IH⁻¹),
|
|
||||||
rewrite [-mul.assoc, ↑fgh_helper, one_mul]}
|
|
||||||
end
|
|
||||||
|
|
||||||
definition free_group_hom [constructor] (f : X → G) : free_group X →g G :=
|
|
||||||
begin
|
|
||||||
fapply homomorphism.mk,
|
|
||||||
{ intro g, refine set_quotient.elim _ _ g,
|
|
||||||
{ intro l, exact foldl (fgh_helper f) 1 l},
|
|
||||||
{ intro l l' r, esimp at *, refine trunc.rec _ r, clear r, intro r,
|
|
||||||
exact fgh_helper_respect_rel f r 1}},
|
|
||||||
{ refine set_quotient.rec_prop _, intro l, refine set_quotient.rec_prop _, intro l',
|
|
||||||
esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul}
|
|
||||||
end
|
|
||||||
|
|
||||||
definition fn_of_free_group_hom [unfold_full] (φ : free_group X →g G) : X → G :=
|
|
||||||
φ ∘ free_group_inclusion
|
|
||||||
|
|
||||||
variables (X G)
|
|
||||||
definition free_group_hom_equiv_fn : (free_group X →g G) ≃ (X → G) :=
|
|
||||||
begin
|
|
||||||
fapply equiv.MK,
|
|
||||||
{ exact fn_of_free_group_hom},
|
|
||||||
{ exact free_group_hom},
|
|
||||||
{ intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul},
|
|
||||||
{ intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp,
|
|
||||||
induction l with s l IH,
|
|
||||||
{ esimp [foldl], exact (respect_one φ)⁻¹},
|
|
||||||
{ rewrite [foldl_cons, fgh_helper_mul],
|
|
||||||
refine _ ⬝ (respect_mul φ (class_of [s]) (class_of l))⁻¹,
|
|
||||||
rewrite [IH], induction s: rewrite [▸*, one_mul], rewrite [-respect_inv φ]}}
|
|
||||||
end
|
|
||||||
|
|
||||||
/- Free Commutative Group of a set -/
|
|
||||||
namespace free_comm_group
|
|
||||||
|
|
||||||
inductive fcg_rel : list (X ⊎ X) → list (X ⊎ X) → Type :=
|
|
||||||
| rrefl : Πl, fcg_rel l l
|
|
||||||
| cancel1 : Πx, fcg_rel [inl x, inr x] []
|
|
||||||
| cancel2 : Πx, fcg_rel [inr x, inl x] []
|
|
||||||
| rflip : Πx y, fcg_rel [x, y] [y, x]
|
|
||||||
| resp_append : Π{l₁ l₂ l₃ l₄}, fcg_rel l₁ l₂ → fcg_rel l₃ l₄ →
|
|
||||||
fcg_rel (l₁ ++ l₃) (l₂ ++ l₄)
|
|
||||||
| rtrans : Π{l₁ l₂ l₃}, fcg_rel l₁ l₂ → fcg_rel l₂ l₃ →
|
|
||||||
fcg_rel l₁ l₃
|
|
||||||
|
|
||||||
open fcg_rel
|
|
||||||
local abbreviation R [reducible] := fcg_rel
|
|
||||||
attribute fcg_rel.rrefl [refl]
|
|
||||||
attribute fcg_rel.rtrans [trans]
|
|
||||||
|
|
||||||
definition fcg_carrier [reducible] : Type := set_quotient (λx y, ∥R X x y∥)
|
|
||||||
local abbreviation FG := fcg_carrier
|
|
||||||
|
|
||||||
definition is_reflexive_R : is_reflexive (λx y, ∥R X x y∥) :=
|
|
||||||
begin constructor, intro s, apply tr, unfold R end
|
|
||||||
local attribute is_reflexive_R [instance]
|
|
||||||
|
|
||||||
variable {X}
|
|
||||||
theorem rel_respect_flip (r : R X l l') : R X (map sum.flip l) (map sum.flip l') :=
|
|
||||||
begin
|
|
||||||
induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂,
|
|
||||||
{ reflexivity},
|
|
||||||
{ repeat esimp [map], exact cancel2 x},
|
|
||||||
{ repeat esimp [map], exact cancel1 x},
|
|
||||||
{ repeat esimp [map], apply rflip},
|
|
||||||
{ rewrite [+map_append], exact resp_append IH₁ IH₂},
|
|
||||||
{ exact rtrans IH₁ IH₂}
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem rel_respect_reverse (r : R X l l') : R X (reverse l) (reverse l') :=
|
|
||||||
begin
|
|
||||||
induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂,
|
|
||||||
{ reflexivity},
|
|
||||||
{ repeat esimp [map], exact cancel2 x},
|
|
||||||
{ repeat esimp [map], exact cancel1 x},
|
|
||||||
{ repeat esimp [map], apply rflip},
|
|
||||||
{ rewrite [+reverse_append], exact resp_append IH₂ IH₁},
|
|
||||||
{ exact rtrans IH₁ IH₂}
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem rel_cons_concat (l s) : R X (s :: l) (concat s l) :=
|
|
||||||
begin
|
|
||||||
induction l with t l IH,
|
|
||||||
{ reflexivity},
|
|
||||||
{ rewrite [concat_cons], transitivity (t :: s :: l),
|
|
||||||
{ exact resp_append !rflip !rrefl},
|
|
||||||
{ exact resp_append (rrefl [t]) IH}}
|
|
||||||
end
|
|
||||||
|
|
||||||
definition fcg_one [constructor] : FG X := class_of []
|
|
||||||
definition fcg_inv [unfold 3] : FG X → FG X :=
|
|
||||||
quotient_unary_map (reverse ∘ map sum.flip)
|
|
||||||
(λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip))
|
|
||||||
definition fcg_mul [unfold 3 4] : FG X → FG X → FG X :=
|
|
||||||
quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s))))
|
|
||||||
|
|
||||||
section
|
|
||||||
local notation 1 := fcg_one
|
|
||||||
local postfix ⁻¹ := fcg_inv
|
|
||||||
local infix * := fcg_mul
|
|
||||||
|
|
||||||
theorem fcg_mul_assoc (g₁ g₂ g₃ : FG X) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g₁,
|
|
||||||
refine set_quotient.rec_prop _ g₂,
|
|
||||||
refine set_quotient.rec_prop _ g₃,
|
|
||||||
clear g₁ g₂ g₃, intro g₁ g₂ g₃,
|
|
||||||
exact ap class_of !append.assoc
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem fcg_one_mul (g : FG X) : 1 * g = g :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g, clear g, intro g,
|
|
||||||
exact ap class_of !append_nil_left
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem fcg_mul_one (g : FG X) : g * 1 = g :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g, clear g, intro g,
|
|
||||||
exact ap class_of !append_nil_right
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem fcg_mul_left_inv (g : FG X) : g⁻¹ * g = 1 :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g, clear g, intro g,
|
|
||||||
apply eq_of_rel, apply tr,
|
|
||||||
induction g with s l IH,
|
|
||||||
{ reflexivity},
|
|
||||||
{ rewrite [▸*, map_cons, reverse_cons, concat_append],
|
|
||||||
refine rtrans _ IH,
|
|
||||||
apply resp_append, reflexivity,
|
|
||||||
change R X ([flip s, s] ++ l) ([] ++ l),
|
|
||||||
apply resp_append,
|
|
||||||
induction s, apply cancel2, apply cancel1,
|
|
||||||
reflexivity}
|
|
||||||
end
|
|
||||||
|
|
||||||
theorem fcg_mul_comm (g h : FG X) : g * h = h * g :=
|
|
||||||
begin
|
|
||||||
refine set_quotient.rec_prop _ g, clear g, intro g,
|
|
||||||
refine set_quotient.rec_prop _ h, clear h, intro h,
|
|
||||||
apply eq_of_rel, apply tr,
|
|
||||||
revert h, induction g with s l IH: intro h,
|
|
||||||
{ rewrite [append_nil_left, append_nil_right]},
|
|
||||||
{ rewrite [append_cons,-concat_append],
|
|
||||||
transitivity concat s (l ++ h), apply rel_cons_concat,
|
|
||||||
rewrite [-append_concat], apply IH}
|
|
||||||
end
|
|
||||||
end
|
|
||||||
end free_comm_group open free_comm_group
|
|
||||||
|
|
||||||
variables (X)
|
|
||||||
definition group_free_comm_group [constructor] : comm_group (fcg_carrier X) :=
|
|
||||||
comm_group.mk fcg_mul _ fcg_mul_assoc fcg_one fcg_one_mul fcg_mul_one
|
|
||||||
fcg_inv fcg_mul_left_inv fcg_mul_comm
|
|
||||||
|
|
||||||
definition free_comm_group [constructor] : CommGroup :=
|
|
||||||
CommGroup.mk _ (group_free_comm_group X)
|
|
||||||
|
|
||||||
/- The universal property of the free commutative group -/
|
|
||||||
variables {X A}
|
|
||||||
definition free_comm_group_inclusion [constructor] (x : X) : free_comm_group X :=
|
|
||||||
class_of [inl x]
|
|
||||||
|
|
||||||
theorem fgh_helper_respect_comm_rel (f : X → A) (r : fcg_rel X l l')
|
|
||||||
: Π(g : A), foldl (fgh_helper f) g l = foldl (fgh_helper f) g l' :=
|
|
||||||
begin
|
|
||||||
induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂: intro g,
|
|
||||||
{ reflexivity},
|
|
||||||
{ unfold [foldl], apply mul_inv_cancel_right},
|
|
||||||
{ unfold [foldl], apply inv_mul_cancel_right},
|
|
||||||
{ unfold [foldl, fgh_helper], apply mul.right_comm},
|
|
||||||
{ rewrite [+foldl_append, IH₁, IH₂]},
|
|
||||||
{ exact !IH₁ ⬝ !IH₂}
|
|
||||||
end
|
|
||||||
|
|
||||||
definition free_comm_group_hom [constructor] (f : X → A) : free_comm_group X →g A :=
|
|
||||||
begin
|
|
||||||
fapply homomorphism.mk,
|
|
||||||
{ intro g, refine set_quotient.elim _ _ g,
|
|
||||||
{ intro l, exact foldl (fgh_helper f) 1 l},
|
|
||||||
{ intro l l' r, esimp at *, refine trunc.rec _ r, clear r, intro r,
|
|
||||||
exact fgh_helper_respect_comm_rel f r 1}},
|
|
||||||
{ refine set_quotient.rec_prop _, intro l, refine set_quotient.rec_prop _, intro l',
|
|
||||||
esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul}
|
|
||||||
end
|
|
||||||
|
|
||||||
definition fn_of_free_comm_group_hom [unfold_full] (φ : free_comm_group X →g A) : X → A :=
|
|
||||||
φ ∘ free_comm_group_inclusion
|
|
||||||
|
|
||||||
variables (X A)
|
|
||||||
definition free_comm_group_hom_equiv_fn : (free_comm_group X →g A) ≃ (X → A) :=
|
|
||||||
begin
|
|
||||||
fapply equiv.MK,
|
|
||||||
{ exact fn_of_free_comm_group_hom},
|
|
||||||
{ exact free_comm_group_hom},
|
|
||||||
{ intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul},
|
|
||||||
{ intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp,
|
|
||||||
induction l with s l IH,
|
|
||||||
{ esimp [foldl], symmetry, exact to_respect_one φ},
|
|
||||||
{ rewrite [foldl_cons, fgh_helper_mul],
|
|
||||||
refine _ ⬝ (to_respect_mul φ (class_of [s]) (class_of l))⁻¹,
|
|
||||||
rewrite [▸*,IH], induction s: rewrite [▸*, one_mul], apply ap (λx, x * _),
|
|
||||||
exact !to_respect_inv⁻¹}}
|
|
||||||
end
|
|
||||||
|
|
||||||
/- set generating normal subgroup -/
|
|
||||||
|
|
||||||
section
|
|
||||||
|
|
||||||
parameters {GG : CommGroup} (S : GG → Prop)
|
|
||||||
|
|
||||||
inductive generating_relation' : GG → Type :=
|
|
||||||
| rincl : Π{g}, S g → generating_relation' g
|
|
||||||
| rmul : Π{g h}, generating_relation' g → generating_relation' h → generating_relation' (g * h)
|
|
||||||
| rinv : Π{g}, generating_relation' g → generating_relation' g⁻¹
|
|
||||||
| rone : generating_relation' 1
|
|
||||||
open generating_relation'
|
|
||||||
definition generating_relation (g : GG) : Prop := ∥ generating_relation' g ∥
|
|
||||||
local abbreviation R := generating_relation
|
|
||||||
definition gr_one : R 1 := tr (rone S)
|
|
||||||
definition gr_inv (g : GG) : R g → R g⁻¹ :=
|
|
||||||
trunc_functor -1 rinv
|
|
||||||
definition gr_mul (g h : GG) : R g → R h → R (g * h) :=
|
|
||||||
trunc_functor2 rmul
|
|
||||||
|
|
||||||
definition normal_generating_relation : subgroup_rel GG :=
|
|
||||||
⦃ subgroup_rel,
|
|
||||||
R := generating_relation,
|
|
||||||
Rone := gr_one,
|
|
||||||
Rinv := gr_inv,
|
|
||||||
Rmul := gr_mul⦄
|
|
||||||
|
|
||||||
parameter (GG)
|
|
||||||
definition quotient_comm_group_gen : CommGroup := quotient_comm_group normal_generating_relation
|
|
||||||
|
|
||||||
end
|
|
||||||
|
|
||||||
section
|
|
||||||
|
|
||||||
parameters {I : Set} (Y : I → CommGroup)
|
|
||||||
|
|
||||||
definition dirsum_carrier : CommGroup := free_comm_group (trunctype.mk (Σi, Y i) _)
|
|
||||||
local abbreviation ι := @free_comm_group_inclusion
|
|
||||||
inductive dirsum_rel : dirsum_carrier → Type :=
|
|
||||||
| rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹)
|
|
||||||
|
|
||||||
definition direct_sum : CommGroup := quotient_comm_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
|
|
||||||
|
|
||||||
end
|
|
||||||
|
|
||||||
/- Tensor group (WIP) -/
|
/- Tensor group (WIP) -/
|
||||||
|
|
||||||
|
|
|
||||||
63
algebra/product_group.hlean
Normal file
63
algebra/product_group.hlean
Normal file
|
|
@ -0,0 +1,63 @@
|
||||||
|
/-
|
||||||
|
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||||
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
Authors: Floris van Doorn, Egbert Rijke
|
||||||
|
|
||||||
|
Constructions with groups
|
||||||
|
-/
|
||||||
|
|
||||||
|
import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group
|
||||||
|
|
||||||
|
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
|
||||||
|
equiv
|
||||||
|
namespace group
|
||||||
|
|
||||||
|
variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
|
||||||
|
{A B : CommGroup}
|
||||||
|
|
||||||
|
/- Binary products (direct product) of Groups -/
|
||||||
|
definition product_one [constructor] : G × G' := (one, one)
|
||||||
|
definition product_inv [unfold 3] : G × G' → G × G' :=
|
||||||
|
λv, (v.1⁻¹, v.2⁻¹)
|
||||||
|
definition product_mul [unfold 3 4] : G × G' → G × G' → G × G' :=
|
||||||
|
λv w, (v.1 * w.1, v.2 * w.2)
|
||||||
|
|
||||||
|
section
|
||||||
|
local notation 1 := product_one
|
||||||
|
local postfix ⁻¹ := product_inv
|
||||||
|
local infix * := product_mul
|
||||||
|
|
||||||
|
theorem product_mul_assoc (g₁ g₂ g₃ : G × G') : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
|
||||||
|
prod_eq !mul.assoc !mul.assoc
|
||||||
|
|
||||||
|
theorem product_one_mul (g : G × G') : 1 * g = g :=
|
||||||
|
prod_eq !one_mul !one_mul
|
||||||
|
|
||||||
|
theorem product_mul_one (g : G × G') : g * 1 = g :=
|
||||||
|
prod_eq !mul_one !mul_one
|
||||||
|
|
||||||
|
theorem product_mul_left_inv (g : G × G') : g⁻¹ * g = 1 :=
|
||||||
|
prod_eq !mul.left_inv !mul.left_inv
|
||||||
|
|
||||||
|
theorem product_mul_comm {G G' : CommGroup} (g h : G × G') : g * h = h * g :=
|
||||||
|
prod_eq !mul.comm !mul.comm
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
variables (G G')
|
||||||
|
definition group_prod [constructor] : group (G × G') :=
|
||||||
|
group.mk product_mul _ product_mul_assoc product_one product_one_mul product_mul_one
|
||||||
|
product_inv product_mul_left_inv
|
||||||
|
|
||||||
|
definition product [constructor] : Group :=
|
||||||
|
Group.mk _ (group_prod G G')
|
||||||
|
|
||||||
|
definition comm_group_prod [constructor] (G G' : CommGroup) : comm_group (G × G') :=
|
||||||
|
⦃comm_group, group_prod G G', mul_comm := product_mul_comm⦄
|
||||||
|
|
||||||
|
definition comm_product [constructor] (G G' : CommGroup) : CommGroup :=
|
||||||
|
CommGroup.mk _ (comm_group_prod G G')
|
||||||
|
|
||||||
|
infix ` ×g `:30 := group.product
|
||||||
|
|
||||||
|
end group
|
||||||
237
algebra/quotient_group.hlean
Normal file
237
algebra/quotient_group.hlean
Normal file
|
|
@ -0,0 +1,237 @@
|
||||||
|
/-
|
||||||
|
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||||
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
Authors: Floris van Doorn, Egbert Rijke
|
||||||
|
|
||||||
|
Constructions with groups
|
||||||
|
-/
|
||||||
|
|
||||||
|
import algebra.group_theory hit.set_quotient types.list types.sum .subgroup
|
||||||
|
|
||||||
|
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
|
||||||
|
equiv
|
||||||
|
namespace group
|
||||||
|
|
||||||
|
variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
|
||||||
|
{A B : CommGroup}
|
||||||
|
|
||||||
|
/- Quotient Group -/
|
||||||
|
|
||||||
|
definition quotient_rel (g h : G) : Prop := N (g * h⁻¹)
|
||||||
|
|
||||||
|
variable {N}
|
||||||
|
|
||||||
|
-- We prove that quotient_rel is an equivalence relation
|
||||||
|
theorem quotient_rel_refl (g : G) : quotient_rel N g g :=
|
||||||
|
transport (λx, N x) !mul.right_inv⁻¹ (subgroup_has_one N)
|
||||||
|
|
||||||
|
theorem quotient_rel_symm (r : quotient_rel N g h) : quotient_rel N h g :=
|
||||||
|
transport (λx, N x) (!mul_inv ⬝ ap (λx, x * _) !inv_inv) (subgroup_respect_inv N r)
|
||||||
|
|
||||||
|
theorem quotient_rel_trans (r : quotient_rel N g h) (s : quotient_rel N h k)
|
||||||
|
: quotient_rel N g k :=
|
||||||
|
have H1 : N ((g * h⁻¹) * (h * k⁻¹)), from subgroup_respect_mul N r s,
|
||||||
|
have H2 : (g * h⁻¹) * (h * k⁻¹) = g * k⁻¹, from calc
|
||||||
|
(g * h⁻¹) * (h * k⁻¹) = ((g * h⁻¹) * h) * k⁻¹ : by rewrite [mul.assoc (g * h⁻¹)]
|
||||||
|
... = g * k⁻¹ : by rewrite inv_mul_cancel_right,
|
||||||
|
show N (g * k⁻¹), from H2 ▸ H1
|
||||||
|
|
||||||
|
theorem is_equivalence_quotient_rel : is_equivalence (quotient_rel N) :=
|
||||||
|
is_equivalence.mk quotient_rel_refl
|
||||||
|
(λg h, quotient_rel_symm)
|
||||||
|
(λg h k, quotient_rel_trans)
|
||||||
|
|
||||||
|
-- We prove that quotient_rel respects inverses and multiplication, so
|
||||||
|
-- it is a congruence relation
|
||||||
|
theorem quotient_rel_resp_inv (r : quotient_rel N g h) : quotient_rel N g⁻¹ h⁻¹ :=
|
||||||
|
have H1 : N (g⁻¹ * (h * g⁻¹) * g), from
|
||||||
|
is_normal_subgroup' N g (quotient_rel_symm r),
|
||||||
|
have H2 : g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h⁻¹⁻¹, from calc
|
||||||
|
g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h * g⁻¹ * g : by rewrite -mul.assoc
|
||||||
|
... = g⁻¹ * h : inv_mul_cancel_right
|
||||||
|
... = g⁻¹ * h⁻¹⁻¹ : by rewrite algebra.inv_inv,
|
||||||
|
show N (g⁻¹ * h⁻¹⁻¹), from H2 ▸ H1
|
||||||
|
|
||||||
|
theorem quotient_rel_resp_mul (r : quotient_rel N g h) (r' : quotient_rel N g' h')
|
||||||
|
: quotient_rel N (g * g') (h * h') :=
|
||||||
|
have H1 : N (g * ((g' * h'⁻¹) * h⁻¹)), from
|
||||||
|
normal_subgroup_insert N r' r,
|
||||||
|
have H2 : g * ((g' * h'⁻¹) * h⁻¹) = (g * g') * (h * h')⁻¹, from calc
|
||||||
|
g * ((g' * h'⁻¹) * h⁻¹) = g * (g' * (h'⁻¹ * h⁻¹)) : by rewrite [mul.assoc]
|
||||||
|
... = (g * g') * (h'⁻¹ * h⁻¹) : mul.assoc
|
||||||
|
... = (g * g') * (h * h')⁻¹ : by rewrite [mul_inv],
|
||||||
|
show N ((g * g') * (h * h')⁻¹), from transport (λx, N x) H2 H1
|
||||||
|
|
||||||
|
local attribute is_equivalence_quotient_rel [instance]
|
||||||
|
|
||||||
|
variable (N)
|
||||||
|
|
||||||
|
definition qg : Type := set_quotient (quotient_rel N)
|
||||||
|
|
||||||
|
variable {N}
|
||||||
|
|
||||||
|
local attribute qg [reducible]
|
||||||
|
|
||||||
|
definition quotient_one [constructor] : qg N := class_of one
|
||||||
|
definition quotient_inv [unfold 3] : qg N → qg N :=
|
||||||
|
quotient_unary_map has_inv.inv (λg g' r, quotient_rel_resp_inv r)
|
||||||
|
definition quotient_mul [unfold 3 4] : qg N → qg N → qg N :=
|
||||||
|
quotient_binary_map has_mul.mul (λg g' r h h' r', quotient_rel_resp_mul r r')
|
||||||
|
|
||||||
|
section
|
||||||
|
local notation 1 := quotient_one
|
||||||
|
local postfix ⁻¹ := quotient_inv
|
||||||
|
local infix * := quotient_mul
|
||||||
|
|
||||||
|
theorem quotient_mul_assoc (g₁ g₂ g₃ : qg N) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g₁,
|
||||||
|
refine set_quotient.rec_prop _ g₂,
|
||||||
|
refine set_quotient.rec_prop _ g₃,
|
||||||
|
clear g₁ g₂ g₃, intro g₁ g₂ g₃,
|
||||||
|
exact ap class_of !mul.assoc
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem quotient_one_mul (g : qg N) : 1 * g = g :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g, clear g, intro g,
|
||||||
|
exact ap class_of !one_mul
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem quotient_mul_one (g : qg N) : g * 1 = g :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g, clear g, intro g,
|
||||||
|
exact ap class_of !mul_one
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem quotient_mul_left_inv (g : qg N) : g⁻¹ * g = 1 :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g, clear g, intro g,
|
||||||
|
exact ap class_of !mul.left_inv
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem quotient_mul_comm {G : CommGroup} {N : normal_subgroup_rel G} (g h : qg N)
|
||||||
|
: g * h = h * g :=
|
||||||
|
begin
|
||||||
|
refine set_quotient.rec_prop _ g, clear g, intro g,
|
||||||
|
refine set_quotient.rec_prop _ h, clear h, intro h,
|
||||||
|
apply ap class_of, esimp, apply mul.comm
|
||||||
|
end
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
variable (N)
|
||||||
|
definition group_qg [constructor] : group (qg N) :=
|
||||||
|
group.mk quotient_mul _ quotient_mul_assoc quotient_one quotient_one_mul quotient_mul_one
|
||||||
|
quotient_inv quotient_mul_left_inv
|
||||||
|
|
||||||
|
definition quotient_group [constructor] : Group :=
|
||||||
|
Group.mk _ (group_qg N)
|
||||||
|
|
||||||
|
definition comm_group_qg [constructor] {G : CommGroup} (N : normal_subgroup_rel G)
|
||||||
|
: comm_group (qg N) :=
|
||||||
|
⦃comm_group, group_qg N, mul_comm := quotient_mul_comm⦄
|
||||||
|
|
||||||
|
definition quotient_comm_group [constructor] {G : CommGroup} (N : subgroup_rel G)
|
||||||
|
: CommGroup :=
|
||||||
|
CommGroup.mk _ (comm_group_qg (normal_subgroup_rel_comm N))
|
||||||
|
|
||||||
|
definition gq_map : G →g quotient_group N :=
|
||||||
|
homomorphism.mk class_of (λ g h, idp)
|
||||||
|
|
||||||
|
namespace quotient
|
||||||
|
notation `⟦`:max a `⟧`:0 := gq_map a _
|
||||||
|
end quotient
|
||||||
|
|
||||||
|
open quotient
|
||||||
|
variable {N}
|
||||||
|
|
||||||
|
definition gq_map_eq_one (g : G) (H : N g) : gq_map N g = 1 :=
|
||||||
|
begin
|
||||||
|
apply eq_of_rel,
|
||||||
|
have e : (g * 1⁻¹ = g),
|
||||||
|
from calc
|
||||||
|
g * 1⁻¹ = g * 1 : one_inv
|
||||||
|
... = g : mul_one,
|
||||||
|
unfold quotient_rel, rewrite e, exact H
|
||||||
|
end
|
||||||
|
|
||||||
|
definition rel_of_gq_map_eq_one (g : G) (H : gq_map N g = 1) : N g :=
|
||||||
|
begin
|
||||||
|
have e : (g * 1⁻¹ = g),
|
||||||
|
from calc
|
||||||
|
g * 1⁻¹ = g * 1 : one_inv
|
||||||
|
... = g : mul_one,
|
||||||
|
rewrite (inverse e),
|
||||||
|
apply rel_of_eq _ H
|
||||||
|
end
|
||||||
|
|
||||||
|
definition quotient_group_elim (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' :=
|
||||||
|
begin
|
||||||
|
fapply homomorphism.mk,
|
||||||
|
-- define function
|
||||||
|
{ apply set_quotient.elim f,
|
||||||
|
intro g h K,
|
||||||
|
apply eq_of_mul_inv_eq_one,
|
||||||
|
have e : f (g * h⁻¹) = f g * (f h)⁻¹,
|
||||||
|
from calc
|
||||||
|
f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul
|
||||||
|
... = f g * (f h)⁻¹ : to_respect_inv,
|
||||||
|
rewrite (inverse e),
|
||||||
|
apply H, exact K},
|
||||||
|
{ intro g h, induction g using set_quotient.rec_prop with g,
|
||||||
|
induction h using set_quotient.rec_prop with h,
|
||||||
|
krewrite (inverse (to_respect_mul (gq_map N) g h)),
|
||||||
|
unfold gq_map, esimp, exact to_respect_mul f g h }
|
||||||
|
end
|
||||||
|
|
||||||
|
definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group_elim f H ∘g gq_map N ~ f :=
|
||||||
|
begin
|
||||||
|
intro g, reflexivity
|
||||||
|
end
|
||||||
|
|
||||||
|
definition glift_unique (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (k : quotient_group N →g G')
|
||||||
|
: ( k ∘g gq_map N ~ f ) → k ~ quotient_group_elim f H :=
|
||||||
|
begin
|
||||||
|
intro K cg, induction cg using set_quotient.rec_prop with g,
|
||||||
|
krewrite (quotient_group_compute f),
|
||||||
|
exact K g
|
||||||
|
end
|
||||||
|
|
||||||
|
definition gq_universal_property (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) :
|
||||||
|
is_contr (Σ(g : quotient_group N →g G'), g ∘g gq_map N = f) :=
|
||||||
|
sorry
|
||||||
|
|
||||||
|
/- set generating normal subgroup -/
|
||||||
|
|
||||||
|
section
|
||||||
|
|
||||||
|
parameters {GG : CommGroup} (S : GG → Prop)
|
||||||
|
|
||||||
|
inductive generating_relation' : GG → Type :=
|
||||||
|
| rincl : Π{g}, S g → generating_relation' g
|
||||||
|
| rmul : Π{g h}, generating_relation' g → generating_relation' h → generating_relation' (g * h)
|
||||||
|
| rinv : Π{g}, generating_relation' g → generating_relation' g⁻¹
|
||||||
|
| rone : generating_relation' 1
|
||||||
|
open generating_relation'
|
||||||
|
definition generating_relation (g : GG) : Prop := ∥ generating_relation' g ∥
|
||||||
|
local abbreviation R := generating_relation
|
||||||
|
definition gr_one : R 1 := tr (rone S)
|
||||||
|
definition gr_inv (g : GG) : R g → R g⁻¹ :=
|
||||||
|
trunc_functor -1 rinv
|
||||||
|
definition gr_mul (g h : GG) : R g → R h → R (g * h) :=
|
||||||
|
trunc_functor2 rmul
|
||||||
|
|
||||||
|
definition normal_generating_relation : subgroup_rel GG :=
|
||||||
|
⦃ subgroup_rel,
|
||||||
|
R := generating_relation,
|
||||||
|
Rone := gr_one,
|
||||||
|
Rinv := gr_inv,
|
||||||
|
Rmul := gr_mul⦄
|
||||||
|
|
||||||
|
parameter (GG)
|
||||||
|
definition quotient_comm_group_gen : CommGroup := quotient_comm_group normal_generating_relation
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
end group
|
||||||
Loading…
Reference in a new issue