From 5d57e60a43481cbeb95951acf16b7567edfa2df2 Mon Sep 17 00:00:00 2001 From: favonia Date: Fri, 9 Jun 2017 15:55:19 -0600 Subject: [PATCH] Minor optimization. --- homology/homology.hlean | 3 +++ homology/torus.hlean | 4 ++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/homology/homology.hlean b/homology/homology.hlean index 2f4145c..51f6400 100644 --- a/homology/homology.hlean +++ b/homology/homology.hlean @@ -142,6 +142,9 @@ namespace homology calc HH theory n (plift.{u v} (A ∨ B)) ≃g HH theory n (plift.{u v} A ∨ plift.{u v} B) : by exact HH_isomorphism theory n (plift_pwedge A B) ... ≃g HH theory n (plift.{u v} A) ×g HH theory n (plift.{u v} B) : by exact Hpwedge theory n (plift.{u v} A) (plift.{u v} B) + definition Hplift_isomorphism (n : ℤ) {A B : Type*} (e : A ≃* B) : HH theory n (plift.{u v} A) ≃g HH theory n (plift.{u v} B) := + HH_isomorphism theory n (!pequiv_plift⁻¹ᵉ* ⬝e* e ⬝e* !pequiv_plift) + end /- homology theory associated to a prespectrum -/ diff --git a/homology/torus.hlean b/homology/torus.hlean index e2bf276..d7c7137 100644 --- a/homology/torus.hlean +++ b/homology/torus.hlean @@ -22,7 +22,7 @@ section calc HH theory n (plift (psphere m ×* psphere m)) ≃g HH theory (n + 1) (plift (⅀ (psphere m ×* psphere m))) : by exact (Hplift_psusp theory n (psphere m ×* psphere m))⁻¹ᵍ ... ≃g HH theory (n + 1) (plift (⅀ (psphere m) ∨ (⅀ (psphere m) ∨ ⅀ (psphere m ∧ psphere m)))) - : by exact HH_isomorphism theory (n + 1) (!pequiv_plift⁻¹ᵉ* ⬝e* susp_product (psphere m) (psphere m) ⬝e* !pequiv_plift) + : by exact Hplift_isomorphism theory (n + 1) (susp_product (psphere m) (psphere m)) ... ≃g HH theory (n + 1) (plift (⅀ (psphere m))) ×g HH theory (n + 1) (plift (⅀ (psphere m) ∨ (⅀ (psphere m ∧ psphere m)))) : by exact Hplift_pwedge theory (n + 1) (⅀ (psphere m)) (⅀ (psphere m) ∨ (⅀ (psphere m ∧ psphere m))) ... ≃g HH theory n (plift (psphere m)) ×g (HH theory n (plift (psphere m)) ×g HH theory n (plift (psphere (m + m)))) @@ -33,7 +33,7 @@ section : by exact Hplift_pwedge theory (n + 1) (⅀ (psphere m)) (⅀ (psphere m ∧ psphere m)) ... ≃g HH theory n (plift (psphere m)) ×g HH theory n (plift (psphere (m + m))) : by exact product_isomorphism (Hplift_psusp theory n (psphere m)) - (Hplift_psusp theory n (psphere m ∧ psphere m) ⬝g HH_isomorphism theory n (!pequiv_plift⁻¹ᵉ* ⬝e* (sphere_smash_sphere m m) ⬝e* !pequiv_plift))) + (Hplift_psusp theory n (psphere m ∧ psphere m) ⬝g Hplift_isomorphism theory n (sphere_smash_sphere m m))) end