From 8937371b33fc6a703a53c9c1c6c67b13dbacc370 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 26 Sep 2018 13:17:57 +0200 Subject: [PATCH] put exit in projective space file it was broken after reindexing spectral sequences --- cohomology/projective_space.hlean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cohomology/projective_space.hlean b/cohomology/projective_space.hlean index 8521394..5a7dffe 100644 --- a/cohomology/projective_space.hlean +++ b/cohomology/projective_space.hlean @@ -22,7 +22,7 @@ namespace temp λx, pt definition fserre : - (λn s, uoH^-(n-s)[K agℤ 2, H^-s[circle₊]]) ⟹ᵍ (λn, H^-n[unit₊]) := + (λp q, uoH^p[K agℤ 2, H^q[circle₊]]) ⟹ᵍ (λn, H^-n[unit₊]) := proof converges_to_g_isomorphism (serre_convergence_map_of_is_conn pt f (EM_spectrum agℤ) 0 @@ -36,7 +36,7 @@ namespace temp end begin intro n, reflexivity end qed - +exit -- this file needs to be updated after reindexing of spectral sequences section local notation `X` := converges_to.X fserre local notation `E∞` := convergence_theorem.Einf (converges_to.HH fserre)