From d057ddec5179915a92f73263b084776a6aeb4f8f Mon Sep 17 00:00:00 2001 From: favonia Date: Fri, 9 Jun 2017 15:00:56 -0600 Subject: [PATCH] Add Hpwedge. --- algebra/direct_sum.hlean | 14 ++++++----- homology/homology.hlean | 50 ++++++++++++++++++++++++++++++++++++---- homotopy/fwedge.hlean | 2 ++ 3 files changed, 56 insertions(+), 10 deletions(-) diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index 142ae36..449b461 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -186,10 +186,11 @@ end group namespace group - definition dirsum_down_left.{u v} {I : Type.{u}} [is_set I] {Y : I → AbGroup} + definition dirsum_down_left.{u v w} {I : Type.{u}} [is_set I] (Y : I → AbGroup.{w}) : dirsum (Y ∘ down.{u v}) ≃g dirsum Y := + proof let to_hom := @dirsum_functor_left _ _ _ _ Y down.{u v} in - let from_hom := dirsum_elim (λi, dirsum_incl (Y ∘ down) (up i)) in + let from_hom := dirsum_elim (λi, dirsum_incl (Y ∘ down.{u v}) (up.{u v} i)) in begin fapply isomorphism.mk, { exact to_hom }, @@ -200,19 +201,20 @@ namespace group 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 ap to_hom (dirsum_elim_compute (λi, dirsum_incl (Y ∘ down) (up i)) i y) ⬝ _, - refine dirsum_elim_compute _ (up i) y ⬝ _, + 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 @dirsum_homotopy _ _ (Y ∘ down) (dirsum (Y ∘ down)) (from_hom ∘g to_hom) !gid _ 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 ap from_hom (dirsum_elim_compute (λi, dirsum_incl Y (down i)) (up i) y) ⬝ _, + 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 } end + qed end group diff --git a/homology/homology.hlean b/homology/homology.hlean index 3c90cd3..ebfa457 100644 --- a/homology/homology.hlean +++ b/homology/homology.hlean @@ -31,7 +31,8 @@ namespace homology (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift (psphere 0)))) section - parameter (theory : homology_theory) + universe variable u + parameter (theory : homology_theory.{u}) open homology_theory theorem HH_base_indep (n : ℤ) {A : Type} (a b : A) @@ -78,13 +79,54 @@ namespace homology } end + definition Hadditive_equiv (n : ℤ) {I : Type} [is_set I] (X : I → Type*) + : dirsum (λi, HH theory n (X i)) ≃g HH theory n (⋁ X) := + isomorphism.mk (dirsum_elim (λi, Hh theory n (fwedge.pinl i))) (Hadditive theory n X) + + definition Hadditive' (n : ℤ) {I : Type₀} [is_set I] (X : I → pType.{u}) : is_equiv + (dirsum_elim (λi, Hh theory n (pinl i)) : dirsum (λi, HH theory n (X i)) → HH theory n (⋁ X)) := + let iso3 := HH_isomorphism n (fwedge_down_left.{0 u} X) in + let iso2 := Hadditive_equiv n (X ∘ down.{0 u}) in + let iso1 := (dirsum_down_left.{0 u} (λ i, HH theory n (X i)))⁻¹ᵍ in + let iso := calc dirsum (λ i, HH theory n (X i)) + ≃g dirsum (λ i, HH theory n (X (down.{0 u} i))) : by exact iso1 + ... ≃g HH theory n (⋁ (X ∘ down.{0 u})) : by exact iso2 + ... ≃g HH theory n (⋁ X) : by exact iso3 + in + begin + 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 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, + reflexivity + }, + refine ap iso3 _ ⬝ _, + { exact Hh theory n (fwedge.pinl (up i)) y }, + { refine _ ⬝ dirsum_elim_compute (λi, Hh theory n (fwedge.pinl i)) (up i) y, + reflexivity + }, + refine (Hpcompose theory n (fwedge_down_left X) (fwedge.pinl (up i)) y)⁻¹ ⬝ _, + refine Hh_homotopy n (fwedge_down_left.{0 u} X ∘* fwedge.pinl (up i)) (fwedge.pinl i) (fwedge_pmap_beta (λ i, pinl (down i)) (up i)) y ⬝ _, + refine (dirsum_elim_compute (λ i, Hh theory n (pinl i)) i y)⁻¹ + } + end + + definition Hadditive'_equiv (n : ℤ) {I : Type₀} [is_set I] (X : I → Type*) + : dirsum (λi, HH theory n (X i)) ≃g HH theory n (⋁ X) := + isomorphism.mk (dirsum_elim (λi, Hh theory n (fwedge.pinl i))) (Hadditive' n X) + definition Hfwedge (n : ℤ) {I : Type} [is_set I] (X : I → Type*): HH theory n (⋁ X) ≃g dirsum (λi, HH theory n (X i)) := (isomorphism.mk _ (Hadditive theory n X))⁻¹ᵍ definition Hpwedge (n : ℤ) (A B : Type*) : HH theory n (pwedge A B) ≃g HH theory n A ×g HH theory n B := - calc HH theory n (pwedge A B) ≃g HH theory n (fwedge (bool.rec A B)) : by exact sorry - ... ≃g dirsum (λb, HH theory n (bool.rec A B b)) : by exact sorry - ... ≃g HH theory n A ×g HH theory n B : by exact sorry + calc HH theory n (A ∨ B) ≃g HH theory n (⋁ (bool.rec A B)) : by exact HH_isomorphism n (pwedge_pequiv_fwedge A B) + ... ≃g dirsum (λb, HH theory n (bool.rec A B b)) : by exact (Hadditive'_equiv n (bool.rec A B))⁻¹ᵍ + ... ≃g dirsum (bool.rec (HH theory n A) (HH theory n B)) : by exact dirsum_isomorphism (bool.rec !isomorphism.refl !isomorphism.refl) + ... ≃g HH theory n A ×g HH theory n B : by exact binary_dirsum (HH theory n A) (HH theory n B) end diff --git a/homotopy/fwedge.hlean b/homotopy/fwedge.hlean index 8e532be..3a08037 100644 --- a/homotopy/fwedge.hlean +++ b/homotopy/fwedge.hlean @@ -232,6 +232,7 @@ namespace fwedge ... ≃* ⋁ (λ i, plift.{u v} (F i)) : by exact fwedge_pequiv (λ i, !pequiv_plift) definition fwedge_down_left.{u v} {I : Type} (F : I → pType) : ⋁ (F ∘ down.{u v}) ≃* ⋁ F := + proof let pto := @fwedge_pmap (lift.{u v} I) (F ∘ down) (⋁ F) (λ i, pinl (down i)) in let pfrom := @fwedge_pmap I F (⋁ (F ∘ down.{u v})) (λ i, pinl (up.{u v} i)) in begin @@ -257,5 +258,6 @@ namespace fwedge } end + qed end fwedge