From aa191493e98c582d379bb8aed681be2390411110 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sun, 14 Jan 2018 17:58:43 -0800 Subject: [PATCH] give alternative definition of free group on a set with decidable equality --- algebra/free_abelian_group.hlean | 4 +- algebra/free_group.hlean | 343 ++++++++++++++++++++++++++++++- move_to_lib.hlean | 269 +++++++++++++++++++++++- pointed_pi.hlean | 7 + property.hlean | 11 +- 5 files changed, 613 insertions(+), 21 deletions(-) diff --git a/algebra/free_abelian_group.hlean b/algebra/free_abelian_group.hlean index d34fef9..24328ed 100644 --- a/algebra/free_abelian_group.hlean +++ b/algebra/free_abelian_group.hlean @@ -49,7 +49,7 @@ namespace group { reflexivity}, { repeat esimp [map], exact cancel2 x}, { repeat esimp [map], exact cancel1 x}, - { repeat esimp [map], apply rflip}, + { repeat esimp [map], apply fcg_rel.rflip}, { rewrite [+map_append], exact resp_append IH₁ IH₂}, { exact rtrans IH₁ IH₂} end @@ -60,7 +60,7 @@ namespace group { reflexivity}, { repeat esimp [map], exact cancel2 x}, { repeat esimp [map], exact cancel1 x}, - { repeat esimp [map], apply rflip}, + { repeat esimp [map], apply fcg_rel.rflip}, { rewrite [+reverse_append], exact resp_append IH₂ IH₁}, { exact rtrans IH₁ IH₂} end diff --git a/algebra/free_group.hlean b/algebra/free_group.hlean index e8f53c0..e88d58c 100644 --- a/algebra/free_group.hlean +++ b/algebra/free_group.hlean @@ -6,9 +6,12 @@ Authors: Floris van Doorn, Egbert Rijke Constructions with groups -/ -import algebra.group_theory hit.set_quotient types.list types.sum +import algebra.group_theory hit.set_quotient types.list types.sum ..move_to_lib open eq algebra is_trunc set_quotient relation sigma sigma.ops prod sum list trunc function equiv + prod.ops decidable is_equiv + +universe variable u namespace group @@ -157,6 +160,19 @@ namespace group esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul} end + definition free_group_hom_eq [constructor] {φ ψ : free_group X →g G} + (H : Πx, φ (free_group_inclusion x) = ψ (free_group_inclusion x)) : φ ~ ψ := + begin + refine set_quotient.rec_prop _, intro l, + induction l with s l IH, + { exact respect_one φ ⬝ (respect_one ψ)⁻¹ }, + { refine respect_mul φ (class_of [s]) (class_of l) ⬝ _ ⬝ + (respect_mul ψ (class_of [s]) (class_of l))⁻¹, + refine ap011 mul _ IH, induction s with x x, exact H x, + refine respect_inv φ (class_of [inl x]) ⬝ ap inv (H x) ⬝ + (respect_inv ψ (class_of [inl x]))⁻¹ } + end + definition fn_of_free_group_hom [unfold_full] (φ : free_group X →g G) : X → G := φ ∘ free_group_inclusion @@ -167,12 +183,323 @@ 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_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 φ]}} + { intro φ, apply homomorphism_eq, apply free_group_hom_eq, intro x, apply one_mul } end - end group +end group + +/- alternative definition of free group on a set with decidable equality -/ + +namespace list + +variables {X : Type.{u}} {v w : X ⊎ X} {l : list (X ⊎ X)} + +inductive is_reduced {X : Type} : list (X ⊎ X) → Type := +| nil : is_reduced [] +| singleton : Πv, is_reduced [v] +| cons : Π⦃v w l⦄, sum.flip v ≠ w → is_reduced (w::l) → is_reduced (v::w::l) + +definition is_reduced_code (H : is_reduced l) : Type.{u} := +begin + cases l with v l, { exact is_reduced.nil = H }, + cases l with w l, { exact is_reduced.singleton v = H }, + exact Σ(pH : sum.flip v ≠ w × is_reduced (w::l)), is_reduced.cons pH.1 pH.2 = H +end + +definition is_reduced_encode (H : is_reduced l) : is_reduced_code H := +begin + induction H with v v w l p Hl IH, + { exact idp }, + { exact idp }, + { exact ⟨(p, Hl), idp⟩ } +end + +definition is_prop_is_reduced (l : list (X ⊎ X)) : is_prop (is_reduced l) := +begin + apply is_prop.mk, intro H₁ H₂, induction H₁ with v v w l p Hl IH, + { exact is_reduced_encode H₂ }, + { exact is_reduced_encode H₂ }, + { cases is_reduced_encode H₂ with pH' q, cases pH' with p' Hl', esimp at q, + subst q, exact ap011 (λx y, is_reduced.cons x y) !is_prop.elim (IH Hl') } +end + +definition rlist (X : Type) : Type := +Σ(l : list (X ⊎ X)), is_reduced l + +local attribute [instance] is_prop_is_reduced +definition rlist_eq {l l' : rlist X} (p : l.1 = l'.1) : l = l' := +subtype_eq p + +definition is_trunc_rlist {n : ℕ₋₂} {X : Type} (H : is_trunc (n.+2) X) : is_trunc (n.+2) (rlist X) := +begin + apply is_trunc_sigma, { apply is_trunc_list, apply is_trunc_sum }, + intro l, apply is_trunc_succ_of_is_prop +end + +definition is_reduced_invert (v : X ⊎ X) : is_reduced (v::l) → is_reduced l := +begin + assert H : Π⦃l'⦄, is_reduced l' → l' = v::l → is_reduced l, + { intro l' Hl', revert l, induction Hl' with v' v' w' l' p' Hl' IH: intro l p, + { cases p }, + { cases cons_eq_cons p with q r, subst r, apply is_reduced.nil }, + { cases cons_eq_cons p with q r, subst r, exact Hl' }}, + intro Hl, exact H Hl idp +end + +definition rnil [constructor] : rlist X := +⟨[], !is_reduced.nil⟩ + +definition rsingleton [constructor] (x : X ⊎ X) : rlist X := +⟨[x], !is_reduced.singleton⟩ + +definition is_reduced_doubleton [constructor] {x y : X ⊎ X} (p : flip x ≠ y) : + is_reduced [x, y] := +is_reduced.cons p !is_reduced.singleton + +definition rdoubleton [constructor] {x y : X ⊎ X} (p : flip x ≠ y) : rlist X := +⟨[x, y], is_reduced_doubleton p⟩ + +definition is_reduced_concat (Hn : sum.flip v ≠ w) (Hl : is_reduced (concat v l)) : + is_reduced (concat w (concat v l)) := +begin + assert H : Π⦃l'⦄, is_reduced l' → l' = concat v l → is_reduced (concat w l'), + { clear Hl, intro l' Hl', revert l, induction Hl' with v' v' w' l' p' Hl' IH: intro l p, + { exfalso, exact concat_neq_nil _ _ p⁻¹ }, + { cases concat_eq_singleton p⁻¹ with q r, subst q, + exact is_reduced_doubleton Hn }, + { do 2 esimp [concat], apply is_reduced.cons p', cases l with x l, + { cases p }, + { apply IH l, esimp [concat] at p, revert p, generalize concat v l, intro l'' p, + cases cons_eq_cons p with q r, exact r }}}, + exact H Hl idp +end + +definition is_reduced_reverse (H : is_reduced l) : is_reduced (reverse l) := +begin + induction H with v v w l p Hl IH, + { apply is_reduced.nil }, + { apply is_reduced.singleton }, + { refine is_reduced_concat _ IH, intro q, apply p, subst q, apply flip_flip } +end + +definition rreverse [constructor] (l : rlist X) : rlist X := ⟨reverse l.1, is_reduced_reverse l.2⟩ + +definition is_reduced_flip (H : is_reduced l) : is_reduced (map flip l) := +begin + induction H with v v w l p Hl IH, + { apply is_reduced.nil }, + { apply is_reduced.singleton }, + { refine is_reduced.cons _ IH, intro q, apply p, exact !flip_flip⁻¹ ⬝ ap flip q ⬝ !flip_flip } +end + +definition rflip [constructor] (l : rlist X) : rlist X := ⟨map flip l.1, is_reduced_flip l.2⟩ + +definition rcons' [decidable_eq X] (v : X ⊎ X) (l : list (X ⊎ X)) : list (X ⊎ X) := +begin + cases l with w l, + { exact [v] }, + { exact if q : sum.flip v = w then l else v::w::l } +end + +definition is_reduced_rcons [decidable_eq X] (v : X ⊎ X) (Hl : is_reduced l) : + is_reduced (rcons' v l) := +begin + cases l with w l, apply is_reduced.singleton, + apply dite (sum.flip v = w): intro q, + { have is_set (X ⊎ X), from !is_trunc_sum, + rewrite [↑rcons', dite_true q _], exact is_reduced_invert w Hl }, + { rewrite [↑rcons', dite_false q], exact is_reduced.cons q Hl, } +end + +definition rcons [constructor] [decidable_eq X] (v : X ⊎ X) (l : rlist X) : rlist X := +⟨rcons' v l.1, is_reduced_rcons v l.2⟩ + +definition rcons_eq [decidable_eq X] : is_reduced (v::l) → rcons' v l = v :: l := +begin + assert H : Π⦃l'⦄, is_reduced l' → l' = v::l → rcons' v l = l', + { intro l' Hl', revert l, induction Hl' with v' v' w' l' p' Hl' IH: intro l p, + { cases p }, + { cases cons_eq_cons p with q r, subst r, cases p, reflexivity }, + { cases cons_eq_cons p with q r, subst q, subst r, rewrite [↑rcons', dite_false p'], }}, + intro Hl, exact H Hl idp +end + +definition rcons_rcons_eq [decidable_eq X] (p : flip v = w) (l : rlist X) : + rcons v (rcons w l) = l := +begin + have is_set (X ⊎ X), from !is_trunc_sum, + induction l with l Hl, + apply rlist_eq, esimp, + induction l with u l IH, + { exact dite_true p _ }, + { apply dite (sum.flip w = u): intro q, + { rewrite [↑rcons' at {1}, dite_true q _], subst p, induction (!flip_flip⁻¹ ⬝ q), + exact rcons_eq Hl }, + { rewrite [↑rcons', dite_false q, dite_true p _] }} +end + +definition reduce_list' [decidable_eq X] (l : list (X ⊎ X)) : list (X ⊎ X) := +begin + induction l with v l IH, + { exact [] }, + { exact rcons' v IH } +end + +definition is_reduced_reduce_list [decidable_eq X] (l : list (X ⊎ X)) : + is_reduced (reduce_list' l) := +begin + induction l with v l IH, apply is_reduced.nil, + apply is_reduced_rcons, exact IH +end + +definition reduce_list [constructor] [decidable_eq X] (l : list (X ⊎ X)) : rlist X := +⟨reduce_list' l, is_reduced_reduce_list l⟩ + +definition rappend' [decidable_eq X] (l : list (X ⊎ X)) (l' : rlist X) : rlist X := foldr rcons l' l +definition rappend_rcons' [decidable_eq X] (x : X ⊎ X) (l₁ : list (X ⊎ X)) (l₂ : rlist X) : + rappend' (rcons' x l₁) l₂ = rcons x (rappend' l₁ l₂) := +begin + induction l₁ with x' l₁ IH, + { reflexivity }, + { apply dite (sum.flip x = x'): intro p, + { have is_set (X ⊎ X), from !is_trunc_sum, rewrite [↑rcons', dite_true p _], + exact (rcons_rcons_eq p _)⁻¹ }, + { rewrite [↑rcons', dite_false p] }} +end + +definition rappend_cons' [decidable_eq X] (x : X ⊎ X) (l₁ : list (X ⊎ X)) (l₂ : rlist X) : + rappend' (x::l₁) l₂ = rcons x (rappend' l₁ l₂) := +idp + +definition rappend [decidable_eq X] (l l' : rlist X) : rlist X := rappend' l.1 l' + +definition rappend_rcons [decidable_eq X] (x : X ⊎ X) (l₁ l₂ : rlist X) : + rappend (rcons x l₁) l₂ = rcons x (rappend l₁ l₂) := +rappend_rcons' x l₁.1 l₂ + +definition rappend_assoc [decidable_eq X] (l₁ l₂ l₃ : rlist X) : + rappend (rappend l₁ l₂) l₃ = rappend l₁ (rappend l₂ l₃) := +begin + induction l₁ with l₁ h, unfold rappend, clear h, induction l₁ with x l₁ IH, + { reflexivity }, + { rewrite [rappend_cons', ▸*, rappend_rcons', IH] } +end + +definition rappend_rnil [decidable_eq X] (l : rlist X) : rappend l rnil = l := +begin + induction l with l H, apply rlist_eq, esimp, induction H with v v w l p Hl IH, + { reflexivity }, + { reflexivity }, + { rewrite [↑rappend at *, rappend_cons', ↑rcons, IH, ↑rcons', dite_false p] } +end + +definition rnil_rappend [decidable_eq X] (l : rlist X) : rappend rnil l = l := +by reflexivity + +definition rappend_left_inv [decidable_eq X] (l : rlist X) : + rappend (rflip (rreverse l)) l = rnil := +begin + induction l with l H, apply rlist_eq, induction l with x l IH, + { reflexivity }, + { have is_set (X ⊎ X), from !is_trunc_sum, + rewrite [↑rappend, ↑rappend', reverse_cons, map_concat, foldr_concat], + refine ap (λx, (rappend' _ x).1) (rlist_eq (dite_true !flip_flip _)) ⬝ + IH (is_reduced_invert _ H) } +end + + +end list open list + +namespace group + open sigma.ops + + variables (X : Type) [decidable_eq X] {G : Group} + definition group_dfree_group [constructor] : group (rlist X) := + group.mk (is_trunc_rlist _) rappend rappend_assoc rnil rnil_rappend rappend_rnil + (rflip ∘ rreverse) rappend_left_inv + + definition dfree_group [constructor] : Group := + Group.mk _ (group_dfree_group X) + + variable {X} + definition fgh_helper_rcons (f : X → G) (g : G) (x : X ⊎ X) {l : list (X ⊎ X)} : + foldl (fgh_helper f) g (rcons' x l) = foldl (fgh_helper f) g (x :: l) := + begin + cases l with x' l, reflexivity, + apply dite (sum.flip x = x'): intro q, + { have is_set (X ⊎ X), from !is_trunc_sum, + rewrite [↑rcons', dite_true q _, foldl_cons, foldl_cons, -q], + induction x with x, rewrite [↑fgh_helper,mul_inv_cancel_right], + rewrite [↑fgh_helper,inv_mul_cancel_right] }, + { rewrite [↑rcons', dite_false q] } + end + + definition fgh_helper_rappend (f : X → G) (g : G) (l l' : rlist X) : + foldl (fgh_helper f) g (rappend l l').1 = foldl (fgh_helper f) g (l.1 ++ l'.1) := + begin + revert g, induction l with l lH, unfold rappend, clear lH, + induction l with v l IH: intro g, reflexivity, + rewrite [rappend_cons', ↑rcons, fgh_helper_rcons, foldl_cons, IH] + end + + local attribute [instance] is_prop_is_reduced + + -- definition dfree_group_hom' [constructor] {G : InfGroup} (f : X → G) : + -- Σ(f : dfree_group X → G), is_mul_hom f := + -- ⟨λx, foldl (fgh_helper f) 1 x.1, + -- begin intro l₁ l₂, exact !fgh_helper_rappend ⬝ !foldl_append ⬝ !fgh_helper_mul end⟩ + + -- definition dfree_group_hom_eq' [constructor] {φ ψ : dfree_group X →g G} + -- (H : Πx, φ (rsingleton (inl x)) = ψ (rsingleton (inl x))) : φ ~ ψ := + -- begin + -- assert H2 : Πv, φ (rsingleton v) = ψ (rsingleton v), + -- { intro v, induction v with x x, exact H x, + -- exact respect_inv φ _ ⬝ ap inv (H x) ⬝ (respect_inv ψ _)⁻¹ }, + -- intro l, induction l with l Hl, + -- induction Hl with v v w l p Hl IH, + -- { exact respect_one φ ⬝ (respect_one ψ)⁻¹ }, + -- { exact H2 v }, + -- { refine ap φ (rlist_eq (rcons_eq (is_reduced.cons p Hl))⁻¹) ⬝ + -- respect_mul φ (rsingleton v) ⟨_, Hl⟩ ⬝ ap011 mul (H2 v) IH ⬝ _, + -- symmetry, exact ap ψ (rlist_eq (rcons_eq (is_reduced.cons p Hl))⁻¹) ⬝ + -- respect_mul ψ (rsingleton v) ⟨_, Hl⟩ } + -- end + + definition dfree_group_hom [constructor] {G : Group} (f : X → G) : dfree_group X →g G := + homomorphism.mk (λx, foldl (fgh_helper f) 1 x.1) + begin intro l₁ l₂, exact !fgh_helper_rappend ⬝ !foldl_append ⬝ !fgh_helper_mul end + + local attribute [instance] is_prop_is_reduced + + definition dfree_group_hom_eq [constructor] {φ ψ : dfree_group X →g G} + (H : Πx, φ (rsingleton (inl x)) = ψ (rsingleton (inl x))) : φ ~ ψ := + begin + assert H2 : Πv, φ (rsingleton v) = ψ (rsingleton v), + { intro v, induction v with x x, exact H x, + exact respect_inv φ _ ⬝ ap inv (H x) ⬝ (respect_inv ψ _)⁻¹ }, + intro l, induction l with l Hl, + induction Hl with v v w l p Hl IH, + { exact respect_one φ ⬝ (respect_one ψ)⁻¹ }, + { exact H2 v }, + { refine ap φ (rlist_eq (rcons_eq (is_reduced.cons p Hl))⁻¹) ⬝ + respect_mul φ (rsingleton v) ⟨_, Hl⟩ ⬝ ap011 mul (H2 v) IH ⬝ _, + symmetry, exact ap ψ (rlist_eq (rcons_eq (is_reduced.cons p Hl))⁻¹) ⬝ + respect_mul ψ (rsingleton v) ⟨_, Hl⟩ } + end + + variable (X) + + definition free_group_of_dfree_group [constructor] : dfree_group X →g free_group X := + dfree_group_hom free_group_inclusion + + definition dfree_group_of_free_group [constructor] : free_group X →g dfree_group X := + free_group_hom (λx, rsingleton (inl x)) + + definition dfree_group_isomorphism : dfree_group X ≃g free_group X := + begin + apply isomorphism.MK (free_group_of_dfree_group X) (dfree_group_of_free_group X), + { apply free_group_hom_eq, intro x, reflexivity }, + { apply dfree_group_hom_eq, intro x, reflexivity } + end + +end group diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 538ae7e..5bc1dde 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -1,6 +1,6 @@ -- definitions, theorems and attributes which should be moved to files in the HoTT library -import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2 +import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2 algebra.graph open eq nat int susp pointed sigma is_equiv equiv fiber algebra trunc pi group is_trunc function unit prod bool @@ -11,7 +11,7 @@ attribute ap010 [unfold 7] attribute tro_invo_tro [unfold 9] -- TODO: move -- TODO: homotopy_of_eq and apd10 should be the same -- TODO: there is also apd10_eq_of_homotopy in both pi and eq(?) - +universe variable u namespace algebra @@ -24,6 +24,16 @@ end algebra namespace eq + definition pathover_tr_pathover_idp_of_eq {A : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'} {p : a = a'} + (q : b =[p] b') : + pathover_tr p b ⬝o pathover_idp_of_eq (tr_eq_of_pathover q) = q := + begin induction q; reflexivity end + + -- rename pathover_of_tr_eq_idp + definition pathover_of_tr_eq_idp' {A : Type} {B : A → Type} {a a₂ : A} (p : a = a₂) (b : B a) : + pathover_of_tr_eq idp = pathover_tr p b := + by induction p; constructor + definition homotopy.symm_symm {A : Type} {P : A → Type} {f g : Πx, P x} (H : f ~ g) : H⁻¹ʰᵗʸ⁻¹ʰᵗʸ = H := begin apply eq_of_homotopy, intro x, apply inv_inv end @@ -130,6 +140,11 @@ begin apply eq_of_homotopy, intro x, apply inv_inv end homotopy_group_isomorphism_of_pequiv n f ⬝g ghomotopy_group_ptrunc_of_le H B +definition fundamental_group_isomorphism {X : Type*} {G : Group} + (e : Ω X ≃ G) (hom_e : Πp q, e (p ⬝ q) = e p * e q) : π₁ X ≃g G := +isomorphism_of_equiv (trunc_equiv_trunc 0 e ⬝e (trunc_equiv 0 G)) + begin intro p q, induction p with p, induction q with q, exact hom_e p q end + definition equiv_pathover2 {A : Type} {a a' : A} (p : a = a') {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a') (r : to_fun f =[p] to_fun g) : f =[p] g := @@ -545,10 +560,17 @@ namespace lift [H : is_trunc n A] : is_trunc n (plift A) := is_trunc_lift A n + definition lift_functor2 {A B C : Type} (f : A → B → C) (x : lift A) (y : lift B) : lift C := + up (f (down x) (down y)) + end lift namespace trunc open trunc_index + +definition Prop_eq {P Q : Prop} (H : P ↔ Q) : P = Q := +tua (equiv_of_is_prop (iff.mp H) (iff.mpr H)) + definition trunc_index_equiv_nat [constructor] : ℕ₋₂ ≃ ℕ := equiv.MK add_two sub_two add_two_sub_two sub_two_add_two @@ -676,6 +698,19 @@ end is_trunc namespace sigma open sigma.ops +definition eq.rec_sigma {A : Type} {B : A → Type} {a : A} {b : B a} + (P : Π⦃a'⦄ {b' : B a'}, ⟨a, b⟩ = ⟨a', b'⟩ → Type) + (IH : P idp) ⦃a' : A⦄ {b' : B a'} (p : ⟨a, b⟩ = ⟨a', b'⟩) : P p := +begin + apply transport (λp, P p) (to_left_inv !sigma_eq_equiv p), + generalize !sigma_eq_equiv p, esimp, intro q, + induction q with q₁ q₂, induction q₂, exact IH +end + + definition ap_dpair_eq_dpair_pr {A A' : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'} (f : Πa, B a → A') (p : a = a') (q : b =[p] b') + : ap (λx, f x.1 x.2) (dpair_eq_dpair p q) = apd011 f p q := + by induction q; reflexivity + definition sigma_eq_equiv_of_is_prop_right [constructor] {A : Type} {B : A → Type} (u v : Σa, B a) [H : Π a, is_prop (B a)] : u = v ≃ u.1 = v.1 := !sigma_eq_equiv ⬝e !sigma_equiv_of_is_contr_right @@ -762,6 +797,49 @@ by induction q'; reflexivity end sigma open sigma namespace group + +definition isomorphism.MK [constructor] {G H : Group} (φ : G →g H) (ψ : H →g G) + (p : φ ∘g ψ ~ gid H) (q : ψ ∘g φ ~ gid G) : G ≃g H := +isomorphism.mk φ (adjointify φ ψ p q) + +protected definition homomorphism.sigma_char [constructor] + (A B : Group) : (A →g B) ≃ Σ(f : A → B), is_mul_hom f := +begin + fapply equiv.MK, + {intro F, exact ⟨F, _⟩ }, + {intro p, cases p with f H, exact (homomorphism.mk f H) }, + {intro p, cases p, reflexivity }, + {intro F, cases F, reflexivity }, +end + +definition homomorphism_pathover {A : Type} {a a' : A} (p : a = a') + {B : A → Group} {C : A → Group} (f : B a →g C a) (g : B a' →g C a') + (r : homomorphism.φ f =[p] homomorphism.φ g) : f =[p] g := +begin + fapply pathover_of_fn_pathover_fn, + { intro a, apply homomorphism.sigma_char }, + { fapply sigma_pathover, exact r, apply is_prop.elimo } +end + +protected definition isomorphism.sigma_char [constructor] + (A B : Group) : (A ≃g B) ≃ Σ(f : A →g B), is_equiv f := +begin + fapply equiv.MK, + {intro F, exact ⟨F, _⟩ }, + {intro p, cases p with f H, exact (isomorphism.mk f H) }, + {intro p, cases p, reflexivity }, + {intro F, cases F, reflexivity }, +end + +definition isomorphism_pathover {A : Type} {a a' : A} (p : a = a') + {B : A → Group} {C : A → Group} (f : B a ≃g C a) (g : B a' ≃g C a') + (r : pathover (λa, B a → C a) f p g) : f =[p] g := +begin + fapply pathover_of_fn_pathover_fn, + { intro a, apply isomorphism.sigma_char }, + { fapply sigma_pathover, apply homomorphism_pathover, exact r, apply is_prop.elimo } +end + -- definition is_equiv_isomorphism @@ -816,9 +894,10 @@ namespace group end group open group namespace fiber + open pointed sigma - definition is_contr_pfiber_pid (A : Type*) : is_contr (pfiber (pid A)) := - is_contr.mk pt begin intro x, induction x with a p, esimp at p, cases p, reflexivity end +definition is_contr_pfiber_pid (A : Type*) : is_contr (pfiber (pid A)) := +is_contr.mk pt begin intro x, induction x with a p, esimp at p, cases p, reflexivity end definition fiber_functor [constructor] {A A' B B' : Type} {f : A → B} {f' : A' → B'} {b : B} {b' : B'} (g : A → A') (h : B → B') (H : hsquare g h f f') (p : h b = b') (x : fiber f b) : fiber f' b' := @@ -1142,6 +1221,10 @@ namespace sum {f₁₀ : A₀₀ → A₂₀} {f₁₂ : A₀₂ → A₂₂} {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂} {g₁₀ : B₀₀ → B₂₀} {g₁₂ : B₀₂ → B₂₂} {g₀₁ : B₀₀ → B₀₂} {g₂₁ : B₂₀ → B₂₂} {h₀₁ : B₀₀ → A₀₂} {h₂₁ : B₂₀ → A₂₂} + + definition flip_flip (x : A ⊎ B) : flip (flip x) = x := + begin induction x: reflexivity end + definition sum_rec_hsquare [unfold 16] (h : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (k : hsquare g₁₀ f₁₂ h₀₁ h₂₁) : hsquare (f₁₀ +→ g₁₀) f₁₂ (sum.rec f₀₁ h₀₁) (sum.rec f₂₁ h₂₁) := begin intro x, induction x with a b, exact h a, exact k b end @@ -1195,3 +1278,181 @@ namespace equiv end end equiv + + +namespace paths + +variables {A : Type} {R : A → A → Type} {a₁ a₂ a₃ a₄ : A} +inductive all (T : Π⦃a₁ a₂ : A⦄, R a₁ a₂ → Type) : Π⦃a₁ a₂ : A⦄, paths R a₁ a₂ → Type := +| nil {} : Π{a : A}, all T (@nil A R a) +| cons : Π{a₁ a₂ a₃ : A} {r : R a₂ a₃} {p : paths R a₁ a₂}, T r → all T p → all T (cons r p) + +inductive Exists (T : Π⦃a₁ a₂ : A⦄, R a₁ a₂ → Type) : Π⦃a₁ a₂ : A⦄, paths R a₁ a₂ → Type := +| base : Π{a₁ a₂ a₃ : A} {r : R a₂ a₃} (p : paths R a₁ a₂), T r → Exists T (cons r p) +| cons : Π{a₁ a₂ a₃ : A} (r : R a₂ a₃) {p : paths R a₁ a₂}, Exists T p → Exists T (cons r p) + +inductive mem (l : R a₃ a₄) : Π⦃a₁ a₂ : A⦄, paths R a₁ a₂ → Type := +| base : Π{a₂ : A} (p : paths R a₂ a₃), mem l (cons l p) +| cons : Π{a₁ a₂ a₃ : A} (r : R a₂ a₃) {p : paths R a₁ a₂}, mem l p → mem l (cons r p) + +definition len (p : paths R a₁ a₂) : ℕ := +begin + induction p with a a₁ a₂ a₃ r p IH, + { exact 0 }, + { exact nat.succ IH } +end + +definition mem_equiv_Exists (l : R a₁ a₂) (p : paths R a₃ a₄) : + mem l p ≃ Exists (λa a' r, ⟨a₁, a₂, l⟩ = ⟨a, a', r⟩) p := +sorry + +end paths + +namespace list +open is_trunc trunc sigma.ops prod.ops lift +variables {A B X : Type} + +definition foldl_homotopy {f g : A → B → A} (h : f ~2 g) (a : A) : foldl f a ~ foldl g a := +begin + intro bs, revert a, induction bs with b bs p: intro a, reflexivity, esimp [foldl], + exact p (f a b) ⬝ ap010 (foldl g) (h a b) bs +end + +definition cons_eq_cons {x x' : X} {l l' : list X} (p : x::l = x'::l') : x = x' × l = l' := +begin + refine lift.down (list.no_confusion p _), intro q r, split, exact q, exact r +end + +definition concat_neq_nil (x : X) (l : list X) : concat x l ≠ nil := +begin + intro p, cases l: cases p, +end + +definition concat_eq_singleton {x x' : X} {l : list X} (p : concat x l = [x']) : + x = x' × l = [] := +begin + cases l with x₂ l, + { cases cons_eq_cons p with q r, subst q, split: reflexivity }, + { exfalso, esimp [concat] at p, apply concat_neq_nil x l, revert p, generalize (concat x l), + intro l' p, cases cons_eq_cons p with q r, exact r } +end + +definition foldr_concat (f : A → B → B) (b : B) (a : A) (l : list A) : + foldr f b (concat a l) = foldr f (f a b) l := +begin + induction l with a' l p, reflexivity, rewrite [concat_cons, foldr_cons, p] +end + +definition iterated_prod (X : Type.{u}) (n : ℕ) : Type.{u} := +iterate (prod X) n (lift unit) + +definition is_trunc_iterated_prod {k : ℕ₋₂} {X : Type} {n : ℕ} (H : is_trunc k X) : + is_trunc k (iterated_prod X n) := +begin + induction n with n IH, + { apply is_trunc_of_is_contr, apply is_trunc_lift }, + { exact @is_trunc_prod _ _ _ H IH } +end + +definition list_of_iterated_prod {n : ℕ} (x : iterated_prod X n) : list X := +begin + induction n with n IH, + { exact [] }, + { exact x.1::IH x.2 } +end + +definition list_of_iterated_prod_succ {n : ℕ} (x : X) (xs : iterated_prod X n) : + @list_of_iterated_prod X (succ n) (x, xs) = x::list_of_iterated_prod xs := +by reflexivity + +definition iterated_prod_of_list (l : list X) : Σn, iterated_prod X n := +begin + induction l with x l IH, + { exact ⟨0, up ⋆⟩ }, + { exact ⟨succ IH.1, (x, IH.2)⟩ } +end + +definition iterated_prod_of_list_cons (x : X) (l : list X) : + iterated_prod_of_list (x::l) = + ⟨succ (iterated_prod_of_list l).1, (x, (iterated_prod_of_list l).2)⟩ := +by reflexivity + +protected definition sigma_char [constructor] (X : Type) : list X ≃ Σ(n : ℕ), iterated_prod X n := +begin + apply equiv.MK iterated_prod_of_list (λv, list_of_iterated_prod v.2), + { intro x, induction x with n x, esimp, induction n with n IH, + { induction x with x, induction x, reflexivity }, + { revert x, change Π(x : X × iterated_prod X n), _, intro xs, cases xs with x xs, + rewrite [list_of_iterated_prod_succ, iterated_prod_of_list_cons], + apply sigma_eq (ap succ (IH xs)..1), + apply pathover_ap, refine prod_pathover _ _ _ _ (IH xs)..2, + apply pathover_of_eq, reflexivity }}, + { intro l, induction l with x l IH, + { reflexivity }, + { exact ap011 cons idp IH }} +end + +local attribute [instance] is_trunc_iterated_prod +definition is_trunc_list [instance] {n : ℕ₋₂} {X : Type} (H : is_trunc (n.+2) X) : + is_trunc (n.+2) (list X) := +begin + assert H : is_trunc (n.+2) (Σ(k : ℕ), iterated_prod X k), + { apply is_trunc_sigma, apply is_trunc_succ_succ_of_is_set, + intro, exact is_trunc_iterated_prod H }, + apply is_trunc_equiv_closed_rev _ (list.sigma_char X), +end + +end list + +/- namespace logic? -/ +namespace decidable +definition double_neg_elim {A : Type} (H : decidable A) (p : ¬ ¬ A) : A := +begin induction H, assumption, contradiction end + + +definition dite_true {C : Type} [H : decidable C] {A : Type} + {t : C → A} {e : ¬ C → A} (c : C) (H' : is_prop C) : dite C t e = t c := +begin + induction H with H H, + exact ap t !is_prop.elim, + contradiction +end + +definition dite_false {C : Type} [H : decidable C] {A : Type} + {t : C → A} {e : ¬ C → A} (c : ¬ C) : dite C t e = e c := +begin + induction H with H H, + contradiction, + exact ap e !is_prop.elim, +end + +definition decidable_eq_of_is_prop (A : Type) [is_prop A] : decidable_eq A := +λa a', decidable.inl !is_prop.elim + +definition decidable_eq_sigma [instance] {A : Type} (B : A → Type) [HA : decidable_eq A] + [HB : Πa, decidable_eq (B a)] : decidable_eq (Σa, B a) := +begin + intro v v', induction v with a b, induction v' with a' b', + cases HA a a' with p np, + { induction p, cases HB a b b' with q nq, + induction q, exact decidable.inl idp, + apply decidable.inr, intro p, apply nq, apply @eq_of_pathover_idp A B, + exact change_path !is_prop.elim p..2 }, + { apply decidable.inr, intro p, apply np, exact p..1 } +end + +open sum +definition decidable_eq_sum [instance] (A B : Type) [HA : decidable_eq A] [HB : decidable_eq B] : + decidable_eq (A ⊎ B) := +begin + intro v v', induction v with a b: induction v' with a' b', + { cases HA a a' with p np, + { exact decidable.inl (ap sum.inl p) }, + { apply decidable.inr, intro p, cases p, apply np, reflexivity }}, + { apply decidable.inr, intro p, cases p }, + { apply decidable.inr, intro p, cases p }, + { cases HB b b' with p np, + { exact decidable.inl (ap sum.inr p) }, + { apply decidable.inr, intro p, cases p, apply np, reflexivity }}, +end +end decidable diff --git a/pointed_pi.hlean b/pointed_pi.hlean index 05fe709..26aee60 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -599,6 +599,13 @@ namespace pointed pfiber f ≃* psigma_gen (λa, f a = pt) (respect_pt f) := pequiv_of_equiv (fiber.sigma_char f pt) idp + definition fiberpt [constructor] {A B : Type*} {f : A →* B} : fiber f pt := + fiber.mk pt (respect_pt f) + + definition psigma_fiber_pequiv [constructor] {A B : Type*} (f : A →* B) : + psigma_gen (fiber f) fiberpt ≃* A := + pequiv_of_equiv (sigma_fiber_equiv f) idp + definition ppmap.sigma_char [constructor] (A B : Type*) : ppmap A B ≃* @psigma_gen (A →ᵘ* B) (λf, f pt = pt) idp := pequiv_of_equiv pmap.sigma_char idp diff --git a/property.hlean b/property.hlean index 65213a1..3477e2c 100644 --- a/property.hlean +++ b/property.hlean @@ -3,7 +3,7 @@ Copyright (c) 2017 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad -/ -import types.trunc .logic +import types.trunc .logic .move_to_lib open funext eq trunc is_trunc logic definition property (X : Type) := X → Prop @@ -18,9 +18,8 @@ definition mem (x : X) (a : property X) := a x infix ∈ := mem notation a ∉ b := ¬ mem a b -/-theorem ext {a b : property X} (H : ∀x, x ∈ a ↔ x ∈ b) : a = b := -eq_of_homotopy (take x, propext (H x)) --/ +theorem ext {X : Type} {a b : property X} (H : ∀x, x ∈ a ↔ x ∈ b) : a = b := +eq_of_homotopy (take x, Prop_eq (H x)) definition subproperty (a b : property X) : Prop := Prop.mk (∀⦃x⦄, x ∈ a → x ∈ b) _ infix ⊆ := subproperty @@ -33,10 +32,8 @@ theorem subproperty.refl (a : property X) : a ⊆ a := take x, assume H, H theorem subproperty.trans {a b c : property X} (subab : a ⊆ b) (subbc : b ⊆ c) : a ⊆ c := take x, assume ax, subbc (subab ax) -/- -theorem subproperty.antisymm {a b : property X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b := +theorem subproperty.antisymm {X : Type} {a b : property X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b := ext (λ x, iff.intro (λ ina, h₁ ina) (λ inb, h₂ inb)) --/ -- an alterantive name /-