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

update after renamings in the HoTT library

Browse source
This commit is contained in:
Floris van Doorn 2016-02-17 15:36:31 -05:00
parent 5c9355c4c1
commit b7f2b9d689
3 changed files with 44 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
group_theory/basic.hlean
View file

@ -21,11 +21,11 @@ set_option class.force_new true
namespace group
definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one
definition Pointed_of_Group (G : Group) : Type* := pointed.mk' G
definition hset_of_Group (G : Group) : hset := trunctype.mk G _
definition pType_of_Group (G : Group) : Type* := pointed.mk' G
definition Set_of_Group (G : Group) : Set := trunctype.mk G _
-- print Type*
-- print Pointed
-- print pType
definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group :=
Group.mk G _
@ -57,7 +57,7 @@ namespace group
theorem respect_inv (φ : G₁ →g G₂) (g : G₁) : φ g⁻¹ = (φ g)⁻¹ :=
eq_inv_of_mul_eq_one (!respect_mul⁻¹ ⬝ ap φ !mul.left_inv ⬝ !respect_one)
definition is_hset_homomorphism [instance] (G₁ G₂ : Group) : is_hset (homomorphism G₁ G₂) :=
definition is_set_homomorphism [instance] (G₁ G₂ : Group) : is_set (homomorphism G₁ G₂) :=
begin
assert H : G₁ →g G₂ ≃ Σ(f : G₁ → G₂), Π(g₁ g₂ : G₁), f (g₁ * g₂) = f g₁ * f g₂,
{ fapply equiv.MK,
@ -69,13 +69,13 @@ namespace group
end
definition pmap_of_homomorphism [constructor] (φ : G₁ →g G₂)
: Pointed_of_Group G₁ →* Pointed_of_Group G₂ :=
: pType_of_Group G₁ →* pType_of_Group G₂ :=
pmap.mk φ !respect_one
definition homomorphism_eq (p : group_fun φ ~ group_fun φ') : φ = φ' :=
begin
induction φ with φ q, induction φ' with φ' q', esimp at p, induction p,
exact ap (homomorphism.mk φ) !is_hprop.elim
exact ap (homomorphism.mk φ) !is_prop.elim
end
/- categorical structure of groups + homomorphisms -/

68
group_theory/constructions.hlean
View file

@ -15,7 +15,7 @@ namespace group
/- Subgroups -/
structure subgroup_rel (G : Group) :=
(R : G → hprop)
(R : G → Prop)
(Rone : R one)
(Rmul : Π{g h}, R g → R h → R (g * h))
(Rinv : Π{g}, R g → R (g⁻¹))
@ -55,7 +55,7 @@ namespace group
... = g * (k * h) : by rewrite [mul_inv_cancel_left],
show N (g * (k * h)), from H2 ▸ H1
-- this is just (Σ(g : G), H g), but only defined if (H g) is an hprop
-- this is just (Σ(g : G), H g), but only defined if (H g) is a prop
definition sg : Type := {g : G | H g}
local attribute sg [reducible]
variable {H}
@ -106,7 +106,7 @@ namespace group
/- Quotient Group -/
definition quotient_rel (g h : G) : hprop := N (g * h⁻¹)
definition quotient_rel (g h : G) : Prop := N (g * h⁻¹)
variable {N}
theorem quotient_rel_refl (g : G) : quotient_rel N g g :=
@ -165,36 +165,36 @@ namespace group
theorem quotient_mul_assoc (g₁ g₂ g₃ : qg N) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
begin
refine set_quotient.rec_hprop _ g₁,
refine set_quotient.rec_hprop _ g₂,
refine set_quotient.rec_hprop _ g₃,
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_hprop _ g, clear g, intro g,
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_hprop _ g, clear g, intro g,
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_hprop _ g, clear g, intro g,
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_hprop _ g, clear g, intro g,
refine set_quotient.rec_hprop _ h, clear h, intro h,
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
@ -262,7 +262,7 @@ namespace group
infix ` ×g `:30 := group.product
/- Free Group of a set -/
variables (X : hset) {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 :=
@ -320,28 +320,28 @@ namespace group
theorem free_group_mul_assoc (g₁ g₂ g₃ : FG X) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
begin
refine set_quotient.rec_hprop _ g₁,
refine set_quotient.rec_hprop _ g₂,
refine set_quotient.rec_hprop _ g₃,
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_hprop _ g, clear g, intro g,
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_hprop _ g, clear g, intro g,
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_hprop _ g, clear g, intro g,
refine set_quotient.rec_prop _ g, clear g, intro g,
apply eq_of_rel, apply tr,
induction g with s l IH,
{ reflexivity},
@ -400,7 +400,7 @@ namespace group
{ 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_hprop _, intro l, refine set_quotient.rec_hprop _, intro l',
{ refine set_quotient.rec_prop _, intro l, refine set_quotient.rec_prop _, intro l',
esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul}
end
@ -414,7 +414,7 @@ namespace group
{ 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_hprop _, intro l, esimp,
{ 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],
@ -493,28 +493,28 @@ namespace group
theorem fcg_mul_assoc (g₁ g₂ g₃ : FG X) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
begin
refine set_quotient.rec_hprop _ g₁,
refine set_quotient.rec_hprop _ g₂,
refine set_quotient.rec_hprop _ g₃,
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_hprop _ g, clear g, intro g,
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_hprop _ g, clear g, intro g,
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_hprop _ g, clear g, intro g,
refine set_quotient.rec_prop _ g, clear g, intro g,
apply eq_of_rel, apply tr,
induction g with s l IH,
{ reflexivity},
@ -529,8 +529,8 @@ namespace group
theorem fcg_mul_comm (g h : FG X) : g * h = h * g :=
begin
refine set_quotient.rec_hprop _ g, clear g, intro g,
refine set_quotient.rec_hprop _ h, clear h, intro h,
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]},
@ -573,7 +573,7 @@ namespace group
{ 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_hprop _, intro l, refine set_quotient.rec_hprop _, intro l',
{ refine set_quotient.rec_prop _, intro l, refine set_quotient.rec_prop _, intro l',
esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul}
end
@ -587,7 +587,7 @@ namespace group
{ 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_hprop _, intro l, esimp,
{ 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],
@ -602,17 +602,17 @@ namespace group
variables {A B}
local abbreviation ι := @free_comm_group_inclusion
inductive tensor_rel_type : free_comm_group (hset_of_Group A ×t hset_of_Group B) → Type :=
inductive tensor_rel_type : free_comm_group (Set_of_Group A ×t Set_of_Group B) → Type :=
| mul_left : Π(a₁ a₂ : A) (b : B), tensor_rel_type (ι (a₁, b) * ι (a₂, b) * (ι (a₁ * a₂, b))⁻¹)
| mul_right : Π(a : A) (b₁ b₂ : B), tensor_rel_type (ι (a, b₁) * ι (a, b₂) * (ι (a, b₁ * b₂))⁻¹)
open tensor_rel_type
definition tensor_rel' (x : free_comm_group (hset_of_Group A ×t hset_of_Group B)) : hprop :=
definition tensor_rel' (x : free_comm_group (Set_of_Group A ×t Set_of_Group B)) : Prop :=
∥ tensor_rel_type x ∥
definition tensor_group_rel (A B : CommGroup)
: normal_subgroup_rel (free_comm_group (hset_of_Group A ×t hset_of_Group B)) :=
: normal_subgroup_rel (free_comm_group (Set_of_Group A ×t Set_of_Group B)) :=
sorry /- relation generated by tensor_rel'-/
definition tensor_group [constructor] : CommGroup :=
@ -625,7 +625,7 @@ namespace group
variables {G₁ G₂ : Group}
-- TODO: maybe define this in more generality for pointed types?
definition kernel [constructor] (φ : G₁ →g G₂) (g : G₁) : hprop := trunctype.mk (φ g = 1) _
definition kernel [constructor] (φ : G₁ →g G₂) (g : G₁) : Prop := trunctype.mk (φ g = 1) _
theorem kernel_mul (φ : G₁ →g G₂) (g h : G₁) (H₁ : kernel φ g) (H₂ : kernel φ h) : kernel φ (g *[G₁] h) :=
begin

8
homotopy/sample.hlean
View file

@ -71,7 +71,7 @@ namespace homotopy
begin
intro b,
apply is_contr.mk (@is_retraction.sect _ _ _ s (λa, tr (fiber.mk a idp)) b),
apply trunc.rec, apply fiber.rec, intros a p,
esimp, apply trunc.rec, apply fiber.rec, intros a p,
apply transport
(λz : (Σy, h a = y), @sect _ _ _ s (λa, tr (mk a idp)) (sigma.pr1 z) =
tr (fiber.mk a (sigma.pr2 z)))
@ -118,7 +118,7 @@ namespace homotopy
: is_surjective f → is_conn_map -1 f :=
begin
intro H, intro b,
exact @is_contr_of_inhabited_hprop (∥fiber f b∥) (is_trunc_trunc -1 (fiber f b)) (H b),
exact @is_contr_of_inhabited_prop (∥fiber f b∥) (is_trunc_trunc -1 (fiber f b)) (H b),
end
definition is_surjection_of_minus_one_conn {A B : Type} (f : A → B)
@ -132,7 +132,7 @@ namespace homotopy
λH, @center (∥A∥) H
definition minus_one_conn_of_merely {A : Type} : ∥A∥ → is_conn -1 A :=
@is_contr_of_inhabited_hprop (∥A∥) (is_trunc_trunc -1 A)
@is_contr_of_inhabited_prop (∥A∥) (is_trunc_trunc -1 A)
section
open arrow
@ -177,7 +177,7 @@ namespace homotopy
apply pathover_of_tr_eq,
rewrite [transport_eq_Fr,idp_con],
revert H, induction n with [n, IH],
{ intro H, apply is_hprop.elim },
{ intro H, apply is_prop.elim },
{ intros H,
change ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid a'),
generalize a',