diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean index 33e1833..77c1dc4 100644 --- a/algebra/arrow_group.hlean +++ b/algebra/arrow_group.hlean @@ -19,35 +19,37 @@ namespace group definition ppi_inv [constructor] {A : Type*} {B : A → Type*} (f : Π*a, Ω (B a)) : Π*a, Ω (B a) := proof ppi.mk (λa, (f a)⁻¹ᵖ) (respect_pt f)⁻² qed - definition inf_group_ppi [constructor] [instance] {A : Type*} (B : A → Type*) : - inf_group (Π*a, Ω (B a)) := + definition inf_pgroup_pppi [constructor] {A : Type*} (B : A → Type*) : + inf_pgroup (Π*a, Ω (B a)) := begin - fapply inf_group.mk, + fapply inf_pgroup.mk, { exact ppi_mul }, { intro f g h, apply eq_of_phomotopy, fapply phomotopy.mk, { intro a, exact con.assoc (f a) (g a) (h a) }, { symmetry, rexact eq_of_square (con2_assoc (respect_pt f) (respect_pt g) (respect_pt h)) }}, - { apply ppi_const }, + { exact ppi_inv }, { intros f, apply eq_of_phomotopy, fapply phomotopy.mk, { intro a, exact one_mul (f a) }, { symmetry, apply eq_of_square, refine _ ⬝vp !ap_id, apply natural_square_tr }}, { intros f, apply eq_of_phomotopy, fapply phomotopy.mk, { intro a, exact mul_one (f a) }, { reflexivity }}, - { exact ppi_inv }, { intro f, apply eq_of_phomotopy, fapply phomotopy.mk, { intro a, exact con.left_inv (f a) }, { exact !con_left_inv_idp }}, end - definition group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) : - group (trunc 0 (Π*a, Ω (B a))) := - !trunc_group + definition inf_group_ppi [constructor] {A : Type*} (B : A → Type*) : + inf_group (Π*a, Ω (B a)) := + @inf_group_of_inf_pgroup _ (inf_pgroup_pppi B) + + definition gppi_loop [constructor] {A : Type*} (B : A → Type*) : InfGroup := + InfGroup.mk (Π*a, Ω (B a)) (inf_group_ppi B) definition Group_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : Group := - Group.mk (trunc 0 (Π*a, Ω (B a))) _ + gtrunc (gppi_loop B) - definition ab_inf_group_ppi [constructor] [instance] {A : Type*} (B : A → Type*) : + definition ab_inf_group_ppi [constructor] {A : Type*} (B : A → Type*) : ab_inf_group (Π*a, Ω (Ω (B a))) := ⦃ab_inf_group, inf_group_ppi (λa, Ω (B a)), mul_comm := begin @@ -56,23 +58,20 @@ namespace group { symmetry, rexact eq_of_square (eckmann_hilton_con2 (respect_pt f) (respect_pt g)) } end⦄ - definition ab_group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) : - ab_group (trunc 0 (Π*a, Ω (Ω (B a)))) := - !trunc_ab_group + definition agppi_loop [constructor] {A : Type*} (B : A → Type*) : AbInfGroup := + AbInfGroup.mk (Π*a, Ω (Ω (B a))) (ab_inf_group_ppi B) definition AbGroup_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : AbGroup := - AbGroup.mk (trunc 0 (Π*a, Ω (Ω (B a)))) _ + agtrunc (agppi_loop B) - definition trunc_ppi_isomorphic_pmap (A B : Type*) - : Group.mk (trunc 0 (Π*(a : A), Ω B)) !trunc_group - ≃g Group.mk (trunc 0 (A →* Ω B)) !trunc_group := - begin - reflexivity, - -- apply trunc_isomorphism_of_equiv (pppi_equiv_pmap A (Ω B)), - -- intro h k, induction h with h h_pt, induction k with k k_pt, reflexivity - end - - section + -- definition trunc_ppi_isomorphic_pmap (A B : Type*) + -- : Group.mk (trunc 0 (Π*(a : A), Ω B)) !group_trunc + -- ≃g Group.mk (trunc 0 (A →* Ω B)) !group_trunc := + -- begin + -- reflexivity, + -- -- apply trunc_isomorphism_of_equiv (pppi_equiv_pmap A (Ω B)), + -- -- intro h k, induction h with h h_pt, induction k with k k_pt, reflexivity + -- end universe variables u v @@ -101,23 +100,22 @@ namespace group variable (k) - definition trunc_ppi_loop_isomorphism_lemma - : isomorphism.{(max u v) (max u v)} - (Group.mk (trunc 0 (k = k)) (@trunc_group (k = k) !inf_group_loop)) - (Group.mk (trunc 0 (Π*(a : A), Ω (pType.mk (B a) (k a)))) !trunc_group) := + definition gloop_ppi_isomorphism : + Ωg (pointed.Mk k) ≃∞g gppi_loop (λ a, pointed.Mk (ppi.to_fun k a)) := begin - apply @trunc_isomorphism_of_equiv _ _ !inf_group_loop !inf_group_ppi (ppi_loop_equiv k), + apply inf_isomorphism_of_equiv (ppi_loop_equiv k), intro f g, induction k with k p, induction p, apply trans (phomotopy_of_eq_homomorphism f g), exact ppi_mul_loop (phomotopy_of_eq f) (phomotopy_of_eq g) end - end + definition trunc_ppi_loop_isomorphism_lemma : + gtrunc (gloop (pointed.Mk k)) ≃g gtrunc (gppi_loop (λa, pointed.Mk (k a))) := + gtrunc_isomorphism_gtrunc (gloop_ppi_isomorphism k) - definition trunc_ppi_loop_isomorphism {A : Type*} (B : A → Type*) - : Group.mk (trunc 0 (Ω (Π*(a : A), B a))) !trunc_group - ≃g Group.mk (trunc 0 (Π*(a : A), Ω (B a))) !trunc_group := - trunc_ppi_loop_isomorphism_lemma (ppi_const B) + definition trunc_ppi_loop_isomorphism {A : Type*} (B : A → Type*) : + gtrunc (gloop (Π*(a : A), B a)) ≃g gtrunc (gppi_loop B) := + proof trunc_ppi_loop_isomorphism_lemma (ppi_const B) qed /- We first define the group structure on A →* Ω B (except for truncatedness). @@ -171,21 +169,24 @@ namespace group loop_susp_intro (pmap_mul f g) ~* pmap_mul (loop_susp_intro f) (loop_susp_intro g) := pwhisker_right _ !ap1_pmap_mul ⬝* !pmap_mul_pcompose - definition inf_group_pmap [constructor] [instance] (A B : Type*) : inf_group (A →* Ω B) := - !inf_group_ppi + definition InfGroup_pmap [reducible] [constructor] (A B : Type*) : InfGroup := + InfGroup.mk (A →* Ω B) !inf_group_ppi - definition group_trunc_pmap [constructor] [instance] (A B : Type*) : group (trunc 0 (A →* Ω B)) := - !trunc_group + definition InfGroup_pmap' [reducible] [constructor] (A : Type*) {B C : Type*} (e : Ω C ≃* B) : + InfGroup := + InfGroup.mk (A →* B) + (@inf_group_of_inf_pgroup _ (inf_pgroup_pequiv_closed (ppmap_pequiv_ppmap_right e) + !inf_pgroup_pppi)) definition Group_trunc_pmap [reducible] [constructor] (A B : Type*) : Group := - Group.mk (trunc 0 (A →* Ω B)) _ + Group.mk (trunc 0 (A →* Ω B)) (@group_trunc _ !inf_group_ppi) definition Group_trunc_pmap_homomorphism [constructor] {A A' B : Type*} (f : A' →* A) : Group_trunc_pmap A B →g Group_trunc_pmap A' B := begin fapply homomorphism.mk, { apply trunc_functor, intro g, exact g ∘* f}, - { intro g h, induction g with g, induction h with h, apply ap tr, + { intro g h, induction g with g, esimp, induction h with h, apply ap tr, apply eq_of_phomotopy, fapply phomotopy.mk, { intro a, reflexivity }, { symmetry, refine _ ⬝ !idp_con⁻¹, @@ -242,16 +243,11 @@ namespace group definition ab_inf_group_pmap [constructor] [instance] (A B : Type*) : ab_inf_group (A →* Ω (Ω B)) := - ⦃ab_inf_group, inf_group_pmap A (Ω B), mul_comm := - begin - intro f g, apply eq_of_phomotopy, fapply phomotopy.mk, - { intro a, exact eckmann_hilton (f a) (g a) }, - { symmetry, rexact eq_of_square (eckmann_hilton_con2 (respect_pt f) (respect_pt g)) } - end⦄ + !ab_inf_group_ppi definition ab_group_trunc_pmap [constructor] [instance] (A B : Type*) : ab_group (trunc 0 (A →* Ω (Ω B))) := - !trunc_ab_group + !ab_group_trunc definition AbGroup_trunc_pmap [reducible] [constructor] (A B : Type*) : AbGroup := AbGroup.mk (trunc 0 (A →* Ω (Ω B))) _ diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index db33e93..d0b56de 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -165,13 +165,13 @@ namespace group fapply is_equiv.adjointify, exact dirsum_functor (λ i, (f i)⁻¹ᵍ), { intro ds, - refine (homomorphism_comp_compute (dirsum_functor (λ i, f i)) (dirsum_functor (λ i, (f i)⁻¹ᵍ)) _)⁻¹ ⬝ _, + refine (homomorphism_compose_eq (dirsum_functor (λ i, f i)) (dirsum_functor (λ i, (f i)⁻¹ᵍ)) _)⁻¹ ⬝ _, refine dirsum_functor_compose (λ i, f i) (λ i, (f i)⁻¹ᵍ) ds ⬝ _, refine dirsum_functor_homotopy _ (λ i, !gid) (λ i, to_right_inv (equiv_of_isomorphism (f i))) ds ⬝ _, exact !dirsum_functor_gid }, { intro ds, - refine (homomorphism_comp_compute (dirsum_functor (λ i, (f i)⁻¹ᵍ)) (dirsum_functor (λ i, f i)) _)⁻¹ ⬝ _, + refine (homomorphism_compose_eq (dirsum_functor (λ i, (f i)⁻¹ᵍ)) (dirsum_functor (λ i, f i)) _)⁻¹ ⬝ _, refine dirsum_functor_compose (λ i, (f i)⁻¹ᵍ) (λ i, f i) ds ⬝ _, refine dirsum_functor_homotopy _ (λ i, !gid) (λ i x, proof @@ -197,19 +197,19 @@ namespace group fapply adjointify, { exact from_hom }, { intro ds, - refine (homomorphism_comp_compute to_hom from_hom ds)⁻¹ ⬝ _, + refine (homomorphism_compose_eq to_hom from_hom ds)⁻¹ ⬝ _, refine @dirsum_homotopy I _ Y (dirsum Y) (to_hom ∘g from_hom) !gid _ ds, intro i y, - refine homomorphism_comp_compute to_hom from_hom _ ⬝ _, + refine homomorphism_compose_eq to_hom from_hom _ ⬝ _, refine ap to_hom (dirsum_elim_compute (λi, dirsum_incl (Y ∘ down.{u v}) (up.{u v} i)) i y) ⬝ _, refine dirsum_elim_compute _ (up.{u v} i) y ⬝ _, reflexivity }, { intro ds, - refine (homomorphism_comp_compute from_hom to_hom ds)⁻¹ ⬝ _, + refine (homomorphism_compose_eq from_hom to_hom ds)⁻¹ ⬝ _, refine @dirsum_homotopy _ _ (Y ∘ down.{u v}) (dirsum (Y ∘ down.{u v})) (from_hom ∘g to_hom) !gid _ ds, intro i y, induction i with i, - refine homomorphism_comp_compute from_hom to_hom _ ⬝ _, + refine homomorphism_compose_eq from_hom to_hom _ ⬝ _, refine ap from_hom (dirsum_elim_compute (λi, dirsum_incl Y (down.{u v} i)) (up.{u v} i) y) ⬝ _, refine dirsum_elim_compute _ i y ⬝ _, reflexivity diff --git a/algebra/free_group.hlean b/algebra/free_group.hlean index 2b75cb6..bf6717b 100644 --- a/algebra/free_group.hlean +++ b/algebra/free_group.hlean @@ -234,7 +234,7 @@ 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 + intro l, exact is_trunc_succ_of_is_prop _ _ _ end definition is_reduced_invert (v : X ⊎ X) : is_reduced (v::l) → is_reduced l := diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean index e9b49d4..9ed0444 100644 --- a/algebra/left_module.hlean +++ b/algebra/left_module.hlean @@ -367,7 +367,7 @@ end isomorphism.mk (to_lminv φ) !is_equiv_inv definition isomorphism.trans [trans] [constructor] (φ : M₁ ≃lm M₂) (ψ : M₂ ≃lm M₃) : M₁ ≃lm M₃ := - isomorphism.mk (ψ ∘lm φ) !is_equiv_compose + isomorphism.mk (ψ ∘lm φ) (is_equiv_compose ψ φ _ _) definition isomorphism.eq_trans [trans] [constructor] {M₁ M₂ : LeftModule R} {M₃ : LeftModule R} (φ : M₁ = M₂) (ψ : M₂ ≃lm M₃) : M₁ ≃lm M₃ := diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean index fd8c2fe..6e1d966 100644 --- a/algebra/product_group.hlean +++ b/algebra/product_group.hlean @@ -72,7 +72,7 @@ namespace group φ (x.1 * y.1) * ψ (x.2 * y.2) = (φ x.1 * φ y.1) * (ψ x.2 * ψ y.2) : by exact ap011 mul (to_respect_mul φ x.1 y.1) (to_respect_mul ψ x.2 y.2) ... = (φ x.1 * ψ x.2) * (φ y.1 * ψ y.2) - : by exact interchange I (φ x.1) (φ y.1) (ψ x.2) (ψ y.2)) end + : by exact mul.comm4 (φ x.1) (φ y.1) (ψ x.2) (ψ y.2)) end definition product_functor [constructor] {G G' H H' : Group} (φ : G →g H) (ψ : G' →g H') : G ×g G' →g H ×g H' := diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index 3acc798..bdc433d 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -331,7 +331,7 @@ namespace group have htpy : Π (a : A), K a ≃ L a, begin intro a, - apply @equiv_of_is_prop (a ∈ K) (a ∈ L) _ _ (K_in_L a) (L_in_K a), + exact @equiv_of_is_prop (a ∈ K) (a ∈ L) (K_in_L a) (L_in_K a) _ _, end, exact subgroup_rel_eq' htpy, end @@ -561,11 +561,12 @@ definition ab_group_kernel_quotient_to_image_codomain_triangle {A B : AbGroup} ( fapply is_prop.elimo end +-- set_option pp.all true +-- print algebra._trans_of_Group_of_AbGroup_2 definition is_surjective_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) : is_surjective (ab_group_kernel_quotient_to_image f) := begin - fapply is_surjective_factor (group_fun (ab_qg_map (kernel f))), - exact image_lift f, + refine is_surjective_factor (ab_qg_map (kernel f)) (image_lift f) _ _, apply @quotient_group_compute _ _ _ (@is_normal_subgroup_ab _ (kernel f) _), exact is_surjective_image_lift f end @@ -573,7 +574,7 @@ definition is_surjective_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) definition is_embedding_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) : is_embedding (ab_group_kernel_quotient_to_image f) := begin - fapply is_embedding_factor (ab_group_kernel_quotient_to_image f) (image_incl f) (kernel_quotient_extension f), + fapply is_embedding_factor (image_incl f) (kernel_quotient_extension f), exact ab_group_kernel_quotient_to_image_codomain_triangle f, exact is_embedding_kernel_quotient_extension f end diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean index 279feed..feaaaea 100644 --- a/algebra/submodule.hlean +++ b/algebra/submodule.hlean @@ -164,7 +164,7 @@ definition is_prop_submodule (S : property M) [is_submodule M S] [H : is_prop M] begin apply @is_trunc_sigma, exact H end local attribute is_prop_submodule [instance] definition is_contr_submodule [instance] (S : property M) [is_submodule M S] [is_contr M] : is_contr (submodule S) := -is_contr_of_inhabited_prop 0 +is_contr_of_inhabited_prop 0 _ definition submodule_isomorphism [constructor] (S : property M) [is_submodule M S] (h : Πg, g ∈ S) : submodule S ≃lm M := @@ -244,7 +244,7 @@ local attribute is_prop_quotient_module [instance] definition is_contr_quotient_module [instance] (S : property M) [is_submodule M S] [is_contr M] : is_contr (quotient_module S) := -is_contr_of_inhabited_prop 0 +is_contr_of_inhabited_prop 0 _ definition rel_of_is_contr_quotient_module (S : property M) [is_submodule M S] (H : is_contr (quotient_module S)) (m : M) : S m := diff --git a/choice.hlean b/choice.hlean index 79c6f9f..df700ba 100644 --- a/choice.hlean +++ b/choice.hlean @@ -18,7 +18,7 @@ equiv.mk _ (H A) definition has_choice_of_succ (X : Type) (H : Πk, has_choice (k.+1) X) (n : ℕ₋₂) : has_choice n X := begin cases n with n, - { intro A, apply is_equiv_of_is_contr }, + { intro A, exact is_equiv_of_is_contr _ _ _ }, { exact H n } end diff --git a/cohomology/basic.hlean b/cohomology/basic.hlean index 69eb5c9..fbad479 100644 --- a/cohomology/basic.hlean +++ b/cohomology/basic.hlean @@ -85,7 +85,6 @@ end definition cohomology_isomorphism_shomotopy_group_sp_cotensor (X : Type*) (Y : spectrum) {n m : ℤ} (p : -m = n) : H^n[X, Y] ≃g πₛ[m] (sp_cotensor X Y) := begin - refine !trunc_ppi_isomorphic_pmap⁻¹ᵍ ⬝g _, refine parametrized_cohomology_isomorphism_shomotopy_group_spi (λx, Y) p ⬝g _, apply shomotopy_group_isomorphism_of_pequiv, intro k, apply pppi_pequiv_ppmap @@ -297,7 +296,7 @@ begin { exfalso, apply H, reflexivity }, { apply is_conn_of_le, apply zero_le_of_nat n, exact is_conn_EMadd1 G n, }}, { apply is_trunc_trunc_of_is_trunc, apply @is_contr_loop_of_is_trunc (n+1) (K G 0), - apply is_trunc_of_le _ (zero_le_of_nat n) } + apply is_trunc_of_le _ (zero_le_of_nat n) _ } end theorem EM_dimension (G : AbGroup) (n : ℤ) (H : n ≠ 0) : diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean index e7b66e5..235115e 100644 --- a/cohomology/serre.hlean +++ b/cohomology/serre.hlean @@ -85,13 +85,15 @@ begin exact pfiber_postnikov_map A n end + +set_option formatter.hide_full_terms false definition pfiber_postnikov_map_pred' (A : spectrum) (n k l : ℤ) (p : n + k = l) : pfiber (postnikov_map_pred (A k) (maxm2 l)) ≃* EM_spectrum (πₛ[n] A) l := begin cases l with l l, { refine pfiber_postnikov_map_pred (A k) l ⬝e* _, exact EM_type_pequiv_EM A p }, - { apply pequiv_of_is_contr, apply is_contr_pfiber_pid, + { refine pequiv_of_is_contr _ _ _ _, apply is_contr_pfiber_pid, apply is_contr_EM_spectrum_neg } end diff --git a/colimit/seq_colim.hlean b/colimit/seq_colim.hlean index 98f2355..d132308 100644 --- a/colimit/seq_colim.hlean +++ b/colimit/seq_colim.hlean @@ -322,8 +322,8 @@ variable (f) definition is_contr_seq_colim {A : ℕ → Type} (f : seq_diagram A) [Πk, is_contr (A k)] : is_contr (seq_colim f) := begin - apply @is_trunc_is_equiv_closed (A 0), - apply is_equiv_inclusion0, intro n, apply is_equiv_of_is_contr + refine is_contr_is_equiv_closed (ι' f 0) _ _, + apply is_equiv_inclusion0, intro n, exact is_equiv_of_is_contr _ _ _ end definition seq_colim_equiv_of_is_equiv [constructor] {n : ℕ} (H : Πk, k ≥ n → is_equiv (@f k)) : @@ -882,7 +882,7 @@ theorem is_trunc_fun_inclusion (k : ℕ₋₂) (H : Πn, is_trunc_fun k (@f n)) is_trunc_fun k (ι' f 0) := begin intro x, - apply @(is_trunc_equiv_closed_rev k (fiber_inclusion x)), + apply is_trunc_equiv_closed_rev k (fiber_inclusion x), apply is_trunc_fun_seq_colim_functor, intro n, apply is_trunc_fun_lrep, exact H end @@ -913,11 +913,11 @@ definition lrep_seq_diagram_fin {n : ℕ} (x : fin n) : begin induction x with k H, esimp, induction H with n H p, reflexivity, - exact ap (@lift_succ2 _) p + exact ap (@lift_succ _) p end definition lrep_seq_diagram_fin_lift_succ {n : ℕ} (x : fin n) : - lrep_seq_diagram_fin (lift_succ2 x) = ap (@lift_succ2 _) (lrep_seq_diagram_fin x) := + lrep_seq_diagram_fin (lift_succ x) = ap (@lift_succ _) (lrep_seq_diagram_fin x) := begin induction x with k H, reflexivity end diff --git a/colimit/sequence.hlean b/colimit/sequence.hlean index a8606a0..0f1d9df 100644 --- a/colimit/sequence.hlean +++ b/colimit/sequence.hlean @@ -6,7 +6,7 @@ Authors: Floris van Doorn, Egbert Rijke import ..move_to_lib types.fin types.trunc -open nat eq equiv sigma sigma.ops is_equiv is_trunc trunc prod fiber function +open nat eq equiv sigma sigma.ops is_equiv is_trunc trunc prod fiber function is_conn namespace seq_colim @@ -77,7 +77,7 @@ namespace seq_colim begin induction H with m H Hlrepf, { apply is_equiv_id }, - { exact is_equiv_compose (@f _) (lrep f H) }, + { exact is_equiv_compose (@f _) (lrep f H) _ _ }, end local attribute is_equiv_lrep [instance] @@ -211,7 +211,7 @@ namespace seq_colim open fin definition seq_diagram_fin [unfold_full] : seq_diagram fin := - lift_succ2 + lift_succ definition id0_seq [unfold_full] (a₁ a₂ : A 0) : ℕ → Type := λ k, rep0 f k a₁ = rep0 f k a₂ diff --git a/component.hlean b/component.hlean new file mode 100644 index 0000000..9e05a55 --- /dev/null +++ b/component.hlean @@ -0,0 +1,100 @@ +-- Author: Floris van Doorn + +import homotopy.connectedness .move_to_lib + +open eq equiv pointed is_conn is_trunc sigma prod trunc function group nat fiber + +namespace is_conn + + open sigma.ops pointed trunc_index + + /- this is equivalent to pfiber (A → ∥A∥₀) ≡ connect 0 A -/ + definition component [constructor] (A : Type*) : Type* := + pType.mk (Σ(a : A), merely (pt = a)) ⟨pt, tr idp⟩ + + lemma is_conn_component [instance] (A : Type*) : is_conn 0 (component A) := + is_conn_zero_pointed' + begin intro x, induction x with a p, induction p with p, induction p, exact tidp end + + definition component_incl [constructor] (A : Type*) : component A →* A := + pmap.mk pr1 idp + + definition is_embedding_component_incl [instance] (A : Type*) : is_embedding (component_incl A) := + is_embedding_pr1 _ + + definition component_intro [constructor] {A B : Type*} (f : A →* B) (H : merely_constant f) : + A →* component B := + begin + fapply pmap.mk, + { intro a, refine ⟨f a, _⟩, exact tinverse (merely_constant_pmap H a) }, + exact subtype_eq !respect_pt + end + + definition component_functor [constructor] {A B : Type*} (f : A →* B) : + component A →* component B := + component_intro (f ∘* component_incl A) !merely_constant_of_is_conn + + -- definition component_elim [constructor] {A B : Type*} (f : A →* B) (H : merely_constant f) : + -- A →* component B := + -- begin + -- fapply pmap.mk, + -- { intro a, refine ⟨f a, _⟩, exact tinverse (merely_constant_pmap H a) }, + -- exact subtype_eq !respect_pt + -- end + + definition loop_component (A : Type*) : Ω (component A) ≃* Ω A := + loop_pequiv_loop_of_is_embedding (component_incl A) + + lemma loopn_component (n : ℕ) (A : Type*) : Ω[n+1] (component A) ≃* Ω[n+1] A := + !loopn_succ_in ⬝e* loopn_pequiv_loopn n (loop_component A) ⬝e* !loopn_succ_in⁻¹ᵉ* + + -- lemma fundamental_group_component (A : Type*) : π₁ (component A) ≃g π₁ A := + -- isomorphism_of_equiv (trunc_equiv_trunc 0 (loop_component A)) _ + + lemma homotopy_group_component (n : ℕ) (A : Type*) : πg[n+1] (component A) ≃g πg[n+1] A := + homotopy_group_isomorphism_of_is_embedding (n+1) (component_incl A) + + definition is_trunc_component [instance] (n : ℕ₋₂) (A : Type*) [is_trunc n A] : + is_trunc n (component A) := + begin + apply @is_trunc_sigma, intro a, cases n with n, + { refine is_contr_of_inhabited_prop _ _, exact tr !is_prop.elim }, + { exact is_trunc_succ_of_is_prop _ _ _ }, + end + + definition ptrunc_component' (n : ℕ₋₂) (A : Type*) : + ptrunc (n.+2) (component A) ≃* component (ptrunc (n.+2) A) := + begin + fapply pequiv.MK', + { exact ptrunc.elim (n.+2) (component_functor !ptr) }, + { intro x, cases x with x p, induction x with a, + refine tr ⟨a, _⟩, + note q := trunc_functor -1 !tr_eq_tr_equiv p, + exact trunc_trunc_equiv_left _ !minus_one_le_succ q }, + { exact sorry }, + { exact sorry } + end + + definition ptrunc_component (n : ℕ₋₂) (A : Type*) : + ptrunc n (component A) ≃* component (ptrunc n A) := + begin + cases n with n, exact sorry, + cases n with n, exact sorry, + exact ptrunc_component' n A + end + + definition break_into_components (A : Type) : A ≃ Σ(x : trunc 0 A), Σ(a : A), ∥ tr a = x ∥ := + calc + A ≃ Σ(a : A) (x : trunc 0 A), tr a = x : + by exact (@sigma_equiv_of_is_contr_right _ _ (λa, !is_contr_sigma_eq))⁻¹ᵉ + ... ≃ Σ(x : trunc 0 A) (a : A), tr a = x : + by apply sigma_comm_equiv + ... ≃ Σ(x : trunc 0 A), Σ(a : A), ∥ tr a = x ∥ : + by exact sigma_equiv_sigma_right (λx, sigma_equiv_sigma_right (λa, !trunc_equiv⁻¹ᵉ)) + + definition pfiber_pequiv_component_of_is_contr [constructor] {A B : Type*} (f : A →* B) + [is_contr B] + /- extra condition, something like trunc_functor 0 f is an embedding -/ : pfiber f ≃* component A := + sorry + +end is_conn diff --git a/higher_groups.hlean b/higher_groups.hlean index b4c8de3..dd27122 100644 --- a/higher_groups.hlean +++ b/higher_groups.hlean @@ -6,7 +6,7 @@ Authors: Ulrik Buchholtz, Egbert Rijke, Floris van Doorn Formalization of the higher groups paper -/ -import .homotopy.EM +import .homotopy.EM algebra.category.constructions.pullback open eq is_conn pointed is_trunc trunc equiv is_equiv trunc_index susp nat algebra prod.ops sigma sigma.ops category EM namespace higher_group diff --git a/homology/basic.hlean b/homology/basic.hlean index 851aa8e..e884723 100644 --- a/homology/basic.hlean +++ b/homology/basic.hlean @@ -102,8 +102,8 @@ namespace homology fapply is_equiv_of_equiv_of_homotopy, { exact equiv_of_isomorphism iso }, { refine dirsum_homotopy _, intro i y, - refine homomorphism_comp_compute iso3 (iso2 ∘g iso1) _ ⬝ _, - refine ap iso3 (homomorphism_comp_compute iso2 iso1 _) ⬝ _, + refine homomorphism_compose_eq iso3 (iso2 ∘g iso1) _ ⬝ _, + refine ap iso3 (homomorphism_compose_eq iso2 iso1 _) ⬝ _, refine ap (iso3 ∘ iso2) _ ⬝ _, { exact dirsum_incl (λ i, HH theory n (X (down i))) (up i) y }, { refine _ ⬝ dirsum_elim_compute (λi, dirsum_incl (λ i, HH theory n (X (down.{0 u} i))) (up i)) i y, diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index 77f5ca2..5df2456 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -197,35 +197,35 @@ namespace EM definition homotopy_group_functor_EMadd1_functor' {G H : AbGroup} (φ : G →g H) (n : ℕ) : hsquare (ghomotopy_group_EMadd1' G n)⁻¹ᵍ (ghomotopy_group_EMadd1' H n)⁻¹ᵍ (π→g[n+1] (EMadd1_functor φ n)) φ := - (homotopy_group_functor_EMadd1_functor φ n)⁻¹ʰᵗʸʰ + begin apply hhinverse, exact (homotopy_group_functor_EMadd1_functor φ n) end - definition EM1_pmap_natural {G H : Group} {X Y : Type*} (f : X →* Y) (eX : G → Ω X) - (eY : H → Ω Y) (rX : Πg h, eX (g * h) = eX g ⬝ eX h) (rY : Πg h, eY (g * h) = eY g ⬝ eY h) - [H2 : is_trunc 1 X] [is_trunc 1 Y] (φ : G →g H) (p : hsquare eX eY φ (Ω→ f)) : - psquare (EM1_pmap eX rX) (EM1_pmap eY rY) (EM1_functor φ) f := + section infgroup + open infgroup + definition EM1_pmap_natural {G H : Group} {X Y : Type*} (f : X →* Y) (eX : G →∞g Ωg X) + (eY : H →∞g Ωg Y) [H2 : is_trunc 1 X] [is_trunc 1 Y] (φ : G →g H) + (p : hsquare eX eY φ (Ωg→ f)) : psquare (EM1_pmap eX) (EM1_pmap eY) (EM1_functor φ) f := begin fapply phomotopy.mk, { intro x, induction x using EM.set_rec, { exact respect_pt f }, { apply eq_pathover, - refine ap_compose f _ _ ⬝ph _ ⬝hp (ap_compose (EM1_pmap eY rY) _ _)⁻¹, + refine ap_compose f _ _ ⬝ph _ ⬝hp (ap_compose (EM1_pmap eY) _ _)⁻¹, refine ap02 _ !elim_pth ⬝ph _ ⬝hp ap02 _ !elim_pth⁻¹, refine _ ⬝hp !elim_pth⁻¹, apply transpose, exact square_of_eq_bot (p g) }}, { exact !idp_con⁻¹ } end - definition EM1_pequiv'_natural {G H : Group} {X Y : Type*} (f : X →* Y) (eX : G ≃* Ω X) - (eY : H ≃* Ω Y) (rX : Πg h, eX (g * h) = eX g ⬝ eX h) (rY : Πg h, eY (g * h) = eY g ⬝ eY h) - [H1 : is_conn 0 X] [H2 : is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y] + definition EM1_pequiv'_natural {G H : Group} {X Y : Type*} (f : X →* Y) (eX : G ≃∞g Ωg X) + (eY : H ≃∞g Ωg Y) [H1 : is_conn 0 X] [H2 : is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y] (φ : G →g H) (p : hsquare eX eY φ (Ω→ f)) : - psquare (EM1_pequiv' eX rX) (EM1_pequiv' eY rY) (EM1_functor φ) f := - EM1_pmap_natural f eX eY rX rY φ p + psquare (EM1_pequiv' eX) (EM1_pequiv' eY) (EM1_functor φ) f := + EM1_pmap_natural f eX eY φ p definition EM1_pequiv_natural {G H : Group} {X Y : Type*} (f : X →* Y) (eX : G ≃g π₁ X) (eY : H ≃g π₁ Y) [H1 : is_conn 0 X] [H2 : is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y] (φ : G →g H) (p : hsquare eX eY φ (π→g[1] f)) : psquare (EM1_pequiv eX) (EM1_pequiv eY) (EM1_functor φ) f := - EM1_pequiv'_natural f _ _ _ _ φ + EM1_pequiv'_natural f _ _ φ begin assert p' : ptrunc_functor 0 (Ω→ f) ∘* pequiv_of_isomorphism eX ~* pequiv_of_isomorphism eY ∘* pmap_of_homomorphism φ, exact phomotopy_of_homotopy p, @@ -238,38 +238,35 @@ namespace EM begin refine EM1_pequiv_natural f _ _ _ _, exact homotopy.rfl end definition EM_up_natural {G H : AbGroup} (φ : G →g H) {X Y : Type*} (f : X →* Y) {n : ℕ} - (eX : G →* Ω[succ (succ n)] X) (eY : H →* Ω[succ (succ n)] Y) - (p : hsquare eX eY φ (Ω→[succ (succ n)] f)) + (eX : G →∞g Ωg[succ (succ n)] X) (eY : H →∞g Ωg[succ (succ n)] Y) + (p : hsquare eX eY φ (Ωg→[succ (succ n)] f)) : hsquare (EM_up eX) (EM_up eY) φ (Ω→[succ n] (Ω→ f)) := - begin - refine p ⬝htyh hsquare_of_psquare (loopn_succ_in_natural (succ n) f), - end + p ⬝htyh hsquare_of_psquare (loopn_succ_in_natural (succ n) f) definition EMadd1_pmap_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) - (eX : G →* Ω[succ n] X) (eY : H →* Ω[succ n] Y) (rX : Π(g h : G), eX (g * h) = eX g ⬝ eX h) - (rY : Π(g h : H), eY (g * h) = eY g ⬝ eY h) [HX : is_trunc (n.+1) X] [HY : is_trunc (n.+1) Y] - (φ : G →g H) (p : hsquare eX eY φ (Ω→[succ n] f)) : - psquare (EMadd1_pmap n eX rX) (EMadd1_pmap n eY rY) (EMadd1_functor φ n) f := + (eX : G →∞g Ωg[succ n] X) (eY : H →∞g Ωg[succ n] Y) + [HX : is_trunc (n.+1) X] [HY : is_trunc (n.+1) Y] + (φ : G →g H) (p : hsquare eX eY φ (Ωg→[succ n] f)) : + psquare (EMadd1_pmap n eX) (EMadd1_pmap n eY) (EMadd1_functor φ n) f := begin - revert X Y f eX eY rX rY HX HY p, induction n with n IH: intros, + revert X Y f eX eY HX HY p, induction n with n IH: intros, { apply EM1_pmap_natural, exact p }, { do 2 rewrite [EMadd1_pmap_succ], refine _ ⬝* pwhisker_left _ !EMadd1_functor_succ⁻¹*, refine (ptrunc_elim_pcompose ((succ n).+1) _ _)⁻¹* ⬝* _ ⬝* (ptrunc_elim_ptrunc_functor ((succ n).+1) _ _)⁻¹*, apply ptrunc_elim_phomotopy, refine _ ⬝* !susp_elim_susp_functor⁻¹*, - refine _ ⬝* susp_elim_phomotopy (IH _ _ _ _ _ (is_homomorphism_EM_up eX rX) _ + refine _ ⬝* susp_elim_phomotopy (IH _ _ _ _ _ (@is_trunc_loop _ _ HX) _ (EM_up_natural φ f eX eY p)), apply susp_elim_natural } end definition EMadd1_pequiv'_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) - (eX : G ≃* Ω[succ n] X) (eY : H ≃* Ω[succ n] Y) (rX : Π(g h : G), eX (g * h) = eX g ⬝ eX h) - (rY : Π(g h : H), eY (g * h) = eY g ⬝ eY h) + (eX : G ≃∞g Ωg[succ n] X) (eY : H ≃∞g Ωg[succ n] Y) [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] [is_conn n Y] [is_trunc (n.+1) Y] - (φ : G →g H) (p : hsquare eX eY φ (Ω→[succ n] f)) : - psquare (EMadd1_pequiv' n eX rX) (EMadd1_pequiv' n eY rY) (EMadd1_functor φ n) f := - EMadd1_pmap_natural f n eX eY rX rY φ p + (φ : G →g H) (p : hsquare eX eY φ (Ωg→[succ n] f)) : + psquare (EMadd1_pequiv' n eX) (EMadd1_pequiv' n eY) (EMadd1_functor φ n) f := + EMadd1_pmap_natural f n eX eY φ p definition EMadd1_pequiv_natural_local_instance {X : Type*} (n : ℕ) [H : is_trunc (n.+1) X] : is_set (Ω[succ n] X) := @@ -277,14 +274,17 @@ namespace EM local attribute EMadd1_pequiv_natural_local_instance [instance] - definition EMadd1_pequiv_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) (eX : G ≃g πg[n+1] X) - (eY : H ≃g πg[n+1] Y) [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] [H3 : is_conn n Y] + definition EMadd1_pequiv_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) + (eX : G ≃g πg[n+1] X) (eY : H ≃g πg[n+1] Y) + [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] [H3 : is_conn n Y] [H4 : is_trunc (n.+1) Y] (φ : G →g H) (p : hsquare eX eY φ (π→g[n+1] f)) : psquare (EMadd1_pequiv n eX) (EMadd1_pequiv n eY) (EMadd1_functor φ n) f := EMadd1_pequiv'_natural f n - (pequiv_of_isomorphism eX ⬝e* ptrunc_pequiv 0 (Ω[succ n] X)) - (pequiv_of_isomorphism eY ⬝e* ptrunc_pequiv 0 (Ω[succ n] Y)) - _ _ φ (p ⬝htyh hsquare_of_psquare (ptrunc_pequiv_natural 0 (Ω→[succ n] f))) + _ --(inf_isomorphism_of_isomorphism eX ⬝∞g gtrunc_isomorphism (Ω[succ n] X)) + _ --(inf_isomorphism_of_isomorphism eY ⬝∞g gtrunc_isomorphism (Ω[succ n] Y)) + φ (p ⬝htyh hsquare_of_psquare (ptrunc_pequiv_natural 0 (Ω→[succ n] f))) + + end infgroup definition EMadd1_pequiv_succ_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) (eX : G ≃g πag[n+2] X) (eY : H ≃g πag[n+2] Y) [is_conn (n.+1) X] [is_trunc (n.+2) X] @@ -343,6 +343,24 @@ namespace EM { refine !loopn_succ_in ⬝e* Ω≃[n] (loop_EMadd1 G (m + n))⁻¹ᵉ* ⬝e* e } end + /- properties about EM -/ + + definition gEM (G : AbGroup) (n : ℕ) : InfGroup := + InfGroup.mk (EM G n) (inf_group_equiv_closed (loop_EM G n) _) + + definition gEM_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) : gEM G n →∞g gEM H n := + inf_homomorphism.mk (EM_functor φ n) sorry + + definition EM_pmap [unfold 8] {G : AbGroup} (X : InfGroup) (n : ℕ) + (e : AbInfGroup_of_AbGroup G →∞g Ωg'[n] X) [H : is_trunc n X] : EM G n →* X := + begin + cases n with n, + { exact pmap_of_inf_homomorphism e }, + { have is_trunc (n.+1) X, from H, exact EMadd1_pmap n e } + end + + -- definition gEM_gfunctor {G H : AbGroup} (n : ℕ) : (G →gg H) →∞g (gEM G n →∞g gEM H n) := + -- inf_homomorphism.mk (EM_functor _ n) sorry /- The Eilenberg-MacLane space K(G,n) with the same homotopy group as X on level n. On paper this is written K(πₙ(X), n). The problem is that for @@ -508,14 +526,14 @@ namespace EM definition homotopy_group_cfunctor : cType*[0] ⇒ Grp := functor.mk (λX, πg[1] X) - (λX Y f, π→g[1] f) + (λX Y (f : X →* Y), π→g[1] f) begin intro, apply homomorphism_eq, exact to_homotopy !homotopy_group_functor_pid end begin intros, apply homomorphism_eq, exact to_homotopy !homotopy_group_functor_pcompose end definition ab_homotopy_group_cfunctor (n : ℕ) : cType*[n.+1] ⇒ AbGrp := functor.mk (λX, πag[n+2] X) - (λX Y f, π→g[n+2] f) + (λX Y (f : X →* Y), by rexact π→g[n+2] f) begin intro, apply homomorphism_eq, exact to_homotopy !homotopy_group_functor_pid end begin intros, apply homomorphism_eq, exact to_homotopy !homotopy_group_functor_pcompose end @@ -593,8 +611,12 @@ namespace EM EM1_functor_gid H end definition is_contr_EM1 {G : Group} (H : is_contr G) : is_contr (EM1 G) := - is_contr_of_is_conn_of_is_trunc - (is_trunc_succ_succ_of_is_trunc_loop _ _ (is_trunc_equiv_closed _ !loop_EM1 _) _) !is_conn_EM1 + begin + refine is_contr_of_is_conn_of_is_trunc _ !is_conn_EM1, + refine is_trunc_succ_succ_of_is_trunc_loop _ _ _ _, + refine is_trunc_equiv_closed _ !loop_EM1 _, + apply is_trunc_succ, exact H + end definition is_contr_EMadd1 (n : ℕ) {G : AbGroup} (H : is_contr G) : is_contr (EMadd1 G n) := begin @@ -642,7 +664,7 @@ namespace EM definition is_conn_fiber_EM1_functor {G H : Group} (φ : G →g H) : is_conn -1 (pfiber (EM1_functor φ)) := begin - apply is_conn_fiber + apply is_conn_fiber_of_is_conn end definition is_trunc_fiber_EMadd1_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) : @@ -654,7 +676,7 @@ namespace EM definition is_conn_fiber_EMadd1_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) : is_conn (n.-1) (pfiber (EMadd1_functor φ n)) := begin - apply is_conn_fiber, apply is_conn_of_is_conn_succ, apply is_conn_EMadd1, + apply is_conn_fiber_of_is_conn, apply is_conn_of_is_conn_succ, apply is_conn_EMadd1, apply is_conn_EMadd1 end @@ -667,7 +689,7 @@ namespace EM definition is_conn_fiber_EM_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) : is_conn (n.-2) (pfiber (EM_functor φ n)) := begin - apply is_conn_fiber, apply is_conn_of_is_conn_succ + apply is_conn_fiber_of_is_conn, apply is_conn_of_is_conn_succ end section diff --git a/homotopy/EMRing.hlean b/homotopy/EMRing.hlean index 4b932fb..c2c4ec8 100644 --- a/homotopy/EMRing.hlean +++ b/homotopy/EMRing.hlean @@ -1,6 +1,6 @@ -- Authors: Floris van Doorn -import .EM .smash_adjoint ..algebra.ring +import .EM .smash_adjoint ..algebra.ring ..algebra.arrow_group open algebra eq EM is_equiv equiv is_trunc is_conn pointed trunc susp smash group nat namespace EM @@ -10,44 +10,58 @@ definition EM1product_adj {R : Ring} : begin have is_trunc 1 (ppmap (EM1 (AbGroup_of_Ring R)) (EMadd1 (AbGroup_of_Ring R) 1)), from is_trunc_pmap_of_is_conn _ _ _ _ _ _ (le.refl 2) !is_trunc_EMadd1, - fapply EM1_pmap, + apply EM1_pmap, fapply inf_homomorphism.mk, { intro r, refine pfunext _ _, exact !loop_EM2⁻¹ᵉ* ∘* EM1_functor (ring_right_action r), }, { intro r r', exact sorry } end -definition EMproduct_map {G H K : AbGroup} (φ : G → H →g K) (n m : ℕ) (g : G) : - EMadd1 H n →* EMadd1 K n := +definition EMproduct_map {A B C : AbGroup} (φ : A → B →g C) (n m : ℕ) (a : A) : + EMadd1 B n →* EMadd1 C n := begin - fapply EMadd1_functor (φ g) n + fapply EMadd1_functor (φ a) n end -definition EM0EMadd1product {G H K : AbGroup} (φ : G →g H →gg K) (n : ℕ) : - G →* EMadd1 H n →** EMadd1 K n := -EMadd1_pfunctor H K n ∘* pmap_of_homomorphism φ +definition EM0EMadd1product {A B C : AbGroup} (φ : A →g B →gg C) (n : ℕ) : + A →* EMadd1 B n →** EMadd1 C n := +EMadd1_pfunctor B C n ∘* pmap_of_homomorphism φ -definition EMadd1product {G H K : AbGroup} (φ : G →g H →gg K) (n m : ℕ) : - EMadd1 G n →* EMadd1 H m →** EMadd1 K (m + succ n) := +definition EMadd1product {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : + EMadd1 A n →* EMadd1 B m →** EMadd1 C (m + succ n) := begin - assert H1 : is_trunc n.+1 (EMadd1 H m →** EMadd1 K (m + succ n)), + assert H1 : is_trunc n.+1 (EMadd1 B m →** EMadd1 C (m + succ n)), { refine is_trunc_pmap_of_is_conn _ (m.-1) !is_conn_EMadd1 _ _ _ _ !is_trunc_EMadd1, exact le_of_eq (trunc_index.of_nat_add_plus_two_of_nat m n)⁻¹ᵖ }, - fapply EMadd1_pmap, - { refine (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* ∘* ppcompose_left !loopn_EMadd1_add⁻¹ᵉ* ∘* - EM0EMadd1product φ m }, - { exact sorry } + apply EMadd1_pmap, + exact sorry + /- the underlying pointed map is: -/ + -- refine (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* ∘* ppcompose_left !loopn_EMadd1_add⁻¹ᵉ* ∘* + -- EM0EMadd1product φ m end -definition EMproduct {G H K : AbGroup} (φ : G →g H →gg K) (n m : ℕ) : - EM G n →* EM H m →** EM K (m + n) := +definition EMproduct {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : + EM A n →* EM B m →** EM C (m + n) := begin cases n with n, { cases m with m, { exact pmap_of_homomorphism2 φ }, { exact EM0EMadd1product φ m }}, { cases m with m, - { exact ppcompose_left (ptransport (EMadd1 K) (zero_add n)⁻¹) ∘* + { exact ppcompose_left (ptransport (EMadd1 C) (zero_add n)⁻¹) ∘* pmap_swap_map (EM0EMadd1product (homomorphism_swap φ) n) }, - { exact ppcompose_left (ptransport (EMadd1 K) !succ_add⁻¹) ∘* EMadd1product φ n m }} + { exact ppcompose_left (ptransport (EMadd1 C) !succ_add⁻¹) ∘* EMadd1product φ n m }} end +definition EMproduct' {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : + EM A n →* EM B m →** EM C (m + n) := +begin + assert H1 : is_trunc n (InfGroup_pmap' (EM B m) (loop_EM C (m + n))), + { exact is_trunc_pmap_of_is_conn_nat _ m !is_conn_EM _ _ _ !le.refl !is_trunc_EM }, + apply EM_pmap (InfGroup_pmap' (EM B m) (loop_EM C (m + n))) n, + exact sorry + -- exact _ /- (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* -/ ∘∞g _ /-ppcompose_left !loopn_EMadd1_add⁻¹ᵉ*-/ ∘∞g + -- _ ∘∞g inf_homomorphism_of_homomorphism φ + +end + + end EM diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index c04d57e..578eefa 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -472,7 +472,7 @@ namespace smash definition smash_pequiv [constructor] (f : A ≃* C) (g : B ≃* D) : A ∧ B ≃* C ∧ D := begin fapply pequiv_of_pmap (f ∧→ g), - refine @homotopy_closed _ _ _ _ _ (smash_functor_homotopy_pushout_functor f g)⁻¹ʰᵗʸ, + refine homotopy_closed _ (smash_functor_homotopy_pushout_functor f g)⁻¹ʰᵗʸ _, apply pushout.is_equiv_functor end @@ -1054,7 +1054,7 @@ namespace smash begin unfold [smash, cofiber, smash'], symmetry, fapply pushout_vcompose_equiv wedge_of_sum, - { symmetry, apply equiv_unit_of_is_contr, apply is_contr_pushout_wedge_of_sum }, + { symmetry, refine equiv_unit_of_is_contr _ _, apply is_contr_pushout_wedge_of_sum }, { intro x, reflexivity }, { apply prod_of_wedge_of_sum } end diff --git a/homotopy/susp.hlean b/homotopy/susp.hlean index aabc70a..c340107 100644 --- a/homotopy/susp.hlean +++ b/homotopy/susp.hlean @@ -71,7 +71,7 @@ namespace susp begin intro p, refine susp_functor_psquare p ⬝v* _, - exact psquare_transpose (loop_susp_counit_natural f₁₂) + exact ptranspose (loop_susp_counit_natural f₁₂) end open pushout unit prod sigma sigma.ops diff --git a/logic.hlean b/logic.hlean index 86c4388..b6863fc 100644 --- a/logic.hlean +++ b/logic.hlean @@ -21,7 +21,7 @@ section open trunc_index definition propext {p q : Prop} (h : p ↔ q) : p = q := -tua (equiv_of_iff_of_is_prop h) +tua (equiv_of_iff_of_is_prop h _ _) end @@ -55,8 +55,8 @@ 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₂ + intro h₃, + apply sum.elim h₃ h₁ h₂ end end logic diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 36dffc8..949f87c 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -7,25 +7,6 @@ open eq nat int susp pointed sigma is_equiv equiv fiber algebra trunc pi group universe variable u -/- -eq_of_homotopy_eta > eq_of_homotopy_apd10 -pathover_of_tr_eq_idp > pathover_idp_of_eq -pathover_of_tr_eq_idp' > pathover_of_tr_eq_idp -homotopy_group_isomorphism_of_ptrunc_pequiv > ghomotopy_group_isomorphism_of_ptrunc_pequiv -equiv_pathover <> equiv_pathover2 -homotopy_group_functor_succ_phomotopy_in > homotopy_group_succ_in_natural -homotopy_group_succ_in_natural > homotopy_group_succ_in_natural_unpointed -le_step_left > le_of_succ_le -pmap.eta > pmap_eta -pType.sigma_char' > pType.sigma_char -cghomotopy_group to aghomotopy_group -is_trunc_loop_of_is_trunc > is_trunc_loopn_of_is_trunc - - -first two arguments reordered in is_trunc_loopn_nat -reorder pathover arguments of constructions with squareovers (mostly implicit) --/ - namespace eq definition transport_lemma {A : Type} {C : A → Type} {g₁ : A → A} @@ -41,34 +22,6 @@ namespace eq variables {A A' B : Type} {a a₂ a₃ : A} {p p' : a = a₂} {p₂ : a₂ = a₃} {a' a₂' a₃' : A'} {b b₂ : B} - definition apd_eq_ap (f : A → A') (p : a = a₂) : eq_of_pathover (apd f p) = ap f p := - begin induction p, reflexivity end - - definition eq_of_pathover_idp_constant (p : b =[idpath a] b₂) : - eq_of_pathover_idp p = eq_of_pathover p := - begin induction p using idp_rec_on, reflexivity end - - definition eq_of_pathover_change_path (r : p = p') (q : a' =[p] a₂') : - eq_of_pathover (change_path r q) = eq_of_pathover q := - begin induction r, reflexivity end - - definition eq_of_pathover_cono (q : a' =[p] a₂') (q₂ : a₂' =[p₂] a₃') : - eq_of_pathover (q ⬝o q₂) = eq_of_pathover q ⬝ eq_of_pathover q₂ := - begin induction q₂, reflexivity end - - definition eq_of_pathover_invo (q : a' =[p] a₂') : - eq_of_pathover q⁻¹ᵒ = (eq_of_pathover q)⁻¹ := - begin induction q, reflexivity end - - definition eq_of_pathover_concato_eq (q : a' =[p] a₂') (q₂ : a₂' = a₃') : - eq_of_pathover (q ⬝op q₂) = eq_of_pathover q ⬝ q₂ := - begin induction q₂, reflexivity end - - definition eq_of_pathover_eq_concato (q : a' = a₂') (q₂ : a₂' =[p₂] a₃') : - eq_of_pathover (q ⬝po q₂) = q ⬝ eq_of_pathover q₂ := - begin induction q, induction q₂, reflexivity end - - end eq open eq namespace nat @@ -90,16 +43,6 @@ namespace nat end nat - definition max0_monotone {n m : ℤ} (H : n ≤ m) : max0 n ≤ max0 m := - begin - induction n with n n, - { induction m with m m, - { exact le_of_of_nat_le_of_nat H }, - { exfalso, exact not_neg_succ_le_of_nat H }}, - { apply zero_le } - end - - -- definition ppi_eq_equiv_internal : (k = l) ≃ (k ~* l) := -- calc (k = l) ≃ ppi.sigma_char P p₀ k = ppi.sigma_char P p₀ l -- : eq_equiv_fn_eq (ppi.sigma_char P p₀) k l @@ -122,21 +65,12 @@ end nat namespace pointed -infixr ` →** `:29 := ppmap end pointed open pointed namespace trunc open trunc_index sigma.ops - definition ptrunc_functor_pconst [constructor] (n : ℕ₋₂) (X Y : Type*) : - ptrunc_functor n (pconst X Y) ~* pconst (ptrunc n X) (ptrunc n Y) := - begin - fapply phomotopy.mk, - { intro x, induction x with x, reflexivity }, - { reflexivity } - end - -- TODO: redefine loopn_ptrunc_pequiv definition apn_ptrunc_functor (n : ℕ₋₂) (k : ℕ) {A B : Type*} (f : A →* B) : Ω→[k] (ptrunc_functor (n+k) f) ∘* (loopn_ptrunc_pequiv n k A)⁻¹ᵉ* ~* @@ -170,94 +104,13 @@ namespace sigma -- rewrite [▸*, is_prop_elimo_self (C a) c] }, -- { esimp, generalize ⟨b, c⟩, intro x q, } -- end ---rexact @(ap pathover_pr1) _ idpo _, - definition sigma_functor2 [constructor] {A₁ A₂ A₃ : Type} - {B₁ : A₁ → Type} {B₂ : A₂ → Type} {B₃ : A₃ → Type} - (f : A₁ → A₂ → A₃) (g : Π⦃a₁ a₂⦄, B₁ a₁ → B₂ a₂ → B₃ (f a₁ a₂)) - (x₁ : Σa₁, B₁ a₁) (x₂ : Σa₂, B₂ a₂) : Σa₃, B₃ a₃ := - ⟨f x₁.1 x₂.1, g x₁.2 x₂.2⟩ - - 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 - - definition ap_sigma_pr1 {A B : Type} {C : B → Type} {a₁ a₂ : A} (f : A → B) (g : Πa, C (f a)) - (p : a₁ = a₂) : (ap (λa, ⟨f a, g a⟩) p)..1 = ap f p := - by induction p; reflexivity - - definition ap_sigma_pr2 {A B : Type} {C : B → Type} {a₁ a₂ : A} (f : A → B) (g : Πa, C (f a)) - (p : a₁ = a₂) : (ap (λa, ⟨f a, g a⟩) p)..2 = - change_path (ap_sigma_pr1 f g p)⁻¹ (pathover_ap C f (apd g p)) := - by induction p; reflexivity - - definition ap_sigma_functor_sigma_eq {A A' : Type} {B : A → Type} {B' : A' → Type} - {a a' : A} {b : B a} {b' : B a'} (f : A → A') (g : Πa, B a → B' (f a)) (p : a = a') (q : b =[p] b') : - ap (sigma_functor f g) (sigma_eq p q) = sigma_eq (ap f p) (pathover_ap B' f (apo g q)) := - by induction q; reflexivity - - definition ap_sigma_functor_id_sigma_eq {A : Type} {B B' : A → Type} - {a a' : A} {b : B a} {b' : B a'} (g : Πa, B a → B' a) (p : a = a') (q : b =[p] b') : - ap (sigma_functor id g) (sigma_eq p q) = sigma_eq p (apo g q) := - by induction q; reflexivity - - definition sigma_eq_pr2_constant {A B : Type} {a a' : A} {b b' : B} (p : a = a') - (q : b =[p] b') : ap pr2 (sigma_eq p q) = (eq_of_pathover q) := - by induction q; reflexivity - - definition sigma_eq_pr2_constant2 {A B : Type} {a a' : A} {b b' : B} (p : a = a') - (q : b = b') : ap pr2 (sigma_eq p (pathover_of_eq p q)) = q := - by induction p; induction q; reflexivity - - definition sigma_eq_concato_eq {A : Type} {B : A → Type} {a a' : A} {b : B a} {b₁ b₂ : B a'} - (p : a = a') (q : b =[p] b₁) (q' : b₁ = b₂) : sigma_eq p (q ⬝op q') = sigma_eq p q ⬝ ap (dpair a') q' := - by induction q'; reflexivity - - definition sigma_functor_compose {A A' A'' : Type} {B : A → Type} {B' : A' → Type} - {B'' : A'' → Type} {f' : A' → A''} {f : A → A'} (g' : Πa, B' a → B'' (f' a)) - (g : Πa, B a → B' (f a)) (x : Σa, B a) : - sigma_functor f' g' (sigma_functor f g x) = sigma_functor (f' ∘ f) (λa, g' (f a) ∘ g a) x := - begin - reflexivity - end - - definition sigma_functor_homotopy {A A' : Type} {B : A → Type} {B' : A' → Type} - {f f' : A → A'} {g : Πa, B a → B' (f a)} {g' : Πa, B a → B' (f' a)} (h : f ~ f') - (k : Πa b, g a b =[h a] g' a b) (x : Σa, B a) : sigma_functor f g x = sigma_functor f' g' x := - sigma_eq (h x.1) (k x.1 x.2) - - variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type} - {B₀₀ : A₀₀ → Type} {B₂₀ : A₂₀ → Type} {B₀₂ : A₀₂ → Type} {B₂₂ : A₂₂ → Type} - {f₁₀ : A₀₀ → A₂₀} {f₁₂ : A₀₂ → A₂₂} {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂} - {g₁₀ : Πa, B₀₀ a → B₂₀ (f₁₀ a)} {g₁₂ : Πa, B₀₂ a → B₂₂ (f₁₂ a)} - {g₀₁ : Πa, B₀₀ a → B₀₂ (f₀₁ a)} {g₂₁ : Πa, B₂₀ a → B₂₂ (f₂₁ a)} - - definition sigma_functor_hsquare (h : hsquare f₁₀ f₁₂ f₀₁ f₂₁) - (k : Πa (b : B₀₀ a), g₂₁ _ (g₁₀ _ b) =[h a] g₁₂ _ (g₀₁ _ b)) : - hsquare (sigma_functor f₁₀ g₁₀) (sigma_functor f₁₂ g₁₂) - (sigma_functor f₀₁ g₀₁) (sigma_functor f₂₁ g₂₁) := - λx, sigma_functor_compose g₂₁ g₁₀ x ⬝ - sigma_functor_homotopy h k x ⬝ - (sigma_functor_compose g₁₂ g₀₁ x)⁻¹ definition sigma_equiv_of_is_embedding_left_fun [constructor] {X Y : Type} {P : Y → Type} {f : X → Y} (H : Πy, P y → fiber f y) (v : Σy, P y) : Σx, P (f x) := ⟨fiber.point (H v.1 v.2), transport P (point_eq (H v.1 v.2))⁻¹ v.2⟩ - definition sigma_equiv_of_is_embedding_left_prop [constructor] {X Y : Type} {P : Y → Type} + definition sigma_equiv_of_is_embedding_left [constructor] {X Y : Type} {P : Y → Type} (f : X → Y) (Hf : is_embedding f) (HP : Πx, is_prop (P (f x))) (H : Πy, P y → fiber f y) : (Σy, P y) ≃ Σx, P (f x) := begin @@ -272,76 +125,12 @@ namespace sigma definition sigma_equiv_of_is_embedding_left_contr [constructor] {X Y : Type} {P : Y → Type} (f : X → Y) (Hf : is_embedding f) (HP : Πx, is_contr (P (f x))) (H : Πy, P y → fiber f y) : (Σy, P y) ≃ X := - sigma_equiv_of_is_embedding_left_prop f Hf _ H ⬝e !sigma_equiv_of_is_contr_right + sigma_equiv_of_is_embedding_left f Hf _ H ⬝e !sigma_equiv_of_is_contr_right end sigma open sigma namespace group -infixr ` →gg `:56 := aghomomorphism - -definition pmap_of_homomorphism2 [constructor] {G H K : AbGroup} (φ : G →g H →gg K) : - G →* H →** K := -pmap.mk (λg, pmap_of_homomorphism (φ g)) - (eq_of_phomotopy (phomotopy_of_homotopy (ap010 group_fun (to_respect_one φ)))) - -definition homomorphism_apply [constructor] (G H : AbGroup) (g : G) : - (G →gg H) →g H := -begin - fapply homomorphism.mk, - { intro φ, exact φ g }, - { intros φ φ', reflexivity } -end - -definition homomorphism_swap [constructor] {G H K : AbGroup} (φ : G →g H →gg K) : - H →g G →gg K := -begin - fapply homomorphism.mk, - { intro h, exact homomorphism_apply H K h ∘g φ }, - { intro h h', apply homomorphism_eq, intro g, exact to_respect_mul (φ g) h h' } -end - -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 @@ -361,360 +150,27 @@ end -- : @is_mul_hom G G' (@ab_group.to_group _ (AbGroup.struct G)) _ φ := -- homomorphism.struct φ - definition pgroup_of_Group (X : Group) : pgroup X := - pgroup_of_group _ idp - definition isomorphism_ap {A : Type} (F : A → Group) {a b : A} (p : a = b) : F a ≃g F b := - isomorphism_of_eq (ap F p) - - definition interchange (G : AbGroup) (a b c d : G) : (a * b) * (c * d) = (a * c) * (b * d) := - calc (a * b) * (c * d) = a * (b * (c * d)) : by exact mul.assoc a b (c * d) - ... = a * ((b * c) * d) : by exact ap (λ bcd, a * bcd) (mul.assoc b c d)⁻¹ - ... = a * ((c * b) * d) : by exact ap (λ bc, a * (bc * d)) (mul.comm b c) - ... = a * (c * (b * d)) : by exact ap (λ bcd, a * bcd) (mul.assoc c b d) - ... = (a * c) * (b * d) : by exact (mul.assoc a c (b * d))⁻¹ - - definition homomorphism_comp_compute {G H K : Group} (g : H →g K) (f : G →g H) (x : G) : (g ∘g f) x = g (f x) := - begin - reflexivity - end + -- definition interchange (G : AbGroup) (a b c d : G) : (a * b) * (c * d) = (a * c) * (b * d) := + -- mul.comm4 a b c d open option definition add_point_AbGroup [unfold 3] {X : Type} (G : X → AbGroup) : X₊ → AbGroup | (some x) := G x | none := trivial_ab_group_lift - definition isomorphism_of_is_contr {G H : Group} (hG : is_contr G) (hH : is_contr H) : G ≃g H := - trivial_group_of_is_contr G ⬝g (trivial_group_of_is_contr H)⁻¹ᵍ + -- definition trunc_isomorphism_of_equiv {A B : Type} [inf_group A] [inf_group B] (f : A ≃ B) + -- (h : is_mul_hom f) : + -- Group.mk (trunc 0 A) (group_trunc A) ≃g Group.mk (trunc 0 B) (group_trunc B) := + -- begin + -- apply isomorphism_of_equiv (trunc_equiv_trunc 0 f), intros x x', + -- induction x with a, induction x' with a', apply ap tr, exact h a a' + -- end - definition trunc_isomorphism_of_equiv {A B : Type} [inf_group A] [inf_group B] (f : A ≃ B) - (h : is_mul_hom f) : Group.mk (trunc 0 A) (trunc_group A) ≃g Group.mk (trunc 0 B) (trunc_group B) := - begin - apply isomorphism_of_equiv (trunc_equiv_trunc 0 f), intros x x', - induction x with a, induction x' with a', apply ap tr, exact h a a' - end - - /----------------- The following are properties for ∞-groups ----------------/ - - local attribute InfGroup_of_Group [coercion] - - /- left and right actions -/ - definition is_equiv_mul_right_inf [constructor] {A : InfGroup} (a : A) : is_equiv (λb, b * a) := - adjointify _ (λb : A, b * a⁻¹) (λb, !inv_mul_cancel_right) (λb, !mul_inv_cancel_right) - - definition right_action_inf [constructor] {A : InfGroup} (a : A) : A ≃ A := - equiv.mk _ (is_equiv_mul_right_inf a) - - /- homomorphisms -/ - - structure inf_homomorphism (G₁ G₂ : InfGroup) : Type := - (φ : G₁ → G₂) - (p : is_mul_hom φ) - - infix ` →∞g `:55 := inf_homomorphism - - abbreviation inf_group_fun [unfold 3] [coercion] [reducible] := @inf_homomorphism.φ - definition inf_homomorphism.struct [unfold 3] [instance] [priority 900] {G₁ G₂ : InfGroup} - (φ : G₁ →∞g G₂) : is_mul_hom φ := - inf_homomorphism.p φ - - definition homomorphism_of_inf_homomorphism [constructor] {G H : Group} (φ : G →∞g H) : G →g H := - homomorphism.mk φ (inf_homomorphism.struct φ) - - definition inf_homomorphism_of_homomorphism [constructor] {G H : Group} (φ : G →g H) : G →∞g H := - inf_homomorphism.mk φ (homomorphism.struct φ) - - variables {G G₁ G₂ G₃ : InfGroup} {g h : G₁} {ψ : G₂ →∞g G₃} {φ₁ φ₂ : G₁ →∞g G₂} (φ : G₁ →∞g G₂) - - definition to_respect_mul_inf /- φ -/ (g h : G₁) : φ (g * h) = φ g * φ h := - respect_mul φ g h - - theorem to_respect_one_inf /- φ -/ : φ 1 = 1 := - have φ 1 * φ 1 = φ 1 * 1, by rewrite [-to_respect_mul_inf φ, +mul_one], - eq_of_mul_eq_mul_left' this - - theorem to_respect_inv_inf /- φ -/ (g : G₁) : φ g⁻¹ = (φ g)⁻¹ := - have φ (g⁻¹) * φ g = 1, by rewrite [-to_respect_mul_inf φ, mul.left_inv, to_respect_one_inf φ], - eq_inv_of_mul_eq_one this - - definition pmap_of_inf_homomorphism [constructor] /- φ -/ : G₁ →* G₂ := - pmap.mk φ begin esimp, exact to_respect_one_inf φ end - - definition inf_homomorphism_change_fun [constructor] {G₁ G₂ : InfGroup} - (φ : G₁ →∞g G₂) (f : G₁ → G₂) (p : φ ~ f) : G₁ →∞g G₂ := - inf_homomorphism.mk f - (λg h, (p (g * h))⁻¹ ⬝ to_respect_mul_inf φ g h ⬝ ap011 mul (p g) (p h)) - - /- categorical structure of groups + homomorphisms -/ - - definition inf_homomorphism_compose [constructor] [trans] [reducible] - (ψ : G₂ →∞g G₃) (φ : G₁ →∞g G₂) : G₁ →∞g G₃ := - inf_homomorphism.mk (ψ ∘ φ) (is_mul_hom_compose _ _) - - variable (G) - definition inf_homomorphism_id [constructor] [refl] : G →∞g G := - inf_homomorphism.mk (@id G) (is_mul_hom_id G) - variable {G} - - abbreviation inf_gid [constructor] := @inf_homomorphism_id - infixr ` ∘∞g `:75 := inf_homomorphism_compose - - structure inf_isomorphism (A B : InfGroup) := - (to_hom : A →∞g B) - (is_equiv_to_hom : is_equiv to_hom) - - infix ` ≃∞g `:25 := inf_isomorphism - attribute inf_isomorphism.to_hom [coercion] - attribute inf_isomorphism.is_equiv_to_hom [instance] - attribute inf_isomorphism._trans_of_to_hom [unfold 3] - - definition equiv_of_inf_isomorphism [constructor] (φ : G₁ ≃∞g G₂) : G₁ ≃ G₂ := - equiv.mk φ _ - - definition pequiv_of_inf_isomorphism [constructor] (φ : G₁ ≃∞g G₂) : - G₁ ≃* G₂ := - pequiv.mk φ begin esimp, exact _ end begin esimp, exact to_respect_one_inf φ end - - definition inf_isomorphism_of_equiv [constructor] (φ : G₁ ≃ G₂) - (p : Πg₁ g₂, φ (g₁ * g₂) = φ g₁ * φ g₂) : G₁ ≃∞g G₂ := - inf_isomorphism.mk (inf_homomorphism.mk φ p) !to_is_equiv - - definition inf_isomorphism_of_eq [constructor] {G₁ G₂ : InfGroup} (φ : G₁ = G₂) : G₁ ≃∞g G₂ := - inf_isomorphism_of_equiv (equiv_of_eq (ap InfGroup.carrier φ)) - begin intros, induction φ, reflexivity end - - definition to_ginv_inf [constructor] (φ : G₁ ≃∞g G₂) : G₂ →∞g G₁ := - inf_homomorphism.mk φ⁻¹ - abstract begin - intro g₁ g₂, apply inj' φ, - rewrite [respect_mul φ, +right_inv φ] - end end - - variable (G) - definition inf_isomorphism.refl [refl] [constructor] : G ≃∞g G := - inf_isomorphism.mk !inf_gid !is_equiv_id - variable {G} - - definition inf_isomorphism.symm [symm] [constructor] (φ : G₁ ≃∞g G₂) : G₂ ≃∞g G₁ := - inf_isomorphism.mk (to_ginv_inf φ) !is_equiv_inv - - definition inf_isomorphism.trans [trans] [constructor] (φ : G₁ ≃∞g G₂) (ψ : G₂ ≃∞g G₃) : G₁ ≃∞g G₃ := - inf_isomorphism.mk (ψ ∘∞g φ) !is_equiv_compose - - definition inf_isomorphism.eq_trans [trans] [constructor] - {G₁ G₂ : InfGroup} {G₃ : InfGroup} (φ : G₁ = G₂) (ψ : G₂ ≃∞g G₃) : G₁ ≃∞g G₃ := - proof inf_isomorphism.trans (inf_isomorphism_of_eq φ) ψ qed - - definition inf_isomorphism.trans_eq [trans] [constructor] - {G₁ : InfGroup} {G₂ G₃ : InfGroup} (φ : G₁ ≃∞g G₂) (ψ : G₂ = G₃) : G₁ ≃∞g G₃ := - inf_isomorphism.trans φ (inf_isomorphism_of_eq ψ) - - postfix `⁻¹ᵍ⁸`:(max + 1) := inf_isomorphism.symm - infixl ` ⬝∞g `:75 := inf_isomorphism.trans - infixl ` ⬝∞gp `:75 := inf_isomorphism.trans_eq - infixl ` ⬝∞pg `:75 := inf_isomorphism.eq_trans - - definition pmap_of_inf_isomorphism [constructor] (φ : G₁ ≃∞g G₂) : G₁ →* G₂ := - pequiv_of_inf_isomorphism φ - - definition to_fun_inf_isomorphism_trans {G H K : InfGroup} (φ : G ≃∞g H) (ψ : H ≃∞g K) : - φ ⬝∞g ψ ~ ψ ∘ φ := - by reflexivity - - definition inf_homomorphism_mul [constructor] {G H : AbInfGroup} (φ ψ : G →∞g H) : G →∞g H := - inf_homomorphism.mk (λg, φ g * ψ g) - abstract begin - intro g g', refine ap011 mul !to_respect_mul_inf !to_respect_mul_inf ⬝ _, - refine !mul.assoc ⬝ ap (mul _) (!mul.assoc⁻¹ ⬝ ap (λx, x * _) !mul.comm ⬝ !mul.assoc) ⬝ - !mul.assoc⁻¹ - end end - - definition trivial_inf_homomorphism (A B : InfGroup) : A →∞g B := - inf_homomorphism.mk (λa, 1) (λa a', (mul_one 1)⁻¹) - - /- given an equivalence A ≃ B we can transport a group structure on A to a group structure on B -/ - - section - - parameters {A B : Type} (f : A ≃ B) [inf_group A] - - definition inf_group_equiv_mul (b b' : B) : B := f (f⁻¹ᶠ b * f⁻¹ᶠ b') - - definition inf_group_equiv_one : B := f one - - definition inf_group_equiv_inv (b : B) : B := f (f⁻¹ᶠ b)⁻¹ - - local infix * := inf_group_equiv_mul - local postfix ^ := inf_group_equiv_inv - local notation 1 := inf_group_equiv_one - - theorem inf_group_equiv_mul_assoc (b₁ b₂ b₃ : B) : (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) := - by rewrite [↑inf_group_equiv_mul, +left_inv f, mul.assoc] - - theorem inf_group_equiv_one_mul (b : B) : 1 * b = b := - by rewrite [↑inf_group_equiv_mul, ↑inf_group_equiv_one, left_inv f, one_mul, right_inv f] - - theorem inf_group_equiv_mul_one (b : B) : b * 1 = b := - by rewrite [↑inf_group_equiv_mul, ↑inf_group_equiv_one, left_inv f, mul_one, right_inv f] - - theorem inf_group_equiv_mul_left_inv (b : B) : b^ * b = 1 := - by rewrite [↑inf_group_equiv_mul, ↑inf_group_equiv_one, ↑inf_group_equiv_inv, - +left_inv f, mul.left_inv] - - definition inf_group_equiv_closed : inf_group B := - ⦃inf_group, - mul := inf_group_equiv_mul, - mul_assoc := inf_group_equiv_mul_assoc, - one := inf_group_equiv_one, - one_mul := inf_group_equiv_one_mul, - mul_one := inf_group_equiv_mul_one, - inv := inf_group_equiv_inv, - mul_left_inv := inf_group_equiv_mul_left_inv⦄ - - end - - section - variables {A B : Type} (f : A ≃ B) [ab_inf_group A] - definition inf_group_equiv_mul_comm (b b' : B) : inf_group_equiv_mul f b b' = inf_group_equiv_mul f b' b := - by rewrite [↑inf_group_equiv_mul, mul.comm] - - definition ab_inf_group_equiv_closed : ab_inf_group B := - ⦃ab_inf_group, inf_group_equiv_closed f, - mul_comm := inf_group_equiv_mul_comm f⦄ - end - - variable (G) - - /- the trivial ∞-group -/ - open unit - definition inf_group_unit [constructor] : inf_group unit := - inf_group.mk (λx y, star) (λx y z, idp) star (unit.rec idp) (unit.rec idp) (λx, star) (λx, idp) - - definition ab_inf_group_unit [constructor] : ab_inf_group unit := - ⦃ab_inf_group, inf_group_unit, mul_comm := λx y, idp⦄ - - definition trivial_inf_group [constructor] : InfGroup := - InfGroup.mk _ inf_group_unit - - definition AbInfGroup_of_InfGroup (G : InfGroup.{u}) (H : Π x y : G, x * y = y * x) : - AbInfGroup.{u} := - begin - induction G, - fapply AbInfGroup.mk, - assumption, - exact ⦃ab_inf_group, struct', mul_comm := H⦄ - end - - definition trivial_ab_inf_group : AbInfGroup.{0} := - begin - fapply AbInfGroup_of_InfGroup trivial_inf_group, intro x y, reflexivity - end - - definition trivial_inf_group_of_is_contr [H : is_contr G] : G ≃∞g trivial_inf_group := - begin - fapply inf_isomorphism_of_equiv, - { apply equiv_unit_of_is_contr}, - { intros, reflexivity} - end - - definition ab_inf_group_of_is_contr (A : Type) [is_contr A] : ab_inf_group A := - have ab_inf_group unit, from ab_inf_group_unit, - ab_inf_group_equiv_closed (equiv_unit_of_is_contr A)⁻¹ᵉ - - definition inf_group_of_is_contr (A : Type) [is_contr A] : inf_group A := - have ab_inf_group A, from ab_inf_group_of_is_contr A, by apply _ - - definition ab_inf_group_lift_unit : ab_inf_group (lift unit) := - ab_inf_group_of_is_contr (lift unit) - - definition trivial_ab_inf_group_lift : AbInfGroup := - AbInfGroup.mk _ ab_inf_group_lift_unit - - definition from_trivial_ab_inf_group (A : AbInfGroup) : trivial_ab_inf_group →∞g A := - trivial_inf_homomorphism trivial_ab_inf_group A - - definition to_trivial_ab_inf_group (A : AbInfGroup) : A →∞g trivial_ab_inf_group := - trivial_inf_homomorphism A trivial_ab_inf_group end group open group namespace fiber - open pointed sigma sigma.ops - -definition loopn_pfiber [constructor] {A B : Type*} (n : ℕ) (f : A →* B) : - Ω[n] (pfiber f) ≃* pfiber (Ω→[n] f) := -begin - induction n with n IH, reflexivity, exact loop_pequiv_loop IH ⬝e* loop_pfiber (Ω→[n] f), -end - -definition fiber_eq_pr2 {A B : Type} {f : A → B} {b : B} {x y : fiber f b} - (p : x = y) : point_eq x = ap f (ap point p) ⬝ point_eq y := -begin induction p, exact !idp_con⁻¹ end - -definition fiber_eq_eta {A B : Type} {f : A → B} {b : B} {x y : fiber f b} - (p : x = y) : p = fiber_eq (ap point p) (fiber_eq_pr2 p) := -begin induction p, induction x with a q, induction q, reflexivity end - -definition fiber_eq_con {A B : Type} {f : A → B} {b : B} {x y z : fiber f b} - (p1 : point x = point y) (p2 : point y = point z) - (q1 : point_eq x = ap f p1 ⬝ point_eq y) (q2 : point_eq y = ap f p2 ⬝ point_eq z) : - fiber_eq p1 q1 ⬝ fiber_eq p2 q2 = - fiber_eq (p1 ⬝ p2) (q1 ⬝ whisker_left (ap f p1) q2 ⬝ !con.assoc⁻¹ ⬝ - whisker_right (point_eq z) (ap_con f p1 p2)⁻¹) := -begin - induction x with a₁ r₁, induction y with a₂ r₂, induction z with a₃ r₃, esimp at *, - induction q2 using eq.rec_symm, induction q1 using eq.rec_symm, - induction p2, induction p1, induction r₃, reflexivity -end - -definition fiber_eq_equiv' [constructor] {A B : Type} {f : A → B} {b : B} (x y : fiber f b) : - (x = y) ≃ (Σ(p : point x = point y), point_eq x = ap f p ⬝ point_eq y) := -@equiv_change_inv _ _ (fiber_eq_equiv x y) (λpq, fiber_eq pq.1 pq.2) - begin intro pq, cases pq, reflexivity end - -definition fiber_eq2_equiv {A B : Type} {f : A → B} {b : B} {x y : fiber f b} - (p₁ p₂ : point x = point y) (q₁ : point_eq x = ap f p₁ ⬝ point_eq y) - (q₂ : point_eq x = ap f p₂ ⬝ point_eq y) : (fiber_eq p₁ q₁ = fiber_eq p₂ q₂) ≃ - (Σ(r : p₁ = p₂), q₁ ⬝ whisker_right (point_eq y) (ap02 f r) = q₂) := -begin - refine (eq_equiv_fn_eq (fiber_eq_equiv' x y)⁻¹ᵉ _ _)⁻¹ᵉ ⬝e sigma_eq_equiv _ _ ⬝e _, - apply sigma_equiv_sigma_right, esimp, intro r, - refine !eq_pathover_equiv_square ⬝e _, - refine eq_hconcat_equiv !ap_constant ⬝e hconcat_eq_equiv (ap_compose (λx, x ⬝ _) _ _) ⬝e _, - refine !square_equiv_eq ⬝e _, - exact eq_equiv_eq_closed idp (idp_con q₂) -end - -definition fiber_eq2 {A B : Type} {f : A → B} {b : B} {x y : fiber f b} - {p₁ p₂ : point x = point y} {q₁ : point_eq x = ap f p₁ ⬝ point_eq y} - {q₂ : point_eq x = ap f p₂ ⬝ point_eq y} (r : p₁ = p₂) - (s : q₁ ⬝ whisker_right (point_eq y) (ap02 f r) = q₂) : (fiber_eq p₁ q₁ = fiber_eq p₂ q₂) := -(fiber_eq2_equiv p₁ p₂ q₁ q₂)⁻¹ᵉ ⟨r, s⟩ - -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' := -fiber.mk (g (point x)) (H (point x) ⬝ ap h (point_eq x) ⬝ p) - -definition pfiber_functor [constructor] {A A' B B' : Type*} {f : A →* B} {f' : A' →* B'} - (g : A →* A') (h : B →* B') (H : psquare g h f f') : pfiber f →* pfiber f' := -pmap.mk (fiber_functor g h H (respect_pt h)) - begin - fapply fiber_eq, - exact respect_pt g, - exact !con.assoc ⬝ to_homotopy_pt H - end - -definition ppoint_natural {A A' B B' : Type*} {f : A →* B} {f' : A' →* B'} - (g : A →* A') (h : B →* B') (H : psquare g h f f') : - psquare (ppoint f) (ppoint f') (pfiber_functor g h H) g := -begin - fapply phomotopy.mk, - { intro x, reflexivity }, - { refine !idp_con ⬝ _ ⬝ !idp_con⁻¹, esimp, apply point_fiber_eq } -end /- if we need this: do pfiber_functor_pcompose and so on first -/ -- definition psquare_pfiber_functor [constructor] {A₁ A₂ A₃ A₄ B₁ B₂ B₃ B₄ : Type*} @@ -734,87 +190,13 @@ end -- { } -- end --- TODO: use this in pfiber_pequiv_of_phomotopy -definition fiber_equiv_of_homotopy {A B : Type} {f g : A → B} (h : f ~ g) (b : B) - : fiber f b ≃ fiber g b := -begin - refine (fiber.sigma_char f b ⬝e _ ⬝e (fiber.sigma_char g b)⁻¹ᵉ), - apply sigma_equiv_sigma_right, intros a, - apply equiv_eq_closed_left, apply h -end - -definition fiber_equiv_of_square {A B C D : Type} {b : B} {d : D} {f : A → B} {g : C → D} (h : A ≃ C) - (k : B ≃ D) (s : k ∘ f ~ g ∘ h) (p : k b = d) : fiber f b ≃ fiber g d := - calc fiber f b ≃ fiber (k ∘ f) (k b) : fiber.equiv_postcompose - ... ≃ fiber (k ∘ f) d : transport_fiber_equiv (k ∘ f) p - ... ≃ fiber (g ∘ h) d : fiber_equiv_of_homotopy s d - ... ≃ fiber g d : fiber.equiv_precompose - -definition fiber_equiv_of_triangle {A B C : Type} {b : B} {f : A → B} {g : C → B} (h : A ≃ C) - (s : f ~ g ∘ h) : fiber f b ≃ fiber g b := -fiber_equiv_of_square h erfl s idp - -definition is_trunc_fun_id (k : ℕ₋₂) (A : Type) : is_trunc_fun k (@id A) := -λa, is_trunc_of_is_contr _ _ - -definition is_conn_fun_id (k : ℕ₋₂) (A : Type) : is_conn_fun k (@id A) := -λa, _ - -open sigma.ops is_conn -definition fiber_compose {A B C : Type} (g : B → C) (f : A → B) (c : C) : - fiber (g ∘ f) c ≃ Σ(x : fiber g c), fiber f (point x) := -begin - fapply equiv.MK, - { intro x, exact ⟨fiber.mk (f (point x)) (point_eq x), fiber.mk (point x) idp⟩ }, - { intro x, exact fiber.mk (point x.2) (ap g (point_eq x.2) ⬝ point_eq x.1) }, - { intro x, induction x with x₁ x₂, induction x₁ with b p, induction x₂ with a q, - induction p, esimp at q, induction q, reflexivity }, - { intro x, induction x with a p, induction p, reflexivity } -end - -definition is_trunc_fun_compose (k : ℕ₋₂) {A B C : Type} {g : B → C} {f : A → B} - (Hg : is_trunc_fun k g) (Hf : is_trunc_fun k f) : is_trunc_fun k (g ∘ f) := -λc, is_trunc_equiv_closed_rev k (fiber_compose g f c) _ - -definition is_conn_fun_compose (k : ℕ₋₂) {A B C : Type} {g : B → C} {f : A → B} - (Hg : is_conn_fun k g) (Hf : is_conn_fun k f) : is_conn_fun k (g ∘ f) := -λc, is_conn_equiv_closed_rev k (fiber_compose g f c) _ end fiber open fiber -namespace fin - -definition lift_succ2 [constructor] ⦃n : ℕ⦄ (x : fin n) : fin (nat.succ n) := -fin.mk x (le.step (is_lt x)) - -end fin - namespace function variables {A B : Type} {f f' : A → B} open is_conn sigma.ops - definition is_contr_of_is_surjective (f : A → B) (H : is_surjective f) (HA : is_contr A) - (HB : is_set B) : is_contr B := - is_contr.mk (f !center) begin intro b, induction H b, exact ap f !is_prop.elim ⬝ p end - - definition is_surjective_of_is_contr [constructor] (f : A → B) (a : A) (H : is_contr B) : - is_surjective f := - λb, image.mk a !eq_of_is_contr - - definition is_contr_of_is_embedding (f : A → B) (H : is_embedding f) (HB : is_prop B) - (a₀ : A) : is_contr A := - is_contr.mk a₀ (λa, is_injective_of_is_embedding (is_prop.elim (f a₀) (f a))) - - definition merely_constant {A B : Type} (f : A → B) : Type := - Σb, Πa, merely (f a = b) - - definition merely_constant_pmap {A B : Type*} {f : A →* B} (H : merely_constant f) (a : A) : - merely (f a = pt) := - tconcat (tconcat (H.2 a) (tinverse (H.2 pt))) (tr (respect_pt f)) - - definition merely_constant_of_is_conn {A B : Type*} (f : A →* B) [is_conn 0 A] : merely_constant f := - ⟨pt, is_conn.elim -1 _ (tr (respect_pt f))⟩ - definition homotopy_group_isomorphism_of_is_embedding (n : ℕ) [H : is_succ n] {A B : Type*} (f : A →* B) [H2 : is_embedding f] : πg[n] A ≃g πg[n] B := begin @@ -825,17 +207,13 @@ namespace function exact sorry end - definition is_embedding_of_square {A B C D : Type} {f : A → B} {g : C → D} (h : A ≃ C) - (k : B ≃ D) (s : k ∘ f ~ g ∘ h) (Hf : is_embedding f) : is_embedding g := - begin - apply is_embedding_homotopy_closed, exact inv_homotopy_of_homotopy_pre _ _ _ s, - apply is_embedding_compose, apply is_embedding_compose, - apply is_embedding_of_is_equiv, exact Hf, apply is_embedding_of_is_equiv - end + definition merely_constant_pmap {A B : Type*} {f : A →* B} (H : merely_constant f) (a : A) : + merely (f a = pt) := + tconcat (tconcat (H.2 a) (tinverse (H.2 pt))) (tr (respect_pt f)) - definition is_embedding_of_square_rev {A B C D : Type} {f : A → B} {g : C → D} (h : A ≃ C) - (k : B ≃ D) (s : k ∘ f ~ g ∘ h) (Hg : is_embedding g) : is_embedding f := - is_embedding_of_square h⁻¹ᵉ k⁻¹ᵉ s⁻¹ʰᵗʸᵛ Hg + definition merely_constant_of_is_conn {A B : Type*} (f : A →* B) [is_conn 0 A] : + merely_constant f := + ⟨pt, is_conn.elim -1 _ (tr (respect_pt f))⟩ end function open function @@ -843,100 +221,6 @@ namespace is_conn open unit trunc_index nat is_trunc pointed.ops sigma.ops prod.ops -definition is_conn_of_eq {n m : ℕ₋₂} (p : n = m) {A : Type} (H : is_conn n A) : is_conn m A := -transport (λk, is_conn k A) p H - --- todo: make trunc_equiv_trunc_of_is_conn_fun a def. -definition ptrunc_pequiv_ptrunc_of_is_conn_fun {A B : Type*} (n : ℕ₋₂) (f : A →* B) - [H : is_conn_fun n f] : ptrunc n A ≃* ptrunc n B := -pequiv_of_pmap (ptrunc_functor n f) (is_equiv_trunc_functor_of_is_conn_fun n f) - -definition is_conn_zero {A : Type} (a₀ : trunc 0 A) (p : Πa a' : A, ∥ a = a' ∥) : is_conn 0 A := -is_conn_succ_intro a₀ (λa a', is_conn_minus_one _ (p a a')) - -definition is_conn_zero_pointed {A : Type*} (p : Πa a' : A, ∥ a = a' ∥) : is_conn 0 A := -is_conn_zero (tr pt) p - -definition is_conn_zero_pointed' {A : Type*} (p : Πa : A, ∥ a = pt ∥) : is_conn 0 A := -is_conn_zero_pointed (λa a', tconcat (p a) (tinverse (p a'))) - -definition is_conn_fiber (n : ℕ₋₂) {A B : Type} (f : A → B) (b : B) [is_conn n A] - [is_conn (n.+1) B] : is_conn n (fiber f b) := -is_conn_equiv_closed_rev _ !fiber.sigma_char _ - -definition is_conn_succ_of_is_conn_loop {n : ℕ₋₂} {A : Type*} - (H : is_conn 0 A) (H2 : is_conn n (Ω A)) : is_conn (n.+1) A := -begin - apply is_conn_succ_intro, exact tr pt, - intros a a', - induction merely_of_minus_one_conn (is_conn_eq -1 a a') with p, induction p, - induction merely_of_minus_one_conn (is_conn_eq -1 pt a) with p, induction p, - exact H2 -end - -definition is_conn_fun_compose {n : ℕ₋₂} {A B C : Type} (g : B → C) (f : A → B) - (H : is_conn_fun n g) (K : is_conn_fun n f) : is_conn_fun n (g ∘ f) := -sorry - -definition pconntype.sigma_char [constructor] (k : ℕ₋₂) : - Type*[k] ≃ Σ(X : Type*), is_conn k X := -equiv.MK (λX, ⟨pconntype.to_pType X, _⟩) - (λX, pconntype.mk (carrier X.1) X.2 pt) - begin intro X, induction X with X HX, induction X, reflexivity end - begin intro X, induction X, reflexivity end - -definition is_embedding_pconntype_to_pType (k : ℕ₋₂) : is_embedding (@pconntype.to_pType k) := -begin - intro X Y, fapply is_equiv_of_equiv_of_homotopy, - { exact eq_equiv_fn_eq (pconntype.sigma_char k) _ _ ⬝e subtype_eq_equiv _ _ }, - intro p, induction p, reflexivity -end - -definition pconntype_eq_equiv {k : ℕ₋₂} (X Y : Type*[k]) : (X = Y) ≃ (X ≃* Y) := -equiv.mk _ (is_embedding_pconntype_to_pType k X Y) ⬝e pType_eq_equiv X Y - -definition pconntype_eq {k : ℕ₋₂} {X Y : Type*[k]} (e : X ≃* Y) : X = Y := -(pconntype_eq_equiv X Y)⁻¹ᵉ e - -definition ptruncconntype.sigma_char [constructor] (n k : ℕ₋₂) : - n-Type*[k] ≃ Σ(X : Type*), is_trunc n X × is_conn k X := -equiv.MK (λX, ⟨ptruncconntype._trans_of_to_pconntype_1 X, (_, _)⟩) - (λX, ptruncconntype.mk (carrier X.1) X.2.1 pt X.2.2) - begin intro X, induction X with X HX, induction HX, induction X, reflexivity end - begin intro X, induction X, reflexivity end - -definition ptruncconntype.sigma_char_pconntype [constructor] (n k : ℕ₋₂) : - n-Type*[k] ≃ Σ(X : Type*[k]), is_trunc n X := -equiv.MK (λX, ⟨ptruncconntype.to_pconntype X, _⟩) - (λX, ptruncconntype.mk (pconntype._trans_of_to_pType X.1) X.2 pt _) - begin intro X, induction X with X HX, induction HX, induction X, reflexivity end - begin intro X, induction X, reflexivity end - -definition is_embedding_ptruncconntype_to_pconntype (n k : ℕ₋₂) : - is_embedding (@ptruncconntype.to_pconntype n k) := -begin - intro X Y, fapply is_equiv_of_equiv_of_homotopy, - { exact eq_equiv_fn_eq (ptruncconntype.sigma_char_pconntype n k) _ _ ⬝e subtype_eq_equiv _ _ }, - intro p, induction p, reflexivity -end - -definition ptruncconntype_eq_equiv {n k : ℕ₋₂} (X Y : n-Type*[k]) : (X = Y) ≃ (X ≃* Y) := -equiv.mk _ (is_embedding_ptruncconntype_to_pconntype n k X Y) ⬝e -pconntype_eq_equiv X Y - -/- duplicate -/ -definition ptruncconntype_eq {n k : ℕ₋₂} {X Y : n-Type*[k]} (e : X ≃* Y) : X = Y := -(ptruncconntype_eq_equiv X Y)⁻¹ᵉ e - -definition ptruncconntype_functor [constructor] {n n' k k' : ℕ₋₂} (p : n = n') (q : k = k') - (X : n-Type*[k]) : n'-Type*[k'] := -ptruncconntype.mk X (is_trunc_of_eq p _) pt (is_conn_of_eq q _) - -definition ptruncconntype_equiv [constructor] {n n' k k' : ℕ₋₂} (p : n = n') (q : k = k') : - n-Type*[k] ≃ n'-Type*[k'] := -equiv.MK (ptruncconntype_functor p q) (ptruncconntype_functor p⁻¹ q⁻¹) - (λX, ptruncconntype_eq pequiv.rfl) (λX, ptruncconntype_eq pequiv.rfl) - -- definition is_conn_pfiber_of_equiv_on_homotopy_groups (n : ℕ) {A B : pType.{u}} (f : A →* B) -- [H : is_conn 0 A] -- (H1 : Πk, k ≤ n → is_equiv (π→[k] f)) @@ -947,204 +231,8 @@ equiv.MK (ptruncconntype_functor p q) (ptruncconntype_functor p⁻¹ q⁻¹) -- definition is_conn_pelim [constructor] {k : ℕ} {X : Type*} (Y : Type*) (H : is_conn k X) : -- (X →* connect k Y) ≃ (X →* Y) := -/- the k-connected cover of X, the fiber of the map X → ∥X∥ₖ. -/ -definition connect (k : ℕ) (X : Type*) : Type* := -pfiber (ptr k X) - -definition is_conn_connect (k : ℕ) (X : Type*) : is_conn k (connect k X) := -is_conn_fun_tr k X (tr pt) - -definition connconnect [constructor] (k : ℕ) (X : Type*) : Type*[k] := -pconntype.mk (connect k X) (is_conn_connect k X) pt - -definition connect_intro [constructor] {k : ℕ} {X : Type*} {Y : Type*} (H : is_conn k X) - (f : X →* Y) : X →* connect k Y := -pmap.mk (λx, fiber.mk (f x) (is_conn.elim (k.-1) _ (ap tr (respect_pt f)) x)) - begin - fapply fiber_eq, exact respect_pt f, apply is_conn.elim_β - end - -definition ppoint_connect_intro [constructor] {k : ℕ} {X : Type*} {Y : Type*} (H : is_conn k X) - (f : X →* Y) : ppoint (ptr k Y) ∘* connect_intro H f ~* f := -begin - induction f with f f₀, induction Y with Y y₀, esimp at (f,f₀), induction f₀, - fapply phomotopy.mk, - { intro x, reflexivity }, - { symmetry, esimp, apply point_fiber_eq } -end - -definition connect_intro_ppoint [constructor] {k : ℕ} {X : Type*} {Y : Type*} (H : is_conn k X) - (f : X →* connect k Y) : connect_intro H (ppoint (ptr k Y) ∘* f) ~* f := -begin - cases f with f f₀, - fapply phomotopy.mk, - { intro x, fapply fiber_eq, reflexivity, - refine @is_conn.elim (k.-1) _ _ _ (λx', !is_trunc_eq) _ x, - refine !is_conn.elim_β ⬝ _, - refine _ ⬝ !idp_con⁻¹, - symmetry, refine _ ⬝ !con_idp, exact fiber_eq_pr2 f₀ }, - { esimp, refine whisker_left _ !fiber_eq_eta ⬝ !fiber_eq_con ⬝ apd011 fiber_eq !idp_con _, esimp, - apply eq_pathover_constant_left, - refine whisker_right _ (whisker_right _ (whisker_right _ !is_conn.elim_β)) ⬝pv _, - esimp [connect], refine _ ⬝vp !con_idp, - apply move_bot_of_left, refine !idp_con ⬝ !con_idp⁻¹ ⬝ph _, - refine !con.assoc ⬝ !con.assoc ⬝pv _, apply whisker_tl, - note r := eq_bot_of_square (transpose (whisker_left_idp_square (fiber_eq_pr2 f₀))⁻¹ᵛ), - refine !con.assoc⁻¹ ⬝ whisker_right _ r⁻¹ ⬝pv _, clear r, - apply move_top_of_left, - refine whisker_right_idp (ap_con tr idp (ap point f₀))⁻¹ᵖ ⬝pv _, - exact (ap_con_idp_left tr (ap point f₀))⁻¹ʰ } -end - -definition connect_intro_equiv [constructor] {k : ℕ} {X : Type*} (Y : Type*) (H : is_conn k X) : - (X →* connect k Y) ≃ (X →* Y) := -begin - fapply equiv.MK, - { intro f, exact ppoint (ptr k Y) ∘* f }, - { intro g, exact connect_intro H g }, - { intro g, apply eq_of_phomotopy, exact ppoint_connect_intro H g }, - { intro f, apply eq_of_phomotopy, exact connect_intro_ppoint H f } -end - -definition connect_intro_pequiv [constructor] {k : ℕ} {X : Type*} (Y : Type*) (H : is_conn k X) : - ppmap X (connect k Y) ≃* ppmap X Y := -pequiv_of_equiv (connect_intro_equiv Y H) (eq_of_phomotopy !pcompose_pconst) - -definition connect_pequiv {k : ℕ} {X : Type*} (H : is_conn k X) : connect k X ≃* X := -@pfiber_pequiv_of_is_contr _ _ (ptr k X) H - -definition loop_connect (k : ℕ) (X : Type*) : Ω (connect (k+1) X) ≃* connect k (Ω X) := -loop_pfiber (ptr (k+1) X) ⬝e* -pfiber_pequiv_of_square pequiv.rfl (loop_ptrunc_pequiv k X) - (phomotopy_of_phomotopy_pinv_left (ap1_ptr k X)) - -definition loopn_connect (k : ℕ) (X : Type*) : Ω[k+1] (connect k X) ≃* Ω[k+1] X := -loopn_pfiber (k+1) (ptr k X) ⬝e* -@pfiber_pequiv_of_is_contr _ _ _ (@is_contr_loop_of_is_trunc (k+1) _ !is_trunc_trunc) - -definition is_conn_of_is_conn_succ_nat (n : ℕ) (A : Type) [is_conn (n+1) A] : is_conn n A := -is_conn_of_is_conn_succ n A - -definition connect_functor (k : ℕ) {X Y : Type*} (f : X →* Y) : connect k X →* connect k Y := -pfiber_functor f (ptrunc_functor k f) (ptr_natural k f)⁻¹* - -definition connect_intro_pequiv_natural {k : ℕ} {X X' : Type*} {Y Y' : Type*} (f : X' →* X) - (g : Y →* Y') (H : is_conn k X) (H' : is_conn k X') : - psquare (connect_intro_pequiv Y H) (connect_intro_pequiv Y' H') - (ppcompose_left (connect_functor k g) ∘* ppcompose_right f) - (ppcompose_left g ∘* ppcompose_right f) := -begin - refine _ ⬝v* _, exact connect_intro_pequiv Y H', - { fapply phomotopy.mk, - { intro h, apply eq_of_phomotopy, apply passoc }, - { xrewrite [▸*, pcompose_right_eq_of_phomotopy, pcompose_left_eq_of_phomotopy, - -+eq_of_phomotopy_trans], - apply ap eq_of_phomotopy, apply passoc_pconst_middle }}, - { fapply phomotopy.mk, - { intro h, apply eq_of_phomotopy, - refine !passoc⁻¹* ⬝* pwhisker_right h (ppoint_natural _ _ _) ⬝* !passoc }, - { xrewrite [▸*, +pcompose_left_eq_of_phomotopy, -+eq_of_phomotopy_trans], - apply ap eq_of_phomotopy, - refine !trans_assoc ⬝ idp ◾** !passoc_pconst_right ⬝ _, - refine !trans_assoc ⬝ idp ◾** !pcompose_pconst_phomotopy ⬝ _, - apply symm_trans_eq_of_eq_trans, symmetry, apply passoc_pconst_right }} -end - end is_conn -namespace misc - open is_conn - - open sigma.ops pointed trunc_index - - /- this is equivalent to pfiber (A → ∥A∥₀) ≡ connect 0 A -/ - definition component [constructor] (A : Type*) : Type* := - pType.mk (Σ(a : A), merely (pt = a)) ⟨pt, tr idp⟩ - - lemma is_conn_component [instance] (A : Type*) : is_conn 0 (component A) := - is_conn_zero_pointed' - begin intro x, induction x with a p, induction p with p, induction p, exact tidp end - - definition component_incl [constructor] (A : Type*) : component A →* A := - pmap.mk pr1 idp - - definition is_embedding_component_incl [instance] (A : Type*) : is_embedding (component_incl A) := - is_embedding_pr1 _ - - definition component_intro [constructor] {A B : Type*} (f : A →* B) (H : merely_constant f) : - A →* component B := - begin - fapply pmap.mk, - { intro a, refine ⟨f a, _⟩, exact tinverse (merely_constant_pmap H a) }, - exact subtype_eq !respect_pt - end - - definition component_functor [constructor] {A B : Type*} (f : A →* B) : component A →* component B := - component_intro (f ∘* component_incl A) !merely_constant_of_is_conn - - -- definition component_elim [constructor] {A B : Type*} (f : A →* B) (H : merely_constant f) : - -- A →* component B := - -- begin - -- fapply pmap.mk, - -- { intro a, refine ⟨f a, _⟩, exact tinverse (merely_constant_pmap H a) }, - -- exact subtype_eq !respect_pt - -- end - - definition loop_component (A : Type*) : Ω (component A) ≃* Ω A := - loop_pequiv_loop_of_is_embedding (component_incl A) - - lemma loopn_component (n : ℕ) (A : Type*) : Ω[n+1] (component A) ≃* Ω[n+1] A := - !loopn_succ_in ⬝e* loopn_pequiv_loopn n (loop_component A) ⬝e* !loopn_succ_in⁻¹ᵉ* - - -- lemma fundamental_group_component (A : Type*) : π₁ (component A) ≃g π₁ A := - -- isomorphism_of_equiv (trunc_equiv_trunc 0 (loop_component A)) _ - - lemma homotopy_group_component (n : ℕ) (A : Type*) : πg[n+1] (component A) ≃g πg[n+1] A := - homotopy_group_isomorphism_of_is_embedding (n+1) (component_incl A) - - definition is_trunc_component [instance] (n : ℕ₋₂) (A : Type*) [is_trunc n A] : - is_trunc n (component A) := - begin - apply @is_trunc_sigma, intro a, cases n with n, - { apply is_contr_of_inhabited_prop, exact tr !is_prop.elim }, - { apply is_trunc_succ_of_is_prop }, - end - - definition ptrunc_component' (n : ℕ₋₂) (A : Type*) : - ptrunc (n.+2) (component A) ≃* component (ptrunc (n.+2) A) := - begin - fapply pequiv.MK', - { exact ptrunc.elim (n.+2) (component_functor !ptr) }, - { intro x, cases x with x p, induction x with a, - refine tr ⟨a, _⟩, - note q := trunc_functor -1 !tr_eq_tr_equiv p, - exact trunc_trunc_equiv_left _ !minus_one_le_succ q }, - { exact sorry }, - { exact sorry } - end - - definition ptrunc_component (n : ℕ₋₂) (A : Type*) : - ptrunc n (component A) ≃* component (ptrunc n A) := - begin - cases n with n, exact sorry, - cases n with n, exact sorry, - exact ptrunc_component' n A - end - - definition break_into_components (A : Type) : A ≃ Σ(x : trunc 0 A), Σ(a : A), ∥ tr a = x ∥ := - calc - A ≃ Σ(a : A) (x : trunc 0 A), tr a = x : - by exact (@sigma_equiv_of_is_contr_right _ _ (λa, !is_contr_sigma_eq))⁻¹ᵉ - ... ≃ Σ(x : trunc 0 A) (a : A), tr a = x : - by apply sigma_comm_equiv - ... ≃ Σ(x : trunc 0 A), Σ(a : A), ∥ tr a = x ∥ : - by exact sigma_equiv_sigma_right (λx, sigma_equiv_sigma_right (λa, !trunc_equiv⁻¹ᵉ)) - - definition pfiber_pequiv_component_of_is_contr [constructor] {A B : Type*} (f : A →* B) [is_contr B] - /- extra condition, something like trunc_functor 0 f is an embedding -/ : pfiber f ≃* component A := - sorry - -end misc namespace sphere @@ -1160,418 +248,13 @@ namespace sphere end sphere -section injective_surjective -open trunc fiber image - - /- do we want to prove this without funext before we move it? -/ - variables {A B C : Type} (f : A → B) - definition is_embedding_factor [is_set A] [is_set B] (g : B → C) (h : A → C) (H : g ∘ f ~ h) : - is_embedding h → is_embedding f := - begin - induction H using homotopy.rec_on_idp, - intro E, - fapply is_embedding_of_is_injective, - intro x y p, - fapply @is_injective_of_is_embedding _ _ _ E _ _ (ap g p) - end - - definition is_surjective_factor (g : B → C) (h : A → C) (H : g ∘ f ~ h) : - is_surjective h → is_surjective g := - begin - induction H using homotopy.rec_on_idp, - intro S, - intro c, - note p := S c, - induction p, - apply tr, - fapply fiber.mk, - exact f a, - exact p - end - -end injective_surjective - --- Yuri Sulyma's code from HoTT MRC - -definition ap1_phomotopy_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : (Ω⇒ p)⁻¹* = Ω⇒ (p⁻¹*) := -begin - induction p using phomotopy_rec_idp, - rewrite ap1_phomotopy_refl, - xrewrite [+refl_symm], - rewrite ap1_phomotopy_refl -end - -definition ap1_phomotopy_trans {A B : Type*} {f g h : A →* B} (q : g ~* h) (p : f ~* g) : Ω⇒ (p ⬝* q) = Ω⇒ p ⬝* Ω⇒ q := -begin - induction p using phomotopy_rec_idp, - induction q using phomotopy_rec_idp, - rewrite trans_refl, - rewrite [+ap1_phomotopy_refl], - rewrite trans_refl -end - -namespace pointed - - definition pbool_pequiv_add_point_unit [constructor] : pbool ≃* unit₊ := - pequiv_of_equiv (bool_equiv_option_unit) idp - - definition to_homotopy_pt_mk {A B : Type*} {f g : A →* B} (h : f ~ g) - (p : h pt ⬝ respect_pt g = respect_pt f) : to_homotopy_pt (phomotopy.mk h p) = p := - to_right_inv !eq_con_inv_equiv_con_eq p - - - variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*} - {f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂} - {f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂} - definition psquare_transpose (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare f₀₁ f₂₁ f₁₀ f₁₂ := p⁻¹* - -end pointed - -namespace pi - definition pi_bool_left_nat {A B : bool → Type} (g : Πx, A x -> B x) : - hsquare (pi_bool_left A) (pi_bool_left B) (pi_functor_right g) (prod_functor (g ff) (g tt)) := - begin intro h, esimp end - - definition pi_bool_left_inv_nat {A B : bool → Type} (g : Πx, A x -> B x) : - hsquare (pi_bool_left A)⁻¹ᵉ (pi_bool_left B)⁻¹ᵉ (prod_functor (g ff) (g tt)) (pi_functor_right g) := hhinverse (pi_bool_left_nat g) - -end pi - -namespace sum - - infix ` +→ `:62 := sum_functor - - variables {A₀₀ A₂₀ A₀₂ A₂₂ B₀₀ B₂₀ B₀₂ B₂₂ A A' B B' C C' : Type} - {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 - - definition sum_functor_hsquare [unfold 19] (h : hsquare f₁₀ f₁₂ f₀₁ f₂₁) - (k : hsquare g₁₀ g₁₂ g₀₁ g₂₁) : hsquare (f₁₀ +→ g₁₀) (f₁₂ +→ g₁₂) (f₀₁ +→ g₀₁) (f₂₁ +→ g₂₁) := - sum_rec_hsquare (λa, ap inl (h a)) (λb, ap inr (k b)) - - definition sum_functor_compose (g : B → C) (f : A → B) (g' : B' → C') (f' : A' → B') : - (g ∘ f) +→ (g' ∘ f') ~ g +→ g' ∘ f +→ f' := - begin intro x, induction x with a a': reflexivity end - - definition sum_rec_sum_functor (g : B → C) (g' : B' → C) (f : A → B) (f' : A' → B') : - sum.rec g g' ∘ sum_functor f f' ~ sum.rec (g ∘ f) (g' ∘ f') := - begin intro x, induction x with a a': reflexivity end - - definition sum_rec_same_compose (g : B → C) (f : A → B) : - sum.rec (g ∘ f) (g ∘ f) ~ g ∘ sum.rec f f := - begin intro x, induction x with a a': reflexivity end - - definition sum_rec_same (f : A → B) : - sum.rec f f ~ f ∘ sum.rec id id := - sum_rec_same_compose f id - -end sum - -namespace prod - - infix ` ×→ `:63 := prod_functor - infix ` ×≃ `:63 := prod_equiv_prod - - definition pprod_incl1 [constructor] (X Y : Type*) : X →* X ×* Y := pmap.mk (λx, (x, pt)) idp - definition pprod_incl2 [constructor] (X Y : Type*) : Y →* X ×* Y := pmap.mk (λy, (pt, y)) idp - -end prod - -namespace equiv - - definition rec_eq_of_equiv {A : Type} {P : A → A → Type} (e : Πa a', a = a' ≃ P a a') - {a a' : A} (Q : P a a' → Type) (H : Π(q : a = a'), Q (e a a' q)) : - Π(p : P a a'), Q p := - equiv_rect (e a a') Q H - - definition rec_idp_of_equiv {A : Type} {P : A → A → Type} (e : Πa a', a = a' ≃ P a a') {a : A} - (r : P a a) (s : e a a idp = r) (Q : Πa', P a a' → Type) (H : Q a r) ⦃a' : A⦄ (p : P a a') : - Q a' p := - rec_eq_of_equiv e _ begin intro q, induction q, induction s, exact H end p - - definition rec_idp_of_equiv_idp {A : Type} {P : A → A → Type} (e : Πa a', a = a' ≃ P a a') {a : A} - (r : P a a) (s : e a a idp = r) (Q : Πa', P a a' → Type) (H : Q a r) : - rec_idp_of_equiv e r s Q H r = H := - begin - induction s, refine !is_equiv_rect_comp ⬝ _, reflexivity - 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 chain_complex - -open fin -definition LES_is_contr_of_is_embedding_of_is_surjective (n : ℕ) {X Y : pType.{u}} (f : X →* Y) - (H : is_embedding (π→[n] f)) (H2 : is_surjective (π→[n+1] f)) : is_contr (π[n] (pfiber f)) := -begin - rexact @is_contr_of_is_embedding_of_is_surjective +3ℕ (LES_of_homotopy_groups f) (n, 0) - (is_exact_LES_of_homotopy_groups f _) proof H qed proof H2 qed -end - -end chain_complex - -namespace susp -open trunc_index -/- move to freudenthal -/ -definition freudenthal_pequiv_trunc_index' (A : Type*) (n : ℕ) (k : ℕ₋₂) [HA : is_conn n A] - (H : k ≤ of_nat (2 * n)) : ptrunc k A ≃* ptrunc k (Ω (susp A)) := -begin - assert lem : Π(l : ℕ₋₂), l ≤ 0 → ptrunc l A ≃* ptrunc l (Ω (susp A)), - { intro l H', exact ptrunc_pequiv_ptrunc_of_le H' (freudenthal_pequiv (zero_le (2 * n)) A) }, - cases k with k, { exact lem -2 (minus_two_le 0) }, - cases k with k, { exact lem -1 (succ_le_succ (minus_two_le -1)) }, - rewrite [-of_nat_add_two at *, add_two_sub_two at HA], - exact freudenthal_pequiv (le_of_of_nat_le_of_nat H) A -end - -end susp - -/- 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 - -namespace category - open functor - /- shortening pullback to pb to keep names relatively short -/ - definition pb_precategory [constructor] {A B : Type} (f : A → B) (C : precategory B) : - precategory A := - precategory.mk (λa a', hom (f a) (f a')) (λa a' a'' h g, h ∘ g) (λa, ID (f a)) - (λa a' a'' a''' k h g, assoc k h g) (λa a' g, id_left g) (λa a' g, id_right g) - - definition pb_Precategory [constructor] {A : Type} (C : Precategory) (f : A → C) : - Precategory := - Precategory.mk A (pb_precategory f C) - - definition pb_Precategory_functor [constructor] {A : Type} (C : Precategory) (f : A → C) : - pb_Precategory C f ⇒ C := - functor.mk f (λa a' g, g) proof (λa, idp) qed proof (λa a' a'' h g, idp) qed - - definition fully_faithful_pb_Precategory_functor {A : Type} (C : Precategory) - (f : A → C) : fully_faithful (pb_Precategory_functor C f) := - begin intro a a', apply is_equiv_id end - - definition split_essentially_surjective_pb_Precategory_functor {A : Type} (C : Precategory) - (f : A → C) (H : is_split_surjective f) : - split_essentially_surjective (pb_Precategory_functor C f) := - begin intro c, cases H c with a p, exact ⟨a, iso.iso_of_eq p⟩ end - - definition is_equivalence_pb_Precategory_functor {A : Type} (C : Precategory) - (f : A → C) (H : is_split_surjective f) : is_equivalence (pb_Precategory_functor C f) := - @(is_equivalence_of_fully_faithful_of_split_essentially_surjective _) - (fully_faithful_pb_Precategory_functor C f) - (split_essentially_surjective_pb_Precategory_functor C f H) - - definition pb_Precategory_equivalence [constructor] {A : Type} (C : Precategory) (f : A → C) - (H : is_split_surjective f) : pb_Precategory C f ≃c C := - equivalence.mk _ (is_equivalence_pb_Precategory_functor C f H) - - definition pb_Precategory_equivalence_of_equiv [constructor] {A : Type} (C : Precategory) - (f : A ≃ C) : pb_Precategory C f ≃c C := - pb_Precategory_equivalence C f (is_split_surjective_of_is_retraction f) - - definition is_isomorphism_pb_Precategory_functor [constructor] {A : Type} (C : Precategory) - (f : A ≃ C) : is_isomorphism (pb_Precategory_functor C f) := - (fully_faithful_pb_Precategory_functor C f, to_is_equiv f) - - definition pb_Precategory_isomorphism [constructor] {A : Type} (C : Precategory) (f : A ≃ C) : - pb_Precategory C f ≅c C := - isomorphism.mk _ (is_isomorphism_pb_Precategory_functor C f) - -end category - -namespace chain_complex - open fin - definition is_contr_homotopy_group_fiber {A B : pType.{u}} {f : A →* B} {n : ℕ} - (H1 : is_embedding (π→[n] f)) (H2 : is_surjective (π→g[n+1] f)) : is_contr (π[n] (pfiber f)) := - begin - apply @is_contr_of_is_embedding_of_is_surjective +3ℕ (LES_of_homotopy_groups f) (n, 0), - exact is_exact_LES_of_homotopy_groups f (n, 1), exact H1, exact H2 - end - - definition is_contr_homotopy_group_fiber_of_is_equiv {A B : pType.{u}} {f : A →* B} {n : ℕ} - (H1 : is_equiv (π→[n] f)) (H2 : is_equiv (π→g[n+1] f)) : is_contr (π[n] (pfiber f)) := - is_contr_homotopy_group_fiber (is_embedding_of_is_equiv _) (is_surjective_of_is_equiv _) - -end chain_complex diff --git a/pointed_pi.hlean b/pointed_pi.hlean index a44015b..9f64d9a 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -269,7 +269,7 @@ namespace pointed fapply phomotopy.mk, { intro x, reflexivity }, { refine !idp_con ⬝ _, esimp, - refine whisker_right _ !ap_sigma_functor_eq_dpair ⬝ _, + refine whisker_right _ !ap_sigma_functor_sigma_eq ⬝ _, induction f₁ with f₁ f₁₀, induction f₂ with f₂ f₂₀, induction A₂ with A₂ a₂₀, induction A₃ with A₃ a₃₀, esimp at * ⊢, induction p₁, induction p₂, reflexivity } end @@ -977,10 +977,11 @@ open is_trunc is_conn namespace is_conn section + /- todo: reorder arguments and make some implicit -/ variables (A : Type*) (n : ℕ₋₂) (H : is_conn (n.+1) A) include H - definition is_contr_ppi_match (P : A → Type*) (H : Πa, is_trunc (n.+1) (P a)) + definition is_contr_ppi_match (P : A → Type*) (H2 : Πa, is_trunc (n.+1) (P a)) : is_contr (Π*(a : A), P a) := begin apply is_contr.mk pt, @@ -997,7 +998,7 @@ namespace is_conn (P : A → Type*) (H3 : Πa, is_trunc l (P a)) : is_trunc k.+1 (Π*(a : A), P a) := begin - have H4 : Πa, is_trunc (n.+1+2+k) (P a), from λa, is_trunc_of_le (P a) H2, + have H4 : Πa, is_trunc (n.+1+2+k) (P a), from λa, is_trunc_of_le (P a) H2 _, clear H2 H3, revert P H4, induction k with k IH: intro P H4, { apply is_prop_of_imp_is_contr, intro f, @@ -1012,11 +1013,24 @@ namespace is_conn definition is_trunc_pmap_of_is_conn (k l : ℕ₋₂) (B : Type*) (H2 : l ≤ n.+1+2+k) (H3 : is_trunc l B) : is_trunc k.+1 (A →* B) := - is_trunc_equiv_closed k.+1 (pppi_equiv_pmap A B) - (is_trunc_ppi_of_is_conn A n H k l H2 (λ a, B) _) + is_trunc_ppi_of_is_conn A n H k l H2 (λ a, B) _ end + open trunc_index algebra nat + definition is_trunc_ppi_of_is_conn_nat + (A : Type*) (n : ℕ) (H : is_conn (n.-1) A) (k l : ℕ) (H2 : l ≤ n + k) + (P : A → Type*) (H3 : Πa, is_trunc l (P a)) : + is_trunc k (Π*(a : A), P a) := + begin + refine is_trunc_ppi_of_is_conn A (n.-2) H (k.-1) l _ P H3, + refine le.trans (of_nat_le_of_nat H2) (le_of_eq !sub_one_add_plus_two_sub_one⁻¹) + end + + definition is_trunc_pmap_of_is_conn_nat (A : Type*) (n : ℕ) (H : is_conn (n.-1) A) (k l : ℕ) + (B : Type*) (H2 : l ≤ n + k) (H3 : is_trunc l B) : is_trunc k (A →* B) := + is_trunc_ppi_of_is_conn_nat A n H k l H2 (λ a, B) _ + -- this is probably much easier to prove directly definition is_trunc_ppi (A : Type*) (n k : ℕ₋₂) (H : n ≤ k) (P : A → Type*) (H2 : Πa, is_trunc n (P a)) : is_trunc k (Π*(a : A), P a) := diff --git a/spectrum/smash.hlean b/spectrum/smash.hlean index c986aa5..61392ad 100644 --- a/spectrum/smash.hlean +++ b/spectrum/smash.hlean @@ -19,7 +19,7 @@ definition smash_prespectrum_fun {X X' : Type*} {Y Y' : prespectrum} (f : X →* smap.mk (λn, smash_functor f (g n)) begin intro n, refine susp_to_loop_psquare _ _ _ _ _, - refine pvconcat (psquare_transpose (phinverse (smash_susp_natural f (g n)))) _, + refine pvconcat (ptranspose (phinverse (smash_susp_natural f (g n)))) _, refine vconcat_phomotopy _ (smash_functor_split f (g (S n))), refine phomotopy_vconcat (smash_functor_split f (susp_functor (g n))) _, refine phconcat _ _, diff --git a/spectrum/trunc.hlean b/spectrum/trunc.hlean index 3ef4582..de2efef 100644 --- a/spectrum/trunc.hlean +++ b/spectrum/trunc.hlean @@ -107,8 +107,7 @@ begin induction p, exact id end definition is_strunc_of_le {k l : ℤ} (E : spectrum) (H : k ≤ l) : is_strunc k E → is_strunc l E := begin - intro T, intro n, exact is_trunc_of_le (E n) - (maxm2_monotone (algebra.add_le_add_right H n)) + intro T, intro n, exact is_trunc_of_le (E n) (maxm2_monotone (algebra.add_le_add_right H n)) _ end definition is_strunc_pequiv_closed {k : ℤ} {E F : spectrum} (H : Πn, E n ≃* F n) diff --git a/univalent_subcategory.hlean b/univalent_subcategory.hlean index 3add859..5012425 100644 --- a/univalent_subcategory.hlean +++ b/univalent_subcategory.hlean @@ -28,7 +28,7 @@ section univ_subcat definition is_univalent_domain_of_fully_faithful_embedding : is_univalent C := begin intros, - apply homotopy_closed eq_equiv_iso_of_fully_faithful eq_equiv_iso_of_fully_faithful_homot + exact homotopy_closed eq_equiv_iso_of_fully_faithful eq_equiv_iso_of_fully_faithful_homot _ end end univ_subcat @@ -216,7 +216,7 @@ end (m, (i, o)) = (m', (i', o')) ≃ (m ~2 m') := begin have is_set A, from pr1 H, - apply equiv_of_is_prop, + refine equiv_of_is_prop _ _ _ _, { intro p, exact apd100 (eq_pr1 p)}, { intro p, apply prod_eq (eq_of_homotopy2 p), apply prod_eq: esimp [Group_props] at *; esimp,