diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index 966ab6766..336032d94 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -82,6 +82,12 @@ namespace functor (θ : Πc, G c ⟶ F c) (r : Πc, θ c ∘ η c = id) (q : Πc, η c ∘ θ c = id) : F ≅ G := iso.mk (nat_trans.mk η p) (@(is_natural_iso _) (λc, is_iso.mk (θ c) (r c) (q c))) + definition natural_iso.mk' [constructor] + (η : Πc, F c ≅ G c) (p : Π(c c' : C) (f : c ⟶ c'), G f ∘ to_hom (η c) = to_hom (η c') ∘ F f) : + F ≅ G := + natural_iso.MK (λc, to_hom (η c)) p (λc, to_inv (η c)) + (λc, to_left_inverse (η c)) (λc, to_right_inverse (η c)) + end section diff --git a/hott/algebra/category/constructions/fundamental_groupoid.hlean b/hott/algebra/category/constructions/fundamental_groupoid.hlean index de91d0028..b8f99535a 100644 --- a/hott/algebra/category/constructions/fundamental_groupoid.hlean +++ b/hott/algebra/category/constructions/fundamental_groupoid.hlean @@ -29,4 +29,8 @@ namespace category fundamental_groupoid A ⇒ fundamental_groupoid B := functor.mk f (λa a', tap f) (λa, tap_tidp f) (λa₁ a₂ a₃ q p, tap_tcon f p q) + notation `Π₁` := fundamental_groupoid + + notation `Π₁⇒` := fundamental_groupoid_functor + end category diff --git a/hott/algebra/category/constructions/pushout.hlean b/hott/algebra/category/constructions/pushout.hlean index df8640d30..ba94a1fc2 100644 --- a/hott/algebra/category/constructions/pushout.hlean +++ b/hott/algebra/category/constructions/pushout.hlean @@ -196,7 +196,7 @@ namespace category end include η - parameters {F G} + parameters {F G H K} definition Cpushout_functor_reduction_rule [unfold 12] (i : R x x') : Cpushout_functor_ob x ⟶ Cpushout_functor_ob x' := begin @@ -361,7 +361,34 @@ namespace category { exact ap010 natural_map (to_right_inverse η₂) e}}, end + end + open bpushout_prehom_index prod prod.ops is_equiv equiv + definition Cpushout_universal {C D E : Precategory} {X : Category} (F : C ⇒ D) (G : C ⇒ E) + (H : D ⇒ X) (K : E ⇒ X) (η : H ∘f F ≅ K ∘f G) : + is_contr (Σ(L : Cpushout F G ⇒ X) (θ : L ∘f Cpushout_inl F G ≅ H × L ∘f Cpushout_inr F G ≅ K), + Πs, natural_map (to_hom θ.2) (to_fun_ob G s) ∘ to_fun_hom L (class_of [DE (λ c, c) F G s]) ∘ + natural_map (to_inv θ.1) (to_fun_ob F s) = natural_map (to_hom η) s) := + begin + fapply is_contr.mk, + { exact ⟨Cpushout_functor η, (Cpushout_functor_inl η, Cpushout_functor_inr η), + Cpushout_functor_coh η⟩}, + intro v₁, induction v₁ with L v₂, induction v₂ with θ p, induction θ with θ₁ θ₂, + fapply sigma_eq, + { esimp, apply eq_of_iso, symmetry, exact Cpushout_functor_unique η L θ₁ θ₂ p}, + fapply sigma_pathover, + { apply prod_pathover: esimp, + { apply iso_pathover, + apply hom_pathover_functor_left_constant_right (precomposition_functor _ _), + apply nat_trans_eq, intro d, + xrewrite [↑[hom_of_eq], to_right_inv !eq_equiv_iso, ▸*], + exact (ap010 natural_map (to_right_inverse θ₁) d)⁻¹}, + { apply iso_pathover, + apply hom_pathover_functor_left_constant_right (precomposition_functor _ _), + apply nat_trans_eq, intro e, + xrewrite [↑[hom_of_eq], to_right_inv !eq_equiv_iso, ▸*], + exact (ap010 natural_map (to_right_inverse θ₂) e)⁻¹}}, + apply is_prop.elimo end /- Pushout of groupoids with a type of basepoints -/ @@ -416,7 +443,7 @@ namespace category Groupoid_paths (bpushout_hom_rel_index k F G) (bpushout_index_inv k F G) (bpushout_index_reverse k F G) (bpushout_index_li k F G) (bpushout_index_ri k F G) - definition Groupoid_pushout [constructor] : Groupoid := + definition Gpushout [constructor] : Groupoid := Groupoid_bpushout (λc, c) F G end diff --git a/hott/algebra/category/functor/attributes.hlean b/hott/algebra/category/functor/attributes.hlean index eb6adb682..5f25a64c8 100644 --- a/hott/algebra/category/functor/attributes.hlean +++ b/hott/algebra/category/functor/attributes.hlean @@ -10,7 +10,7 @@ Adjoint functors, isomorphisms and equivalences have their own file import .basic function arity -open eq functor trunc prod is_equiv iso equiv function is_trunc +open eq functor trunc prod is_equiv iso equiv function is_trunc sigma namespace category variables {C D E : Precategory} {F : C ⇒ D} {G : D ⇒ C} @@ -20,8 +20,6 @@ namespace category definition fully_faithful [class] (F : C ⇒ D) := Π(c c' : C), is_equiv (@(to_fun_hom F) c c') definition split_essentially_surjective [class] (F : C ⇒ D) := Π(d : D), Σ(c : C), F c ≅ d definition essentially_surjective [class] (F : C ⇒ D) := Π(d : D), ∃(c : C), F c ≅ d - definition is_weak_equivalence [class] (F : C ⇒ D) := - fully_faithful F × essentially_surjective F definition is_equiv_of_fully_faithful [instance] (F : C ⇒ D) [H : fully_faithful F] (c c' : C) : is_equiv (@(to_fun_hom F) c c') := @@ -136,8 +134,9 @@ namespace category : is_prop (essentially_surjective F) := by unfold essentially_surjective; exact _ - theorem is_prop_is_weak_equivalence [instance] (F : C ⇒ D) : is_prop (is_weak_equivalence F) := - by unfold is_weak_equivalence; exact _ + definition essentially_surjective_of_split_essentially_surjective [instance] (F : C ⇒ D) + [H : split_essentially_surjective F] : essentially_surjective F := + λd, tr (H d) definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) := equiv_of_is_prop (λH, (faithful_of_fully_faithful F, full_of_fully_faithful F)) @@ -161,4 +160,36 @@ namespace category (λc', !is_embedding_equiv_is_injective))) -/ + definition fully_faithful_compose (G : D ⇒ E) (F : C ⇒ D) [fully_faithful G] [fully_faithful F] : + fully_faithful (G ∘f F) := + λc c', is_equiv_compose (to_fun_hom G) (to_fun_hom F) + + definition full_compose (G : D ⇒ E) (F : C ⇒ D) [full G] [full F] : full (G ∘f F) := + λc c', is_surjective_compose (to_fun_hom G) (to_fun_hom F) _ _ + + definition faithful_compose (G : D ⇒ E) (F : C ⇒ D) [H₁ : faithful G] [H₂ : faithful F] : + faithful (G ∘f F) := + λc c' f f' p, H₂ (H₁ p) + + definition essentially_surjective_compose (G : D ⇒ E) (F : C ⇒ D) [H₁ : essentially_surjective G] + [H₂ : essentially_surjective F] : essentially_surjective (G ∘f F) := + begin + intro e, + induction H₁ e with v, induction v with d p, + induction H₂ d with w, induction w with c q, + exact exists.intro c (to_fun_iso G q ⬝i p) + end + + definition split_essentially_surjective_compose (G : D ⇒ E) (F : C ⇒ D) + [H₁ : split_essentially_surjective G] [H₂ : split_essentially_surjective F] + : split_essentially_surjective (G ∘f F) := + begin + intro e, induction H₁ e with d p, induction H₂ d with c q, + exact ⟨c, to_fun_iso G q ⬝i p⟩ + end + + /- we get the fact that the identity functor satisfies all these properties via the fact that it + is an isomorphism -/ + + end category diff --git a/hott/algebra/category/functor/basic.hlean b/hott/algebra/category/functor/basic.hlean index 77956ae9b..129972287 100644 --- a/hott/algebra/category/functor/basic.hlean +++ b/hott/algebra/category/functor/basic.hlean @@ -273,4 +273,29 @@ namespace functor ap010_assoc K (H ∘f G) F a], end + definition hom_pathover_functor_left_functor_right {c₁ c₂ : C} {p : c₁ = c₂} (F G : C ⇒ D) + {f₁ : F c₁ ⟶ G c₁} {f₂ : F c₂ ⟶ G c₂} + (q : to_fun_hom G (hom_of_eq p) ∘ f₁ = f₂ ∘ to_fun_hom F (hom_of_eq p)) : f₁ =[p] f₂ := + hom_pathover (hom_whisker_right _ (respect_hom_of_eq G _)⁻¹ ⬝ q ⬝ + hom_whisker_left _ (respect_hom_of_eq F _)) + + definition hom_pathover_constant_left_functor_right {c₁ c₂ : C} {p : c₁ = c₂} {d : D} (F : C ⇒ D) + {f₁ : d ⟶ F c₁} {f₂ : d ⟶ F c₂} (q : to_fun_hom F (hom_of_eq p) ∘ f₁ = f₂) : f₁ =[p] f₂ := + hom_pathover_constant_left (hom_whisker_right _ (respect_hom_of_eq F _)⁻¹ ⬝ q) + + definition hom_pathover_functor_left_constant_right {c₁ c₂ : C} {p : c₁ = c₂} {d : D} (F : C ⇒ D) + {f₁ : F c₁ ⟶ d} {f₂ : F c₂ ⟶ d} (q : f₁ = f₂ ∘ to_fun_hom F (hom_of_eq p)) : f₁ =[p] f₂ := + hom_pathover_constant_right (q ⬝ hom_whisker_left _ (respect_hom_of_eq F _)) + + definition hom_pathover_id_left_functor_right {c₁ c₂ : C} {p : c₁ = c₂} (F : C ⇒ C) + {f₁ : c₁ ⟶ F c₁} {f₂ : c₂ ⟶ F c₂} (q : to_fun_hom F (hom_of_eq p) ∘ f₁ = f₂ ∘ hom_of_eq p) : + f₁ =[p] f₂ := + hom_pathover_id_left (hom_whisker_right _ (respect_hom_of_eq F _)⁻¹ ⬝ q) + + definition hom_pathover_functor_left_id_right {c₁ c₂ : C} {p : c₁ = c₂} (F : C ⇒ C) + {f₁ : F c₁ ⟶ c₁} {f₂ : F c₂ ⟶ c₂} (q : hom_of_eq p ∘ f₁ = f₂ ∘ to_fun_hom F (hom_of_eq p)) : + f₁ =[p] f₂ := + hom_pathover_id_right (q ⬝ hom_whisker_left _ (respect_hom_of_eq F _)) + + end functor diff --git a/hott/algebra/category/functor/equivalence.hlean b/hott/algebra/category/functor/equivalence.hlean index 7d6c3d4a7..e10a2a5f7 100644 --- a/hott/algebra/category/functor/equivalence.hlean +++ b/hott/algebra/category/functor/equivalence.hlean @@ -8,7 +8,7 @@ Functors which are equivalences or isomorphisms import .adjoint -open eq functor iso prod nat_trans is_equiv equiv is_trunc +open eq functor iso prod nat_trans is_equiv equiv is_trunc sigma.ops namespace category variables {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C} @@ -18,6 +18,9 @@ namespace category (is_iso_unit : is_iso η) (is_iso_counit : is_iso ε) + definition is_weak_equivalence [class] (F : C ⇒ D) := + fully_faithful F × essentially_surjective F + abbreviation inverse := @is_equivalence.G postfix ⁻¹ := inverse --a second notation for the inverse, which is not overloaded (there is no unicode superscript F) @@ -33,8 +36,16 @@ namespace category (to_functor : C ⇒ D) (struct : is_isomorphism to_functor) + structure weak_equivalence (C D : Precategory) := + mk' :: (intermediate : Precategory) + (left_functor : intermediate ⇒ C) + (right_functor : intermediate ⇒ D) + [structl : is_weak_equivalence left_functor] + [structr : is_weak_equivalence right_functor] + infix ` ≃c `:25 := equivalence infix ` ≅c `:25 := isomorphism + infix ` ≃w `:25 := weak_equivalence attribute equivalence.struct isomorphism.struct [instance] [priority 1500] attribute equivalence.to_functor isomorphism.to_functor [coercion] @@ -51,8 +62,8 @@ namespace category definition iso_counit (F : C ⇒ D) [H : is_equivalence F] : F ∘f F⁻¹ᴱ ≅ 1 := @(iso.mk _) !is_iso_counit - definition split_essentially_surjective_of_is_equivalence (F : C ⇒ D) - [H : is_equivalence F] : split_essentially_surjective F := + definition split_essentially_surjective_of_is_equivalence [instance] (F : C ⇒ D) + [is_equivalence F] : split_essentially_surjective F := begin intro d, fconstructor, { exact F⁻¹ d}, @@ -131,6 +142,37 @@ namespace category equivalence.mk F is_equivalence.mk end + section + parameters {C D : Precategory} (F : C ⇒ D) + [H₁ : fully_faithful F] [H₂ : split_essentially_surjective F] + + include H₁ H₂ + definition inverse_of_fully_faithful_of_split_essentially_surjective [constructor] : D ⇒ C := + begin + fapply functor.mk, + { exact λd, (H₂ d).1}, + { intro d d' g, apply (to_fun_hom F)⁻¹ᶠ, refine to_inv (H₂ d').2 ∘ g ∘ to_hom (H₂ d).2}, + { intro d, apply inv_eq_of_eq, rewrite [id_left, respect_id, to_left_inverse]}, + { intros d₁ d₂ d₃ g f, apply inv_eq_of_eq, + rewrite [respect_comp, +right_inv (to_fun_hom F), +assoc', comp_inverse_cancel_left]} + end + + definition is_equivalence_of_fully_faithful_of_split_essentially_surjective [constructor] + : is_equivalence F := + begin + fapply is_equivalence.mk, + { exact inverse_of_fully_faithful_of_split_essentially_surjective}, + { fapply natural_iso.mk', + { intro c, esimp, apply reflect_iso F, exact (H₂ (F c)).2}, + intro c c' f, esimp, apply eq_of_fn_eq_fn' (to_fun_hom F), + rewrite [+respect_comp, +right_inv (to_fun_hom F), comp_inverse_cancel_left]}, + { fapply natural_iso.mk', + { intro c, esimp, exact (H₂ c).2}, + intro c c' f, esimp, rewrite [right_inv (to_fun_hom F), comp_inverse_cancel_left]} + end + + end + variables {C D E : Precategory} {F : C ⇒ D} --TODO: add variants @@ -141,8 +183,8 @@ namespace category apply eq_inverse_of_comp_eq_id, apply counit_unit_eq end - definition fully_faithful_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F] - : fully_faithful F := + definition fully_faithful_of_is_equivalence [instance] [constructor] (F : C ⇒ D) + [H : is_equivalence F] : fully_faithful F := begin intro c c', fapply adjointify, @@ -178,10 +220,13 @@ namespace category [H : is_isomorphism F] : is_equiv (to_fun_ob F) := pr2 H - definition is_fully_faithful_of_is_isomorphism [instance] [unfold 4] (F : C ⇒ D) + definition fully_faithful_of_is_isomorphism [unfold 4] (F : C ⇒ D) [H : is_isomorphism F] : fully_faithful F := pr1 H + section + local attribute fully_faithful_of_is_isomorphism [instance] + definition strict_inverse [constructor] (F : C ⇒ D) [H : is_isomorphism F] : D ⇒ C := begin fapply functor.mk, @@ -215,9 +260,10 @@ namespace category { rewrite [adj], rewrite [▸*,respect_inv_of_eq F]}, { rewrite [adj,▸*,respect_hom_of_eq F]}}, end + end - definition is_equivalence_of_is_isomorphism [instance] [constructor] (F : C ⇒ D) [H : is_isomorphism F] - : is_equivalence F := + definition is_equivalence_of_is_isomorphism [instance] [constructor] (F : C ⇒ D) + [is_isomorphism F] : is_equivalence F := begin fapply is_equivalence.mk, { apply F⁻¹ˢ}, @@ -369,6 +415,33 @@ namespace category : c ⟶ c' ≃ H c ⟶ H c' := equiv.mk (to_fun_hom (isomorphism.to_functor H)) _ + /- weak equivalences -/ + + theorem is_prop_is_weak_equivalence [instance] (F : C ⇒ D) : is_prop (is_weak_equivalence F) := + by unfold is_weak_equivalence; exact _ + + definition is_weak_equivalence_of_is_equivalence [instance] (F : C ⇒ D) [is_equivalence F] + : is_weak_equivalence F := + (_, _) + + definition fully_faithful_of_is_weak_equivalence.mk [instance] (F : C ⇒ D) + [H : is_weak_equivalence F] : fully_faithful F := + pr1 H + + definition essentially_surjective_of_is_weak_equivalence.mk [instance] (F : C ⇒ D) + [H : is_weak_equivalence F] : essentially_surjective F := + pr2 H + + definition is_weak_equivalence_compose (G : D ⇒ E) (F : C ⇒ D) + [H : is_weak_equivalence G] [K : is_weak_equivalence F] : is_weak_equivalence (G ∘f F) := + (fully_faithful_compose G F, essentially_surjective_compose G F) + + definition weak_equivalence.mk [constructor] (F : C ⇒ D) (H : is_weak_equivalence F) : C ≃w D := + weak_equivalence.mk' C 1 F + + definition weak_equivalence.symm [unfold 3] : C ≃w D → D ≃w C + | (@weak_equivalence.mk' _ _ X F₁ F₂ H₁ H₂) := weak_equivalence.mk' X F₂ F₁ + /- TODO definition is_equiv_isomorphism_of_eq [constructor] (C D : Precategory) : is_equiv (@isomorphism_of_eq C D) := @@ -401,6 +474,8 @@ namespace category definition is_equivalence_equiv_is_weak_equivalence [constructor] {C D : Category} (F : C ⇒ D) : is_equivalence F ≃ is_weak_equivalence F := sorry + + -- weak_equivalence.trans -/ diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index c7b11635f..c81e2cad6 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -179,6 +179,13 @@ namespace iso variable {C} definition iso_eq {f f' : a ≅ b} (p : to_hom f = to_hom f') : f = f' := by (cases f; cases f'; apply (iso_mk_eq p)) + + definition iso_pathover {X : Type} {x₁ x₂ : X} {p : x₁ = x₂} {a : X → ob} {b : X → ob} + {f₁ : a x₁ ≅ b x₁} {f₂ : a x₂ ≅ b x₂} (q : to_hom f₁ =[p] to_hom f₂) : f₁ =[p] f₂ := + begin + cases f₁, cases f₂, esimp at q, induction q, apply pathover_idp_of_eq, + exact ap (iso.mk _) !is_prop.elim + end variable [C] -- The structure for isomorphism can be characterized up to equivalence by a sigma type. @@ -225,6 +232,41 @@ namespace iso p ▸ !iso.refl = iso_of_eq p := by cases p; reflexivity + definition hom_pathover {X : Type} {x₁ x₂ : X} {p : x₁ = x₂} {a b : X → ob} + {f₁ : a x₁ ⟶ b x₁} {f₂ : a x₂ ⟶ b x₂} (q : hom_of_eq (ap b p) ∘ f₁ = f₂ ∘ hom_of_eq (ap a p)) : + f₁ =[p] f₂ := + begin + induction p, apply pathover_idp_of_eq, exact !id_left⁻¹ ⬝ q ⬝ !id_right + end + + definition hom_pathover_constant_left {X : Type} {x₁ x₂ : X} {p : x₁ = x₂} {a : ob} {b : X → ob} + {f₁ : a ⟶ b x₁} {f₂ : a ⟶ b x₂} (q : hom_of_eq (ap b p) ∘ f₁ = f₂) : f₁ =[p] f₂ := + hom_pathover (q ⬝ !id_right⁻¹ ⬝ ap (λx, _ ∘ hom_of_eq x) !ap_constant⁻¹) + + definition hom_pathover_constant_right {X : Type} {x₁ x₂ : X} {p : x₁ = x₂} {a : X → ob} {b : ob} + {f₁ : a x₁ ⟶ b} {f₂ : a x₂ ⟶ b} (q : f₁ = f₂ ∘ hom_of_eq (ap a p)) : f₁ =[p] f₂ := + hom_pathover (ap (λx, hom_of_eq x ∘ _) !ap_constant ⬝ !id_left ⬝ q) + + definition hom_pathover_id_left {p : a = b} {c : ob → ob} {f₁ : a ⟶ c a} {f₂ : b ⟶ c b} + (q : hom_of_eq (ap c p) ∘ f₁ = f₂ ∘ hom_of_eq p) : f₁ =[p] f₂ := + hom_pathover (q ⬝ ap (λx, _ ∘ hom_of_eq x) !ap_id⁻¹) + + definition hom_pathover_id_right {p : a = b} {c : ob → ob} {f₁ : c a ⟶ a} {f₂ : c b ⟶ b} + (q : hom_of_eq p ∘ f₁ = f₂ ∘ hom_of_eq (ap c p)) : f₁ =[p] f₂ := + hom_pathover (ap (λx, hom_of_eq x ∘ _) !ap_id ⬝ q) + + definition hom_pathover_id_left_id_right {p : a = b} {f₁ : a ⟶ a} {f₂ : b ⟶ b} + (q : hom_of_eq p ∘ f₁ = f₂ ∘ hom_of_eq p) : f₁ =[p] f₂ := + hom_pathover_id_left (ap (λx, hom_of_eq x ∘ _) !ap_id ⬝ q) + + definition hom_pathover_id_left_constant_right {p : a = b} {f₁ : a ⟶ c} {f₂ : b ⟶ c} + (q : f₁ = f₂ ∘ hom_of_eq p) : f₁ =[p] f₂ := + hom_pathover_constant_right (q ⬝ ap (λx, _ ∘ hom_of_eq x) !ap_id⁻¹) + + definition hom_pathover_constant_left_id_right {p : a = b} {f₁ : c ⟶ a} {f₂ : c ⟶ b} + (q : hom_of_eq p ∘ f₁ = f₂) : f₁ =[p] f₂ := + hom_pathover_constant_left (ap (λx, hom_of_eq x ∘ _) !ap_id ⬝ q) + section open funext variables {X : Type} {x y : X} {F G : X → ob} diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean index 30967ff72..46748fb39 100644 --- a/hott/algebra/category/precategory.hlean +++ b/hott/algebra/category/precategory.hlean @@ -74,6 +74,14 @@ namespace category definition comp_id_eq_id_comp (f : hom a b) : f ∘ id = id ∘ f := !id_right ⬝ !id_left⁻¹ definition id_comp_eq_comp_id (f : hom a b) : id ∘ f = f ∘ id := !id_left ⬝ !id_right⁻¹ + definition hom_whisker_left (g : b ⟶ c) (p : f = f') : g ∘ f = g ∘ f' := + ap (λx, g ∘ x) p + + definition hom_whisker_right (g : c ⟶ a) (p : f = f') : f ∘ g = f' ∘ g := + ap (λx, x ∘ g) p + + /- many variants of hom_pathover are defined in .iso and .functor.basic -/ + definition left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id := calc i = i ∘ id : by rewrite id_right ... = id : by rewrite H diff --git a/hott/book.md b/hott/book.md index 4f4a5aacf..0c0c02bee 100644 --- a/hott/book.md +++ b/hott/book.md @@ -151,7 +151,7 @@ Every file is in the folder [homotopy](homotopy/homotopy.md) - 8.4 (Fiber sequences and the long exact sequence): Mostly in [homotopy.chain_complex](homotopy/chain_complex.hlean), [homotopy.LES_of_homotopy_groups](homotopy/LES_of_homotopy_groups.hlean). Definitions 8.4.1 and 8.4.2 in [types.pointed](types/pointed.hlean), Corollary 8.4.8 in [homotopy.homotopy_group](homotopy/homotopy_group.hlean). - 8.5 (The Hopf fibration): [hit.pushout](hit/pushout.hlean) (Lemma 8.5.3), [hopf](homotopy/hopf.hlean) (The Hopf construction, Lemmas 8.5.5 and 8.5.7), [susp](homotopy/susp.hlean) (Definition 8.5.6), [circle](homotopy/circle.hlean) (multiplication on the circle, Lemma 8.5.8), [join](homotopy/join.hlean) (join is associative, Lemma 8.5.9), [complex_hopf](homotopy/complex_hopf.hlean) (the H-space structure on the circle and the complex Hopf fibration, i.e. Theorem 8.5.1), [sphere2](homotopy/sphere2.hlean) (Corollary 8.5.2) - 8.6 (The Freudenthal suspension theorem): [connectedness](homotopy/connectedness.hlean) (Lemma 8.6.1), [wedge](homotopy/wedge.hlean) (Wedge connectivity, Lemma 8.6.2). Corollary 8.6.14 is proven directly in [freudenthal](homotopy/freudenthal.hlean), however, we don't prove Theorem 8.6.4. Stability of iterated suspensions is also in [freudenthal](homotopy/freudenthal.hlean). The homotopy groups of spheres in this section are computed in [sphere2](homotopy/sphere2.hlean). -- 8.7 (The van Kampen theorem): [vankampen](homotopy/vankampen.hlean) (the pushout of Groupoids is formalized in [algebra.category.constructions.pushout](algebra/category/constructions/pushout.hlean) with some definitions in [algebra.graph](algebra/graph.hlean)) +- 8.7 (The van Kampen theorem): [vankampen](homotopy/vankampen.hlean) (the pushout of Groupoids is formalized in [algebra.category.constructions.pushout](algebra/category/constructions/pushout.hlean), including the universal property of this pushout. Some preliminary definitions for this pushout are in [algebra.graph](algebra/graph.hlean)) - 8.8 (Whitehead’s theorem and Whitehead’s principle): 8.8.1 and 8.8.2 at the bottom of [types.trunc](types/trunc.hlean), 8.8.3 in [homotopy_group](homotopy/homotopy_group.hlean). [Rest to be moved] - 8.9 (A general statement of the encode-decode method): [types.eq](types/eq.hlean). - 8.10 (Additional Results): Theorem 8.10.3 is formalized in [homotopy.EM](homotopy/EM.hlean). diff --git a/hott/function.hlean b/hott/function.hlean index 48ccbe42d..6363ff8ac 100644 --- a/hott/function.hlean +++ b/hott/function.hlean @@ -11,7 +11,7 @@ import hit.trunc types.equiv cubical.square open equiv sigma sigma.ops eq trunc is_trunc pi is_equiv fiber prod -variables {A B : Type} (f : A → B) {b : B} +variables {A B C : Type} (f : A → B) {b : B} /- the image of a map is the (-1)-truncated fiber -/ definition image' [constructor] (f : A → B) (b : B) : Type := ∥ fiber f b ∥ @@ -273,6 +273,33 @@ namespace function { intro H, induction H with g p, reflexivity}, end + definition is_embedding_compose (g : B → C) (f : A → B) + (H₁ : is_embedding g) (H₂ : is_embedding f) : is_embedding (g ∘ f) := + begin + intros, apply @(is_equiv.homotopy_closed (ap g ∘ ap f)), + { apply is_equiv_compose}, + symmetry, exact ap_compose g f + end + + definition is_surjective_compose (g : B → C) (f : A → B) + (H₁ : is_surjective g) (H₂ : is_surjective f) : is_surjective (g ∘ f) := + begin + intro c, induction H₁ c with b p, induction H₂ b with a q, + exact image.mk a (ap g q ⬝ p) + end + + definition is_split_surjective_compose (g : B → C) (f : A → B) + (H₁ : is_split_surjective g) (H₂ : is_split_surjective f) : is_split_surjective (g ∘ f) := + begin + intro c, induction H₁ c with b p, induction H₂ b with a q, + exact fiber.mk a (ap g q ⬝ p) + end + + definition is_injective_compose (g : B → C) (f : A → B) + (H₁ : Π⦃b b'⦄, g b = g b' → b = b') (H₂ : Π⦃a a'⦄, f a = f a' → a = a') + ⦃a a' : A⦄ (p : g (f a) = g (f a')) : a = a' := + H₂ (H₁ p) + /- The definitions is_surjective_of_is_equiv diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean index 18e7aa8e3..c5dd63d55 100644 --- a/hott/homotopy/EM.hlean +++ b/hott/homotopy/EM.hlean @@ -131,7 +131,7 @@ namespace EM begin intro x, induction x using EM.elim, { exact Point X}, - { note p := e⁻¹ᵉ g, exact p}, + { exact e⁻¹ᵉ g}, { exact inv_preserve_binary e concat mul r g h} end diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index e7b29ece8..8db9fb116 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -314,6 +314,7 @@ namespace susp { reflexivity} end + -- TODO: rename to psusp_adjoint_loop (also in above lemmas) definition susp_adjoint_loop [constructor] (X Y : Type*) : psusp X →* Y ≃ X →* Ω Y := begin fapply equiv.MK, diff --git a/hott/homotopy/vankampen.hlean b/hott/homotopy/vankampen.hlean index 5a5596517..f1afb104f 100644 --- a/hott/homotopy/vankampen.hlean +++ b/hott/homotopy/vankampen.hlean @@ -8,7 +8,7 @@ import hit.pushout hit.prop_trunc algebra.category.constructions.pushout algebra.category.constructions.fundamental_groupoid algebra.category.functor.equivalence open eq pushout category functor sum iso paths set_quotient is_trunc trunc pi quotient - is_equiv fiber equiv + is_equiv fiber equiv function namespace pushout section @@ -16,12 +16,14 @@ namespace pushout parameters {S TL : Type.{u}} -- do we want to put these in different universe levels? {BL : Type.{v}} {TR : Type.{w}} (k : S → TL) (f : TL → BL) (g : TL → TR) [ksurj : is_surjective k] - include ksurj + definition pushout_of_sum [unfold 6] (x : BL + TR) : pushout f g := quotient.class_of _ x - local notation `F` := fundamental_groupoid_functor f - local notation `G` := fundamental_groupoid_functor g + include ksurj + + local notation `F` := Π₁⇒ f + local notation `G` := Π₁⇒ g local notation `C` := Groupoid_bpushout k F G local notation `R` := bpushout_prehom_index k F G local notation `Q` := bpushout_hom_rel_index k F G @@ -321,6 +323,8 @@ namespace pushout trunc 0 (pushout_of_sum x = pushout_of_sum y) ≃ @hom C _ x y := pushout_teq_equiv x (pushout_of_sum y) +--Groupoid_pushout k F G + definition decode_point_comp [unfold 8] {x₁ x₂ x₃ : BL + TR} (c₂ : @hom C _ x₂ x₃) (c₁ : @hom C _ x₁ x₂) : decode_point (c₂ ∘ c₁) = tconcat (decode_point c₁) (decode_point c₂) := @@ -330,7 +334,7 @@ namespace pushout apply decode_list_append end - definition vankampen_functor [constructor] : C ⇒ fundamental_groupoid (pushout f g) := + definition vankampen_functor [constructor] : C ⇒ Π₁ (pushout f g) := begin fconstructor, { exact pushout_of_sum}, @@ -362,5 +366,14 @@ namespace pushout { exact essentially_surjective_vankampen_functor} end + definition fundamental_groupoid_bpushout [constructor] : + Groupoid_bpushout k (Π₁⇒ f) (Π₁⇒ g) ≃w Π₁ (pushout f g) := + weak_equivalence.mk vankampen_functor is_weak_equivalence_vankampen_functor + end + + definition fundamental_groupoid_pushout [constructor] {TL BL TR : Type} + (f : TL → BL) (g : TL → TR) : Groupoid_bpushout (@id TL) (Π₁⇒ f) (Π₁⇒ g) ≃w Π₁ (pushout f g) := + fundamental_groupoid_bpushout (@id TL) f g + end pushout diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index db7a8577f..d928943ad 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -276,7 +276,7 @@ namespace pointed end prefix `Ω→`:(max+5) := ap1 - notation `Ω→[`:95 n:0 `] `:0 f:95 := apn n f + notation `Ω→[`:95 n:0 `]`:0 := apn n /- categorical properties of pointed homotopies -/ diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index cd7a631e9..3d87a67b9 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -191,6 +191,7 @@ namespace sigma : bc =[p] ⟨p ▸ bc.1, p ▸D bc.2⟩ := by induction p; induction bc; apply idpo + -- TODO: interchange sigma_pathover and sigma_pathover' definition sigma_pathover (p : a = a') (u : Σ(b : B a), C a b) (v : Σ(b : B a'), C a' b) (r : u.1 =[p] v.1) (s : u.2 =[apd011 C p r] v.2) : u =[p] v := begin @@ -198,6 +199,21 @@ namespace sigma esimp [apd011] at s, induction s using idp_rec_on, apply idpo end + definition sigma_pathover' (p : a = a') (u : Σ(b : B a), C a b) (v : Σ(b : B a'), C a' b) + (r : u.1 =[p] v.1) (s : pathover (λx, C x.1 x.2) u.2 (sigma_eq p r) v.2) : u =[p] v := + begin + induction u, induction v, esimp at *, induction r, + induction s using idp_rec_on, apply idpo + end + + definition sigma_pathover_nondep {B : Type} {C : A → B → Type} (p : a = a') + (u : Σ(b : B), C a b) (v : Σ(b : B), C a' b) + (r : u.1 = v.1) (s : pathover (λx, C (prod.pr1 x) (prod.pr2 x)) u.2 (prod.prod_eq p r) v.2) : u =[p] v := + begin + induction p, induction u, induction v, esimp at *, induction r, + induction s using idp_rec_on, apply idpo + end + /- TODO: * define the projections from the type u =[p] v diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index ea82806f5..255d5b265 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -717,6 +717,7 @@ namespace trunc tconcat (loop_ptrunc_pequiv n A p) (loop_ptrunc_pequiv n A q) := encode_con p q + -- rename definition iterated_loop_ptrunc_pequiv (n : ℕ₋₂) (k : ℕ) (A : Type*) : Ω[k] (ptrunc (n+k) A) ≃* ptrunc n (Ω[k] A) := begin