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

base subgroups on sets and unbundle

Browse source
This commit is contained in:
Jeremy Avigad 2017-04-07 15:12:31 -04:00
parent a001491183
commit c74779959a
3 changed files with 280 additions and 190 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

366
algebra/subgroup.hlean
View file

@ -1,73 +1,65 @@
/-
Copyright (c) 2015 Egbert Rijke. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Egbert Rijke
Authors: Floris van Doorn, Egbert Rijke, Jeremy Avigad
Basic concepts of group theory
-/
import algebra.group_theory ..move_to_lib ..set
import algebra.group_theory ..move_to_lib
open eq algebra is_trunc sigma sigma.ops prod trunc
open eq algebra is_trunc sigma sigma.ops prod trunc set
namespace group
/- #Subgroups -/
/-- Recall that a subtype of a type A is the same thing as a family of mere propositions over A. Thus, we define a subgroup of a group G to be a family of mere propositions over (the underlying type of) G, closed under the constants and operations --/
/-- Recall that a subtype of a type A is the same thing as a family
of mere propositions over A. Thus, we define a subgroup of a
group G to be a family of mere propositions over (the underlying
type of) G, closed under the constants and operations --/
/-- Question: Why is this called subgroup_rel. Because it is a unary relation? --/
structure subgroup_rel (G : Group) : Type :=
(R : G → Prop)
(Rone : R one)
(Rmul : Π{g h}, R g → R h → R (g * h))
(Rinv : Π{g}, R g → R (g⁻¹))
attribute subgroup_rel.R [coercion]
structure is_subgroup [class] (G : Group) (H : set G) : Type :=
(one_mem : 1 ∈ H)
(mul_mem : Π{g h}, g ∈ H → h ∈ H → g * h ∈ H)
(inv_mem : Π{g}, g ∈ H → g⁻¹ ∈ H)
/-- Every group G has at least two subgroups, the trivial subgroup containing only one, and the full subgroup. --/
definition trivial_subgroup.{u} (G : Group.{u}) : subgroup_rel.{u u} G :=
definition trivial_subgroup [instance] (G : Group) : is_subgroup G '{1} :=
begin
fapply subgroup_rel.mk,
{ intro g, fapply trunctype.mk, exact (g = one), exact _ },
{ esimp },
{ intros g h p q, esimp at *, rewrite p, rewrite q, exact mul_one one},
{ intros g p, esimp at *, rewrite p, exact one_inv }
fapply is_subgroup.mk,
{ esimp, apply mem_insert },
{ intros g h p q, esimp at *, apply mem_singleton_of_eq, rewrite [eq_of_mem_singleton p, eq_of_mem_singleton q, mul_one]},
{ intros g p, esimp at *, apply mem_singleton_of_eq, rewrite [eq_of_mem_singleton p, one_inv] }
end
definition is_trivial_subgroup (G : Group) (R : subgroup_rel G) : Type :=
(Π g : G, R g → g = 1)
definition full_subgroup.{u} (G : Group.{u}) : subgroup_rel.{u 0} G :=
definition full_subgroup [instance] (G : Group) : is_subgroup G univ :=
begin
fapply subgroup_rel.mk,
{ intro g, fapply trunctype.mk, exact unit, exact _ },
{ esimp, constructor },
{ intros g h p q, esimp, constructor },
{ intros g p, esimp, constructor }
fapply is_subgroup.mk,
{ apply logic.trivial },
{ intros, apply logic.trivial },
{ intros, apply logic.trivial }
end
definition is_full_subgroup (G : Group) (R : subgroup_rel G) : Prop :=
trunctype.mk' -1 (Π g : G, R g)
/-- Every group homomorphism f : G -> H determines a subgroup of H,
the image of f, and a subgroup of G, the kernel of f. In the
following definition we define the image of f. Since a subgroup
is required to be closed under the group operations, showing
that the image of f is closed under the group operations is part
of the definition of the image of f. --/
/-- Every group homomorphism f : G -> H determines a subgroup of H, the image of f, and a subgroup of G, the kernel of f. In the following definition we define the image of f. Since a subgroup is required to be closed under the group operations, showing that the image of f is closed under the group operations is part of the definition of the image of f. --/
/-- TODO. We need to find some reasonable way of dealing with universe levels. The reason why it currently is what it is, is because lean is inflexible with universe leves once tactic mode is started --/
definition image_subgroup.{u1 u2} {G : Group.{u1}} {H : Group.{u2}} (f : G →g H) : subgroup_rel.{u2 (max u1 u2)} H :=
definition image_subgroup [instance] {G : Group} {H : Group} (f : G →g H) :
is_subgroup H (image f) :=
begin
fapply subgroup_rel.mk,
-- definition of the subset
{ intro h, apply ttrunc, exact fiber f h},
fapply is_subgroup.mk,
-- subset contains 1
{ apply trunc.tr, fapply fiber.mk, exact 1, apply respect_one},
{ fapply image.mk, exact 1, apply respect_one},
-- subset is closed under multiplication
{ intro h h', intro u v,
induction u with p, induction v with q,
induction p with x p, induction q with y q,
induction u with x p, induction v with y q,
induction p, induction q,
apply tr, apply fiber.mk (x * y), apply respect_mul},
apply image.mk (x * y), apply respect_mul},
-- subset is closed under inverses
{ intro g, intro t, induction t, induction a with x p, induction p,
apply tr, apply fiber.mk x⁻¹, apply respect_inv }
{ intro g, intro t, induction t with x p, induction p,
apply image.mk x⁻¹, apply respect_inv }
end
section kernels
@ -75,92 +67,90 @@ namespace group
variables {G₁ G₂ : Group}
-- 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 [constructor] (φ : G₁ →g G₂) : set G₁ := { g | 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) :=
begin
esimp at *,
exact calc
φ (g * h) = (φ g) * (φ h) : to_respect_mul
... = 1 * (φ h) : H₁
... = 1 * 1 : H₂
... = 1 : one_mul
end
theorem mul_mem_kernel (φ : G₁ →g G₂) (g h : G₁) (H₁ : g ∈ kernel φ) (H₂ : h ∈ kernel φ) : g * h ∈ kernel φ :=
calc
φ (g * h) = (φ g) * (φ h) : to_respect_mul
... = 1 * (φ h) : H₁
... = 1 * 1 : H₂
... = 1 : one_mul
theorem kernel_inv (φ : G₁ →g G₂) (g : G₁) (H : kernel_pred φ g) : kernel_pred φ (g⁻¹) :=
begin
esimp at *,
exact calc
φ g⁻¹ = (φ g)⁻¹ : to_respect_inv
... = 1⁻¹ : H
... = 1 : one_inv
end
theorem inv_mem_kernel (φ : G₁ →g G₂) (g : G₁) (H : g ∈ kernel φ) : g⁻¹ ∈ kernel φ :=
calc
φ g⁻¹ = (φ g)⁻¹ : to_respect_inv
... = 1⁻¹ : H
... = 1 : one_inv
definition kernel_subgroup [constructor] (φ : G₁ →g G₂) : subgroup_rel G₁ :=
⦃ subgroup_rel,
R := kernel_pred φ,
Rone := respect_one φ,
Rmul := kernel_mul φ,
Rinv := kernel_inv φ
definition is_subgroup_kernel [constructor] [instance] (φ : G₁ →g G₂) : is_subgroup G₁ (kernel φ) :=
⦃ is_subgroup,
one_mem := respect_one φ,
mul_mem := mul_mem_kernel φ,
inv_mem := inv_mem_kernel φ
⦄
end kernels
/-- Now we should be able to show that if f is a homomorphism for which the kernel is trivial and the image is full, then f is an isomorphism, except that no one defined the proposition that f is an isomorphism :/ --/
-- definition is_iso_from_kertriv_imfull {G H : Group} (f : G →g H) : is_trivial_subgroup G (kernel f) → is_full_subgroup H (image_subgroup f) → unit /- replace unit by is_isomorphism f -/ := sorry
/-- Now we should be able to show that if f is a homomorphism for which the kernel is trivial and the
image is full, then f is an isomorphism, except that no one defined the proposition that f is an
isomorphism :/ --/
/- definition is_iso_from_kertriv_imfull {G H : Group} (f : G →g H) :
is_trivial_subgroup G (kernel f) → is_full_subgroup H (image_subgroup f) → unit
/- replace unit by is_isomorphism f -/ := sorry -/
/- #Normal subgroups -/
/-- 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 is_normal.{u v} [constructor] {G : Group.{u}} (R : G → Prop.{v}) : Prop.{max u v} :=
trunctype.mk (Π{g} h, R g → R (h * g * h⁻¹)) _
definition is_normal [constructor] (G : Group) (N : set G) : Prop :=
trunctype.mk (Π{g} h, g ∈ N → h * g * h⁻¹ ∈ N) _
structure normal_subgroup_rel (G : Group) extends subgroup_rel G :=
(is_normal_subgroup : is_normal R)
structure is_normal_subgroup [class] (G : Group) (N : set G) extends is_subgroup G N :=
(is_normal : is_normal G N)
attribute subgroup_rel.R [coercion]
abbreviation subgroup_to_rel [unfold 2] := @subgroup_rel.R
abbreviation subgroup_has_one [unfold 2] := @subgroup_rel.Rone
abbreviation subgroup_respect_mul [unfold 2] := @subgroup_rel.Rmul
abbreviation subgroup_respect_inv [unfold 2] := @subgroup_rel.Rinv
abbreviation is_normal_subgroup [unfold 2] := @normal_subgroup_rel.is_normal_subgroup
abbreviation subgroup_one_mem [unfold 2] := @is_subgroup.one_mem
abbreviation subgroup_mul_mem [unfold 2] := @is_subgroup.mul_mem
abbreviation subgroup_inv_mem [unfold 2] := @is_subgroup.inv_mem
abbreviation subgroup_is_normal [unfold 2] := @is_normal_subgroup.is_normal
section
variables {G G' G₁ G₂ G₃ : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
section
variables {G G' G₁ G₂ G₃ : Group} {H N : set G} [is_subgroup G H]
[is_normal_subgroup G N] {g g' h h' k : G}
{A B : AbGroup}
theorem is_normal_subgroup' (h : G) (r : N g) : N (h⁻¹ * g * h) :=
inv_inv h ▸ is_normal_subgroup N h⁻¹ r
theorem is_normal_subgroup' (h : G) (r : g ∈ N) : h⁻¹ * g * h ∈ N :=
inv_inv h ▸ subgroup_is_normal N h⁻¹ r
definition normal_subgroup_rel_ab.{u} [constructor] (R : subgroup_rel.{_ u} A)
: normal_subgroup_rel.{_ u} A :=
⦃normal_subgroup_rel, R,
is_normal_subgroup := abstract begin
definition is_normal_subgroup_ab.{u} [constructor] {C : set A} (subgrpA : is_subgroup A C)
: is_normal_subgroup A C :=
⦃ is_normal_subgroup, subgrpA,
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 : h * g * h⁻¹ ∈ N) : g ∈ N :=
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) : by rewrite [inv_mul_cancel_right]
... = g : inv_mul_cancel_left,
H ▸ is_normal_subgroup' N h r
H ▸ is_normal_subgroup' h r
theorem is_normal_subgroup_rev' (h : G) (r : N (h⁻¹ * g * h)) : N g :=
is_normal_subgroup_rev N h⁻¹ ((inv_inv h)⁻¹ ▸ r)
theorem is_normal_subgroup_rev' (h : G) (r : h⁻¹ * g * h ∈ N) : g ∈ N :=
is_normal_subgroup_rev h⁻¹ ((inv_inv h)⁻¹ ▸ r)
theorem normal_subgroup_insert (r : N k) (r' : N (g * h)) : N (g * (k * h)) :=
have H1 : N ((g * h) * (h⁻¹ * k * h)), from
subgroup_respect_mul N r' (is_normal_subgroup' N h r),
theorem normal_subgroup_insert (r : k ∈ N) (r' : g * h ∈ N) : g * (k * h) ∈ N :=
have H1 : (g * h) * (h⁻¹ * k * h) ∈ N, from
subgroup_mul_mem r' (is_normal_subgroup' h r),
have H2 : (g * h) * (h⁻¹ * k * h) = g * (k * h), from calc
(g * h) * (h⁻¹ * k * h) = g * (h * (h⁻¹ * k * h)) : mul.assoc
... = g * (h * (h⁻¹ * (k * h))) : by rewrite [mul.assoc h⁻¹]
... = g * (k * h) : by rewrite [mul_inv_cancel_left],
show N (g * (k * h)), from H2 ▸ H1
/-- In the following, we show that the kernel of any group homomorphism f : G₁ →g G₂ is a normal subgroup of G₁ --/
theorem is_normal_subgroup_kernel {G₁ G₂ : Group} (φ : G₁ →g G₂) (g : G₁) (h : G₁)
: kernel_pred φ g → kernel_pred φ (h * g * h⁻¹) :=
: g ∈ kernel φ → h * g * h⁻¹ ∈ kernel φ :=
begin
esimp at *,
intro p,
@ -173,22 +163,17 @@ namespace group
... = 1 : mul.right_inv
end
/-- Thus, we extend the kernel subgroup to a normal subgroup --/
definition normal_subgroup_kernel [constructor] {G₁ G₂ : Group} (φ : G₁ →g G₂) : normal_subgroup_rel G₁ :=
⦃ normal_subgroup_rel,
kernel_subgroup φ,
is_normal_subgroup := is_normal_subgroup_kernel φ
⦄
-- this is just (Σ(g : G), H g), but only defined if (H g) is a prop
definition sg : Type := {g : G | H g}
definition sg {G : Group} (H : set G) : Type := {g : G | g ∈ H}
local attribute sg [reducible]
variable {H}
definition subgroup_one [constructor] : sg H := ⟨one, !subgroup_has_one⟩
definition subgroup_one [constructor] : sg H := ⟨one, subgroup_one_mem H⟩
definition subgroup_inv [unfold 3] : sg H → sg H :=
λv, ⟨v.1⁻¹, subgroup_respect_inv H v.2⟩
λv, ⟨v.1⁻¹, subgroup_inv_mem v.2⟩
definition subgroup_mul [unfold 3 4] : sg H → sg H → sg H :=
λv w, ⟨v.1 * w.1, subgroup_respect_mul H v.2 w.2⟩
λv w, ⟨v.1 * w.1, subgroup_mul_mem v.2 w.2⟩
definition subgroup_elt (x : sg H) : G := x.1
section
local notation 1 := subgroup_one
@ -207,43 +192,52 @@ namespace group
theorem subgroup_mul_left_inv (g : sg H) : g⁻¹ * g = 1 :=
subtype_eq !mul.left_inv
theorem subgroup_mul_comm {G : AbGroup} {H : subgroup_rel G} (g h : sg H)
: g * h = h * g :=
theorem subgroup_mul_comm {G : AbGroup} {H : set G} [subgrpH : is_subgroup G H] (g h : sg H)
: subgroup_mul g h = subgroup_mul h g :=
subtype_eq !mul.comm
end
variable (H)
definition group_sg [constructor] : group (sg H) :=
group.mk _ subgroup_mul subgroup_mul_assoc subgroup_one subgroup_one_mul subgroup_mul_one
subgroup_inv subgroup_mul_left_inv
subgroup_inv subgroup_mul_left_inv
definition subgroup [constructor] : Group :=
Group.mk _ (group_sg H)
definition ab_group_sg [constructor] {G : AbGroup} (H : subgroup_rel G)
: ab_group (sg H) :=
⦃ab_group, group_sg H, mul_comm := subgroup_mul_comm⦄
variable {H}
definition ab_subgroup [constructor] {G : AbGroup} (H : subgroup_rel G)
definition ab_group_sg [constructor] {G : AbGroup} (H : set G) [is_subgroup G H]
: ab_group (sg H) :=
⦃ab_group, (group_sg H), mul_comm := subgroup_mul_comm⦄
definition ab_subgroup [constructor] {G : AbGroup} (H : set G) [is_subgroup G H]
: AbGroup :=
AbGroup.mk _ (ab_group_sg H)
definition kernel {G H : Group} (f : G →g H) : Group := subgroup (kernel_subgroup f)
definition Kernel {G H : Group} (f : G →g H) : Group := subgroup (kernel f)
definition ab_kernel {G H : AbGroup} (f : G →g H) : AbGroup := ab_subgroup (kernel_subgroup f)
definition ab_kernel {G H : AbGroup} (f : G →g H) : AbGroup := ab_subgroup (kernel f)
definition incl_of_subgroup [constructor] {G : Group} (H : subgroup_rel G) : subgroup H →g G :=
definition incl_of_subgroup [constructor] {G : Group} (H : set G) [is_subgroup G H] :
subgroup H →g G :=
begin
fapply homomorphism.mk,
-- the underlying function
{ intro h, induction h with g, exact g},
-- is a homomorphism
-- is a homomorphism
intro g h, reflexivity
end
definition is_embedding_incl_of_subgroup {G : Group} (H : subgroup_rel G) : is_embedding (incl_of_subgroup H) :=
function.is_embedding_pr1 _
definition is_embedding_incl_of_subgroup {G : Group} (H : set G) [is_subgroup G H] :
is_embedding (incl_of_subgroup H) :=
begin
fapply function.is_embedding_of_is_injective,
intro h h',
fapply subtype_eq
end
definition ab_kernel_incl {G H : AbGroup} (f : G →g H) : ab_kernel f →g G :=
begin
@ -255,27 +249,41 @@ namespace group
fapply is_embedding_incl_of_subgroup,
end
definition subgroup_rel_of_subgroup {G : Group} (H1 H2 : subgroup_rel G) (hyp : Π (g : G), subgroup_rel.R H1 g → subgroup_rel.R H2 g) : subgroup_rel (subgroup H2) :=
subgroup_rel.mk
-- definition of the subset
(λ h, H1 (incl_of_subgroup H2 h))
-- contains 1
(subgroup_has_one H1)
-- closed under multiplication
(λ g h p q, subgroup_respect_mul H1 p q)
-- closed under inverses
(λ h p, subgroup_respect_inv H1 p)
definition is_subgroup_of_subgroup {G : Group} {H1 H2 : set G} [is_subgroup G H1]
[is_subgroup G H2] (hyp : Π (g : G), g ∈ H1 → g ∈ H2) :
is_subgroup (subgroup H2) {h | incl_of_subgroup H2 h ∈ H1} :=
is_subgroup.mk
(subgroup_one_mem H1)
(begin
intros g h p q,
apply mem_set_of,
apply subgroup_mul_mem (of_mem_set_of p) (of_mem_set_of q),
end)
(begin
intros h p,
apply mem_set_of,
apply subgroup_inv_mem (of_mem_set_of p)
end)
definition image {G H : Group} (f : G →g H) : Group :=
subgroup (image_subgroup f)
definition Image {G H : Group} (f : G →g H) : Group :=
subgroup (image f)
definition ab_image {G : AbGroup} {H : AbGroup} (f : G →g H) : AbGroup :=
ab_subgroup (image_subgroup f)
definition ab_image {G : AbGroup} {H : Group} (f : G →g H) : AbGroup :=
AbGroup_of_Group (Image f)
begin
intro g h,
induction g with x t, induction h with y s,
fapply subtype_eq,
induction t with g p, induction s with h q, induction p, induction q,
refine (((respect_mul f g h)⁻¹ ⬝ _) ⬝ (respect_mul f h g)),
apply (ap f),
induction G, induction struct', apply mul_comm
end
definition image_incl {G H : Group} (f : G →g H) : image f →g H :=
incl_of_subgroup (image_subgroup f)
definition image_incl {G H : Group} (f : G →g H) : Image f →g H :=
incl_of_subgroup (image f)
definition ab_image_incl {A B : AbGroup} (f : A →g B) : ab_image f →g B := incl_of_subgroup (image_subgroup f)
definition ab_image_incl {A B : AbGroup} (f : A →g B) : ab_image f →g B := incl_of_subgroup (image f)
definition is_equiv_surjection_ab_image_incl {A B : AbGroup} (f : A →g B) (H : is_surjective f) : is_equiv (ab_image_incl f ) :=
begin
@ -298,7 +306,7 @@ definition iso_surjection_ab_image_incl [constructor] {A B : AbGroup} (f : A →
exact is_equiv_surjection_ab_image_incl f H
end
definition hom_lift [constructor] {G H : Group} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : G →g subgroup K :=
definition hom_lift [constructor] {G H : Group} (f : G →g H) (K : set H) [is_subgroup H K] (Hyp : Π (g : G), K (f g)) : G →g subgroup K :=
begin
fapply homomorphism.mk,
intro g,
@ -308,14 +316,14 @@ definition hom_lift [constructor] {G H : Group} (f : G →g H) (K : subgroup_rel
intro g h, apply subtype_eq, esimp, apply respect_mul
end
definition hom_factors_through_lift {G H : Group} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) :
definition hom_factors_through_lift {G H : Group} (f : G →g H) (K : set H) [is_subgroup H K] (Hyp : Π (g : G), K (f g)) :
f = incl_of_subgroup K ∘g hom_lift f K Hyp :=
begin
fapply homomorphism_eq,
reflexivity
end
definition ab_hom_lift [constructor] {G H : AbGroup} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : G →g ab_subgroup K :=
definition ab_hom_lift [constructor] {G H : AbGroup} (f : G →g H) (K : set H) [is_subgroup H K] (Hyp : Π (g : G), K (f g)) : G →g ab_subgroup K :=
begin
fapply homomorphism.mk,
intro g,
@ -325,7 +333,7 @@ definition ab_hom_lift [constructor] {G H : AbGroup} (f : G →g H) (K : subgrou
intro g h, apply subtype_eq, apply respect_mul,
end
definition ab_hom_factors_through_lift {G H : AbGroup} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) :
definition ab_hom_factors_through_lift {G H : AbGroup} (f : G →g H) (K : set H) [is_subgroup H K] (Hyp : Π (g : G), K (f g)) :
f = incl_of_subgroup K ∘g hom_lift f K Hyp :=
begin
fapply homomorphism_eq,
@ -337,16 +345,16 @@ definition ab_hom_lift_kernel [constructor] {A B C : AbGroup} (f : A →g B) (g
fapply ab_hom_lift,
exact f,
intro a,
exact Hyp a,
exact Hyp a,
end
definition ab_hom_lift_kernel_factors {A B C : AbGroup} (f : A →g B) (g : B →g C) (Hyp : Π (a : A), g (f a) = 1) :
definition ab_hom_lift_kernel_factors {A B C : AbGroup} (f : A →g B) (g : B →g C) (Hyp : Π (a : A), g (f a) = 1) :
f = ab_kernel_incl g ∘g ab_hom_lift_kernel f g Hyp :=
begin
fapply ab_hom_factors_through_lift,
end
definition image_lift [constructor] {G H : Group} (f : G →g H) : G →g image f :=
definition image_lift [constructor] {G H : Group} (f : G →g H) : G →g Image f :=
begin
fapply hom_lift f,
intro g,
@ -355,7 +363,7 @@ f = ab_kernel_incl g ∘g ab_hom_lift_kernel f g Hyp :=
exact g, reflexivity
end
definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g image f :=
definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g Image f :=
begin
fapply hom_lift f,
intro g,
@ -367,7 +375,7 @@ definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g i
definition is_surjective_image_lift {G H : Group} (f : G →g H) : is_surjective (image_lift f) :=
begin
intro h,
induction h with h p, induction p with x, induction x with g p,
induction h with h p, induction p with g,
fapply image.mk,
exact g, induction p, reflexivity
end
@ -378,7 +386,8 @@ definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g i
reflexivity
end
definition image_incl_injective {G H : Group} (f : G →g H) : Π (x y : image f), (image_incl f x = image_incl f y) → (x = y) :=
definition image_incl_injective {G H : Group} (f : G →g H) : Π (x y : Image f),
(image_incl f x = image_incl f y) → (x = y) :=
begin
intro x y,
intro p,
@ -386,7 +395,8 @@ definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g i
exact p
end
definition image_incl_eq_one {G H : Group} (f : G →g H) : Π (x : image f), (image_incl f x = 1) → x = 1 :=
definition image_incl_eq_one {G H : Group} (f : G →g H) :
Π (x : Image f), (image_incl f x = 1) → x = 1 :=
begin
intro x,
fapply image_incl_injective f x 1,
@ -401,13 +411,14 @@ definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g i
open image
definition image_elim {f₁ : G₁ →g G₂} (f₂ : G₁ →g G₃) (h : Π⦃g⦄, f₁ g = 1 → f₂ g = 1) :
image f₁ →g G₃ :=
Image f₁ →g G₃ :=
homomorphism.mk (total_image.elim_set f₂ (image_elim_lemma h))
begin
refine total_image.rec _, intro g,
refine total_image.rec _, intro g',
exact to_respect_mul f₂ g g'
end
end
definition image_homomorphism {A B C : AbGroup} (f : A →g B) (g : B →g C) :
ab_image f →g ab_image (g ∘g f) :=
@ -424,14 +435,15 @@ definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g i
definition image_homomorphism_square {A B C : AbGroup} (f : A →g B) (g : B →g C) :
g ∘g image_incl f ~ image_incl (g ∘g f ) ∘g image_homomorphism f g :=
begin
intro x, induction x with b p, induction p with x, induction x with a p, induction p, reflexivity
intro x, induction x with b p, induction p with x, induction p, reflexivity
end
end
variables {G H K : Group} {R : subgroup_rel G} {S : subgroup_rel H} {T : subgroup_rel K}
variables {G H K : Group} {R : set G} [is_subgroup G R]
{S : set H} [is_subgroup H S] {T : set K} [is_subgroup K T]
open function
definition subgroup_functor_fun [unfold 7] (φ : G →g H) (h : Πg, R g → S (φ g)) (x : subgroup R) :
definition subgroup_functor_fun [unfold 7] (φ : G →g H) (h : Πg, g ∈ R → φ g ∈ S)
(x : subgroup R) :
subgroup S :=
begin
induction x with g hg,
@ -439,7 +451,7 @@ definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g i
end
definition subgroup_functor [constructor] (φ : G →g H)
(h : Πg, R g → S (φ g)) : subgroup R →g subgroup S :=
(h : Πg, g ∈ R → φ g ∈ S) : subgroup R →g subgroup S :=
begin
fapply homomorphism.mk,
{ exact subgroup_functor_fun φ h },
@ -447,13 +459,15 @@ definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g i
exact sigma_eq !to_respect_mul !is_prop.elimo }
end
definition ab_subgroup_functor [constructor] {G H : AbGroup} {R : subgroup_rel G}
{S : subgroup_rel H} (φ : G →g H)
(h : Πg, R g → S (φ g)) : ab_subgroup R →g ab_subgroup S :=
definition ab_subgroup_functor [constructor] {G H : AbGroup}
{R : set G} [is_subgroup G R]
{S : set H} [is_subgroup H S]
(φ : G →g H)
(h : Πg, g ∈ R → φ g ∈ S) : ab_subgroup R →g ab_subgroup S :=
subgroup_functor φ h
theorem subgroup_functor_compose (ψ : H →g K) (φ : G →g H)
(hψ : Πg, S g → T (ψ g)) (hφ : Πg, R g → S (φ g)) :
(hψ : Πg, g ∈ S → ψ g ∈ T) (hφ : Πg, g ∈ R → φ g ∈ S) :
subgroup_functor ψ hψ ∘g subgroup_functor φ hφ ~
subgroup_functor (ψ ∘g φ) (λg, proof hψ (φ g) qed ∘ hφ g) :=
begin
@ -465,28 +479,31 @@ definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g i
intro g, induction g with g hg, reflexivity
end
definition subgroup_functor_mul {G H : AbGroup} {R : subgroup_rel G} {S : subgroup_rel H}
(ψ φ : G →g H) (hψ : Πg, R g → S (ψ g)) (hφ : Πg, R g → S (φ g)) :
definition subgroup_functor_mul {G H : AbGroup} {R : set G} [subgroupR : is_subgroup G R]
{S : set H} [subgroupS : is_subgroup H S]
(ψ φ : G →g H) (hψ : Πg, g ∈ R → ψ g ∈ S) (hφ : Πg, g ∈ R → φ g ∈ S) :
homomorphism_mul (ab_subgroup_functor ψ hψ) (ab_subgroup_functor φ hφ) ~
ab_subgroup_functor (homomorphism_mul ψ φ)
(λg hg, subgroup_respect_mul S (hψ g hg) (hφ g hg)) :=
(λg hg, subgroup_mul_mem (hψ g hg) (hφ g hg)) :=
begin
intro g, induction g with g hg, reflexivity
end
definition subgroup_functor_homotopy {ψ φ : G →g H} (hψ : Πg, R g → S (ψ g))
(hφ : Πg, R g → S (φ g)) (p : φ ~ ψ) :
(hφ : Πg, g ∈ R → φ g ∈ S) (p : φ ~ ψ) :
subgroup_functor φ hφ ~ subgroup_functor ψ hψ :=
begin
intro g, induction g with g hg,
exact subtype_eq (p g)
end
definition subgroup_of_subgroup_incl {R S : subgroup_rel G} (H : Π (g : G), R g -> S g) : subgroup R →g subgroup S
definition subgroup_of_subgroup_incl {R S : set G} [is_subgroup G R] [is_subgroup G S]
(H : Π (g : G), g ∈ R → g ∈ S) : subgroup R →g subgroup S
:=
subgroup_functor (gid G) H
definition is_embedding_subgroup_of_subgroup_incl {R S : subgroup_rel G} (H : Π (g : G), R g -> S g) : is_embedding (subgroup_of_subgroup_incl H) :=
definition is_embedding_subgroup_of_subgroup_incl {R S : set G} [is_subgroup G R] [is_subgroup G S]
(H : Π (g : G), g ∈ R -> g ∈ S) : is_embedding (subgroup_of_subgroup_incl H) :=
begin
fapply is_embedding_of_is_injective,
intro x y p,
@ -495,16 +512,19 @@ definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g i
unfold subgroup_of_subgroup_incl at p, exact ap pr1 p,
end
definition ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : subgroup_rel A} (H : Π (a : A), R a -> S a) : ab_subgroup R →g ab_subgroup S
definition ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : set A} [is_subgroup A R] [is_subgroup A S]
(H : Π (a : A), a ∈ R → a ∈ S) : ab_subgroup R →g ab_subgroup S
:=
ab_subgroup_functor (gid A) H
definition is_embedding_ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : subgroup_rel A} (H : Π (a : A), R a -> S a) : is_embedding (ab_subgroup_of_subgroup_incl H) :=
definition is_embedding_ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : set A} [is_subgroup A R] [is_subgroup A S]
(H : Π (a : A), a ∈ R → a ∈ S) : is_embedding (ab_subgroup_of_subgroup_incl H) :=
begin
fapply is_embedding_subgroup_of_subgroup_incl,
fapply is_embedding_subgroup_of_subgroup_incl
end
definition ab_subgroup_iso {A : AbGroup} {R S : subgroup_rel A} (H : Π (a : A), R a -> S a) (K : Π (a : A), S a -> R a) :
definition ab_subgroup_iso {A : AbGroup} {R S : set A} [is_subgroup A R] [is_subgroup A S]
(H : Π (a : A), R a -> S a) (K : Π (a : A), S a -> R a) :
ab_subgroup R ≃g ab_subgroup S :=
begin
fapply isomorphism.mk,
@ -515,10 +535,12 @@ definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g i
intro r, induction r with a p, fapply subtype_eq, reflexivity
end
definition ab_subgroup_iso_triangle {A : AbGroup} {R S : subgroup_rel A} (H : Π (a : A), R a -> S a) (K : Π (a : A), S a -> R a) : incl_of_subgroup R ~ incl_of_subgroup S ∘g ab_subgroup_iso H K :=
definition ab_subgroup_iso_triangle {A : AbGroup} {R S : set A} [is_subgroup A R] [is_subgroup A S]
(H : Π (a : A), R a -> S a) (K : Π (a : A), S a -> R a) :
incl_of_subgroup R ~ incl_of_subgroup S ∘g ab_subgroup_iso H K :=
begin
intro r, induction r, reflexivity
end
end
end group

19
logic.hlean
View file

@ -25,15 +25,15 @@ tua (equiv_of_iff_of_is_prop h)
end
definition false : Prop := trunctype.mk empty _
definition false : Prop := trunctype.mk (lift empty) _
definition false.elim {A : Type} (h : false) : A := empty.elim h
definition false.elim {A : Type} (h : false) : A := lift.rec empty.elim h
definition true : Prop := trunctype.mk unit _
definition true : Prop := trunctype.mk (lift unit) _
definition true.intro : true := unit.star
definition true.intro : true := lift.up unit.star
definition trivial : true := unit.star
definition trivial : true := lift.up unit.star
definition and (p q : Prop) : Prop := tprod p q
@ -48,10 +48,15 @@ definition and.right {p q : Prop} (h : p ∧ q) : q := prod.pr2 h
definition not (p : Prop) : Prop := trunctype.mk (p → empty) _
prefix `~` := not
definition or.inl := @or.intro_left
definition or.inr := @or.intro_right
definition or.elim {A B C : Type} [is_prop C] (h₀ : A ∨ B) (h₁ : (A → C)) (h₂ : B → C) : C :=
begin
apply trunc.elim_on h₀,
intro h₃,
apply sum.elim h₃ h₁ h₂
end
end logic

85
set.hlean
View file

@ -18,8 +18,9 @@ definition mem (x : X) (a : set X) := a x
infix ∈ := mem
notation a ∉ b := ¬ mem a b
theorem ext {a b : set X} (H : ∀x, x ∈ a ↔ x ∈ b) : a = b :=
/-theorem ext {a b : set X} (H : ∀x, x ∈ a ↔ x ∈ b) : a = b :=
eq_of_homotopy (take x, propext (H x))
-/
definition subset (a b : set X) : Prop := Prop.mk (∀⦃x⦄, x ∈ a → x ∈ b) _
infix ⊆ := subset
@ -32,12 +33,16 @@ theorem subset.refl (a : set X) : a ⊆ a := take x, assume H, H
theorem subset.trans {a b c : set X} (subab : a ⊆ b) (subbc : b ⊆ c) : a ⊆ c :=
take x, assume ax, subbc (subab ax)
/-
theorem subset.antisymm {a b : set X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b :=
ext (λ x, iff.intro (λ ina, h₁ ina) (λ inb, h₂ inb))
-/
-- an alterantive name
/-
theorem eq_of_subset_of_subset {a b : set X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b :=
subset.antisymm h₁ h₂
-/
theorem mem_of_subset_of_mem {s₁ s₂ : set X} {a : X} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ :=
assume h₁ h₂, h₁ _ h₂
@ -45,29 +50,35 @@ assume h₁ h₂, h₁ _ h₂
/- empty set -/
definition empty : set X := λx, false
notation `∅` := empty
notation `∅` := set.empty
theorem not_mem_empty (x : X) : ¬ (x ∈ ∅) :=
assume H : x ∈ ∅, H
assume H : x ∈ ∅, false.elim H
theorem mem_empty_eq (x : X) : x ∈ ∅ = false := rfl
/-
theorem eq_empty_of_forall_not_mem {s : set X} (H : ∀ x, x ∉ s) : s = ∅ :=
ext (take x, iff.intro
(assume xs, absurd xs (H x))
(assume xe, absurd xe (not_mem_empty x)))
-/
set_option formatter.hide_full_terms false
theorem ne_empty_of_mem {s : set X} {x : X} (H : x ∈ s) : s ≠ ∅ :=
begin intro Hs, rewrite Hs at H, apply not_mem_empty x H end
theorem empty_subset (s : set X) : ∅ ⊆ s :=
take x, assume H, empty.elim H
theorem eq_empty_of_subset_empty {s : set X} (H : s ⊆ ∅) : s = ∅ :=
theorem empty_subset (s : set X) : ∅ ⊆ s :=
take x, assume H, false.elim H
/-theorem eq_empty_of_subset_empty {s : set X} (H : s ⊆ ∅) : s = ∅ :=
subset.antisymm H (empty_subset s)
theorem subset_empty_iff (s : set X) : s ⊆ ∅ ↔ s = ∅ :=
iff.intro eq_empty_of_subset_empty (take xeq, by rewrite xeq; apply subset.refl ∅)
-/
/- universal set -/
@ -81,15 +92,17 @@ theorem empty_ne_univ [h : inhabited X] : (empty : set X) ≠ univ :=
assume H : empty = univ,
absurd (mem_univ (inhabited.value h)) (eq.rec_on H (not_mem_empty (arbitrary X)))
theorem subset_univ (s : set X) : s ⊆ univ := λ x H, unit.star
theorem subset_univ (s : set X) : s ⊆ univ := λ x H, trivial
/-
theorem eq_univ_of_univ_subset {s : set X} (H : univ ⊆ s) : s = univ :=
eq_of_subset_of_subset (subset_univ s) H
-/
/-
theorem eq_univ_of_forall {s : set X} (H : ∀ x, x ∈ s) : s = univ :=
ext (take x, iff.intro (assume H', unit.star) (assume H', H x))
ext (take x, iff.intro (assume H', trivial) (assume H', H x))
-/
/- set-builder notation -/
@ -97,6 +110,10 @@ ext (take x, iff.intro (assume H', unit.star) (assume H', H x))
definition set_of (P : X → Prop) : set X := P
notation `{` binder ` | ` r:(scoped:1 P, set_of P) `}` := r
theorem mem_set_of {P : X → Prop} {a : X} (h : P a) : a ∈ {x | P x} := h
theorem of_mem_set_of {P : X → Prop} {a : X} (h : a ∈ {x | P x}) : P a := h
-- {x ∈ s | P}
definition sep (P : X → Prop) (s : set X) : set X := λx, x ∈ s ∧ P x
notation `{` binder ` ∈ ` s ` | ` r:(scoped:1 p, sep p s) `}` := r
@ -105,8 +122,10 @@ notation `{` binder ` ∈ ` s ` | ` r:(scoped:1 p, sep p s) `}` := r
definition insert (x : X) (a : set X) : set X := {y : X | y = x ∨ y ∈ a}
abbreviation insert_same_level.{u} := @insert.{u u}
-- '{x, y, z}
notation `'{`:max a:(foldr `, ` (x b, insert x b) ∅) `}`:0 := a
notation `'{`:max a:(foldr `, ` (x b, insert_same_level x b) ∅) `}`:0 := a
theorem subset_insert (x : X) (a : set X) : a ⊆ insert x a :=
take y, assume ys, or.inr ys
@ -120,4 +139,48 @@ assume h, or.inr h
theorem eq_or_mem_of_mem_insert {x a : X} {s : set X} : x ∈ insert a s → x = a ∨ x ∈ s :=
assume h, h
/- singleton -/
open trunc_index
theorem mem_singleton_iff {X : Type} [is_set X] (a b : X) : a ∈ '{b} ↔ a = b :=
iff.intro
(assume ainb, or.elim ainb (λ aeqb, aeqb) (λ f, false.elim f))
(assume aeqb, or.inl aeqb)
theorem mem_singleton (a : X) : a ∈ '{a} := !mem_insert
theorem eq_of_mem_singleton {X : Type} [is_set X] {x y : X} (h : x ∈ '{y}) : x = y :=
or.elim (eq_or_mem_of_mem_insert h)
(suppose x = y, this)
(suppose x ∈ ∅, absurd this (not_mem_empty x))
theorem mem_singleton_of_eq {x y : X} (H : x = y) : x ∈ '{y} :=
eq.symm H ▸ mem_singleton y
/-
theorem insert_eq (x : X) (s : set X) : insert x s = '{x} ∪ s :=
ext (take y, iff.intro
(suppose y ∈ insert x s,
or.elim this (suppose y = x, or.inl (or.inl this)) (suppose y ∈ s, or.inr this))
(suppose y ∈ '{x} ∪ s,
or.elim this
(suppose y ∈ '{x}, or.inl (eq_of_mem_singleton this))
(suppose y ∈ s, or.inr this)))
-/
/-
theorem pair_eq_singleton (a : X) : '{a, a} = '{a} :=
by rewrite [insert_eq_of_mem !mem_singleton]
-/
/-
theorem singleton_ne_empty (a : X) : '{a} ≠ ∅ :=
begin
intro H,
apply not_mem_empty a,
rewrite -H,
apply mem_insert
end
-/
end set