From b6394b97508b6f63f4c979c7e019197d7f433699 Mon Sep 17 00:00:00 2001 From: favonia Date: Tue, 6 Jun 2017 17:12:50 -0600 Subject: [PATCH] A more useful lemma! --- homology/homology.hlean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/homology/homology.hlean b/homology/homology.hlean index 12ecbf7..2deb9b5 100644 --- a/homology/homology.hlean +++ b/homology/homology.hlean @@ -47,8 +47,11 @@ namespace homology ... = Hh theory n (pmap.mk f (h pt ⬝ respect_pt g)) x : by exact Hh_homotopy' n f (respect_pt f) (h pt ⬝ respect_pt g) x ... = Hh theory n g x : by exact ap (λ f, Hh theory n f x) (@pmap_eq _ _ (pmap.mk f (h pt ⬝ respect_pt g)) _ h (refl (h pt ⬝ respect_pt g))) - definition is_equiv_Hh (n : ℤ) {A B : Type*} (e : A ≃* B) : is_equiv (Hh theory n e) := + definition HH_isomorphism (n : ℤ) {A B : Type*} (e : A ≃* B) + : HH theory n A ≃g HH theory n B := begin + fapply isomorphism.mk, + { exact Hh theory n e }, fapply adjointify, { exact Hh theory n e⁻¹ᵉ* }, { intro x, exact calc