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

some small changes, move aut to group_constructions

Browse source
This commit is contained in:
Floris van Doorn 2016-09-14 17:11:44 -04:00
parent 65e6e062be
commit d2f95f344f
2 changed files with 25 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
algebra/group_basics.hlean
View file

@ -70,7 +70,7 @@ namespace group
variables {G₁ G₂ : Group} variables {G₁ G₂ : Group}
-- TODO: maybe define this in more generality for pointed types? <-- Do you mean pointed sets? -- TODO: maybe define this in more generality for pointed sets?
definition kernel_pred [constructor] (φ : G₁ →g G₂) (g : G₁) : Prop := trunctype.mk (φ g = 1) _ definition kernel_pred [constructor] (φ : G₁ →g G₂) (g : G₁) : Prop := trunctype.mk (φ g = 1) _
theorem kernel_mul (φ : G₁ →g G₂) (g h : G₁) (H₁ : kernel_pred φ g) (H₂ : kernel_pred φ h) : kernel_pred φ (g *[G₁] h) := theorem kernel_mul (φ : G₁ →g G₂) (g h : G₁) (H₁ : kernel_pred φ g) (H₂ : kernel_pred φ h) : kernel_pred φ (g *[G₁] h) :=
@ -109,34 +109,18 @@ namespace group
/-- Next, we formalize some aspects of normal subgroups. Recall that a normal subgroup H of a group G is a subgroup which is invariant under all inner automorophisms on G. --/ /-- Next, we formalize some aspects of normal subgroups. Recall that a normal subgroup H of a group G is a subgroup which is invariant under all inner automorophisms on G. --/
definition aut.{u} (G : Group.{u}) : Group.{u} := definition is_normal [constructor] {G : Group} (R : G → Prop) : Prop :=
begin trunctype.mk (Π{g} h, R g → R (h * g * h⁻¹)) _
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⁻¹ --/
/-- There is a problem with the following definition, namely that there is no mere proposition that says that N is normal --/
structure normal_subgroup_rel (G : Group) extends subgroup_rel G := structure normal_subgroup_rel (G : Group) extends subgroup_rel G :=
(is_normal : Π{g} h, R g → R (h * g * h⁻¹)) (is_normal_subgroup : is_normal R)
/-- expect something like (is_normal : isNormal R) where isNormal R is a predefined predicate on subgroups of G --/
attribute subgroup_rel.R [coercion] attribute subgroup_rel.R [coercion]
abbreviation subgroup_to_rel [unfold 2] := @subgroup_rel.R abbreviation subgroup_to_rel [unfold 2] := @subgroup_rel.R
abbreviation subgroup_has_one [unfold 2] := @subgroup_rel.Rone abbreviation subgroup_has_one [unfold 2] := @subgroup_rel.Rone
abbreviation subgroup_respect_mul [unfold 2] := @subgroup_rel.Rmul abbreviation subgroup_respect_mul [unfold 2] := @subgroup_rel.Rmul
abbreviation subgroup_respect_inv [unfold 2] := @subgroup_rel.Rinv abbreviation subgroup_respect_inv [unfold 2] := @subgroup_rel.Rinv
abbreviation is_normal_subgroup [unfold 2] := @normal_subgroup_rel.is_normal abbreviation is_normal_subgroup [unfold 2] := @normal_subgroup_rel.is_normal_subgroup
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}
@ -146,7 +130,7 @@ namespace group
definition normal_subgroup_rel_comm.{u} (R : subgroup_rel.{_ u} A) : normal_subgroup_rel.{_ u} A := definition normal_subgroup_rel_comm.{u} (R : subgroup_rel.{_ u} A) : normal_subgroup_rel.{_ u} A :=
⦃normal_subgroup_rel, R, ⦃normal_subgroup_rel, R,
is_normal := abstract begin is_normal_subgroup := abstract begin
intros g h r, xrewrite [mul.comm h g, mul_inv_cancel_right], exact r intros g h r, xrewrite [mul.comm h g, mul_inv_cancel_right], exact r
end end⦄ end end⦄
@ -187,7 +171,7 @@ namespace group
definition normal_subgroup_kernel [constructor] {G₁ G₂ : Group} (φ : G₁ →g G₂) : normal_subgroup_rel G₁ := definition normal_subgroup_kernel [constructor] {G₁ G₂ : Group} (φ : G₁ →g G₂) : normal_subgroup_rel G₁ :=
⦃ normal_subgroup_rel, ⦃ normal_subgroup_rel,
kernel_subgroup φ, kernel_subgroup φ,
is_normal := is_normal_subgroup_kernel φ is_normal_subgroup := is_normal_subgroup_kernel φ
⦄ ⦄
-- this is just (Σ(g : G), H g), but only defined if (H g) is a prop -- this is just (Σ(g : G), H g), but only defined if (H g) is a prop

18
algebra/group_constructions.hlean
View file

@ -12,6 +12,24 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum
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}