michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

give the definition of the I-ary direct sum

Browse source
This commit is contained in:
Floris van Doorn 2016-03-31 13:22:45 -04:00
parent a6bf82618f
commit c1038a3f96
1 changed files with 53 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

56
group_theory/constructions.hlean
View file

@ -36,6 +36,12 @@ namespace group
theorem is_normal_subgroup' (h : G) (r : N g) : N (h⁻¹ * g * h) := theorem is_normal_subgroup' (h : G) (r : N g) : N (h⁻¹ * g * h) :=
inv_inv h ▸ is_normal_subgroup N h⁻¹ r inv_inv h ▸ is_normal_subgroup N h⁻¹ r
definition normal_subgroup_rel_comm.{u} (R : subgroup_rel.{_ u} A) : normal_subgroup_rel.{_ u} A :=
⦃normal_subgroup_rel, R,
is_normal := abstract begin
intros g h r, xrewrite [mul.comm h g, mul_inv_cancel_right], exact r
end end⦄
theorem is_normal_subgroup_rev (h : G) (r : N (h * g * h⁻¹)) : N g := theorem is_normal_subgroup_rev (h : G) (r : N (h * g * h⁻¹)) : N g :=
have H : h⁻¹ * (h * g * h⁻¹) * h = g, from calc have H : h⁻¹ * (h * g * h⁻¹) * h = g, from calc
h⁻¹ * (h * g * h⁻¹) * h = h⁻¹ * (h * g) * h⁻¹ * h : by rewrite [-mul.assoc h⁻¹] h⁻¹ * (h * g * h⁻¹) * h = h⁻¹ * (h * g) * h⁻¹ * h : by rewrite [-mul.assoc h⁻¹]
@ -212,9 +218,9 @@ namespace group
: comm_group (qg N) := : comm_group (qg N) :=
⦃comm_group, group_qg N, mul_comm := quotient_mul_comm⦄ ⦃comm_group, group_qg N, mul_comm := quotient_mul_comm⦄
definition quotient_comm_group [constructor] {G : CommGroup} (N : normal_subgroup_rel G) definition quotient_comm_group [constructor] {G : CommGroup} (N : subgroup_rel G)
: CommGroup := : CommGroup :=
CommGroup.mk _ (comm_group_qg N) CommGroup.mk _ (comm_group_qg (normal_subgroup_rel_comm N))
/- Binary products (direct sums) of Groups -/ /- Binary products (direct sums) of Groups -/
definition product_one [constructor] : G × G' := (one, one) definition product_one [constructor] : G × G' := (one, one)
@ -596,7 +602,51 @@ namespace group
exact !to_respect_inv⁻¹}} exact !to_respect_inv⁻¹}}
end end
/- Free Commutative Group of a set -/ /- 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) -/
/- namespace tensor_group /- namespace tensor_group
variables {A B} variables {A B}