michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

A more useful lemma!

Browse source
This commit is contained in:
favonia 2017-06-06 17:12:50 -06:00
parent 32a6cc639d
commit b6394b9750
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
homology/homology.hlean
View file

@ -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 (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))) ... = 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 begin
fapply isomorphism.mk,
{ exact Hh theory n e },
fapply adjointify, fapply adjointify,
{ exact Hh theory n e⁻¹ᵉ* }, { exact Hh theory n e⁻¹ᵉ* },
{ intro x, exact calc { intro x, exact calc