216 lines
6.9 KiB
Text
216 lines
6.9 KiB
Text
import .spectrum .EM
|
||
|
||
-- TODO move this
|
||
open trunc_index nat
|
||
|
||
namespace int
|
||
|
||
section
|
||
private definition maxm2_le.lemma₁ {n k : ℕ} : n+(1:int) + -[1+ k] ≤ n :=
|
||
le.intro (
|
||
calc n + 1 + -[1+ k] + k = n + 1 - (k + 1) + k : by reflexivity
|
||
... = n : sorry)
|
||
|
||
private definition maxm2_le.lemma₂ {n : ℕ} {k : ℤ} : -[1+ n] + 1 + k ≤ k :=
|
||
le.intro (
|
||
calc -[1+ n] + 1 + k + n = - (n + 1) + 1 + k + n : by reflexivity
|
||
... = k : sorry)
|
||
|
||
definition maxm2_le (n k : ℤ) : maxm2 (n+1+k) ≤ (maxm1m1 n).+1+2+(maxm1m1 k) :=
|
||
begin
|
||
rewrite [-(maxm1_eq_succ n)],
|
||
induction n with n n,
|
||
{ induction k with k k,
|
||
{ induction k with k IH,
|
||
{ apply le.tr_refl },
|
||
{ exact succ_le_succ IH } },
|
||
{ exact trunc_index.le_trans (maxm2_monotone maxm2_le.lemma₁)
|
||
(maxm2_le_maxm1 n) } },
|
||
{ krewrite (add_plus_two_comm -1 (maxm1m1 k)),
|
||
rewrite [-(maxm1_eq_succ k)],
|
||
exact trunc_index.le_trans (maxm2_monotone maxm2_le.lemma₂)
|
||
(maxm2_le_maxm1 k) }
|
||
end
|
||
end
|
||
|
||
end int
|
||
|
||
open int trunc eq is_trunc lift unit pointed equiv is_equiv algebra EM
|
||
|
||
namespace spectrum
|
||
|
||
definition ptrunc_maxm2_change_int {k l : ℤ} (X : Type*) (p : k = l)
|
||
: ptrunc (maxm2 k) X ≃* ptrunc (maxm2 l) X :=
|
||
pequiv_ap (λ n, ptrunc (maxm2 n) X) p
|
||
|
||
definition loop_ptrunc_maxm2_pequiv (k : ℤ) (X : Type*) :
|
||
Ω (ptrunc (maxm2 (k+1)) X) ≃* ptrunc (maxm2 k) (Ω X) :=
|
||
begin
|
||
induction k with k k,
|
||
{ exact loop_ptrunc_pequiv k X },
|
||
{ refine pequiv_of_is_contr _ _ _ !is_trunc_trunc,
|
||
apply is_contr_loop,
|
||
cases k with k,
|
||
{ change is_set (trunc 0 X), apply _ },
|
||
{ change is_set (trunc -2 X), apply _ }}
|
||
end
|
||
|
||
definition is_trunc_of_is_trunc_maxm2 (k : ℤ) (X : Type)
|
||
: is_trunc (maxm2 k) X → is_trunc (max0 k) X :=
|
||
λ H, @is_trunc_of_le X _ _ (maxm2_le_maxm0 k) H
|
||
|
||
definition strunc [constructor] (k : ℤ) (E : spectrum) : spectrum :=
|
||
spectrum.MK (λ(n : ℤ), ptrunc (maxm2 (k + n)) (E n))
|
||
(λ(n : ℤ), ptrunc_pequiv_ptrunc (maxm2 (k + n)) (equiv_glue E n)
|
||
⬝e* (loop_ptrunc_maxm2_pequiv (k + n) (E (n+1)))⁻¹ᵉ*
|
||
⬝e* (loop_pequiv_loop
|
||
(ptrunc_maxm2_change_int _ (add.assoc k n 1))))
|
||
|
||
definition strunc_change_int [constructor] {k l : ℤ} (E : spectrum) (p : k = l) :
|
||
strunc k E →ₛ strunc l E :=
|
||
begin induction p, reflexivity end
|
||
|
||
definition is_trunc_maxm2_loop (A : pType) (k : ℤ)
|
||
: is_trunc (maxm2 (k + 1)) A → is_trunc (maxm2 k) (Ω A) :=
|
||
begin
|
||
intro H, induction k with k k,
|
||
{ apply is_trunc_loop, exact H },
|
||
{ apply is_contr_loop, cases k with k,
|
||
{ exact H },
|
||
{ have H2 : is_contr A, from H, apply _ } }
|
||
end
|
||
|
||
definition is_strunc [reducible] (k : ℤ) (E : spectrum) : Type :=
|
||
Π (n : ℤ), is_trunc (maxm2 (k + n)) (E n)
|
||
|
||
definition is_strunc_change_int {k l : ℤ} (E : spectrum) (p : k = l)
|
||
: is_strunc k E → is_strunc l E :=
|
||
begin induction p, exact id end
|
||
|
||
definition is_strunc_of_le {k l : ℤ} (E : spectrum) (H : k ≤ l)
|
||
: is_strunc k E → is_strunc l E :=
|
||
begin
|
||
intro T, intro n, exact is_trunc_of_le (E n)
|
||
(maxm2_monotone (algebra.add_le_add_right H n))
|
||
end
|
||
|
||
definition is_strunc_strunc (k : ℤ) (E : spectrum)
|
||
: is_strunc k (strunc k E) :=
|
||
λ n, is_trunc_trunc (maxm2 (k + n)) (E n)
|
||
|
||
definition is_trunc_maxm2_change_int {k l : ℤ} (X : pType) (p : k = l)
|
||
: is_trunc (maxm2 k) X → is_trunc (maxm2 l) X :=
|
||
by induction p; exact id
|
||
|
||
definition strunc_functor [constructor] (k : ℤ) {E F : spectrum} (f : E →ₛ F) :
|
||
strunc k E →ₛ strunc k F :=
|
||
smap.mk (λn, ptrunc_functor (maxm2 (k + n)) (f n)) sorry
|
||
|
||
definition is_strunc_EM_spectrum (G : AbGroup)
|
||
: is_strunc 0 (EM_spectrum G) :=
|
||
begin
|
||
intro n, induction n with n n,
|
||
{ -- case ≥ 0
|
||
apply is_trunc_maxm2_change_int (EM G n) (zero_add n)⁻¹,
|
||
apply is_trunc_EM },
|
||
{ change is_contr (EM_spectrum G (-[1+n])),
|
||
induction n with n IH,
|
||
{ -- case = -1
|
||
apply is_contr_loop, exact is_trunc_EM G 0 },
|
||
{ -- case < -1
|
||
apply is_trunc_loop, apply is_trunc_succ, exact IH }}
|
||
end
|
||
|
||
definition strunc_elim [constructor] {k : ℤ} {E F : spectrum} (f : E →ₛ F)
|
||
(H : is_strunc k F) : strunc k E →ₛ F :=
|
||
smap.mk (λn, ptrunc.elim (maxm2 (k + n)) (f n))
|
||
(λn, sorry)
|
||
|
||
definition trivial_shomotopy_group_of_is_strunc (E : spectrum)
|
||
{n k : ℤ} (K : is_strunc n E) (H : n < k)
|
||
: is_contr (πₛ[k] E) :=
|
||
let m := n + (2 - k) in
|
||
have I : m < 2, from
|
||
calc
|
||
m = (2 - k) + n : int.add_comm n (2 - k)
|
||
... < (2 - k) + k : add_lt_add_left H (2 - k)
|
||
... = 2 : sub_add_cancel 2 k,
|
||
@trivial_homotopy_group_of_is_trunc (E (2 - k)) (max0 m) 2
|
||
(is_trunc_of_is_trunc_maxm2 m (E (2 - k)) (K (2 - k)))
|
||
(nat.succ_le_succ (max0_le_of_le (le_sub_one_of_lt I)))
|
||
|
||
definition str [constructor] (k : ℤ) (E : spectrum) : E →ₛ strunc k E :=
|
||
smap.mk (λ n, ptr (maxm2 (k + n)) (E n))
|
||
(λ n, sorry)
|
||
|
||
|
||
structure truncspectrum (n : ℤ) :=
|
||
(carrier : spectrum)
|
||
(struct : is_strunc n carrier)
|
||
|
||
notation n `-spectrum` := truncspectrum n
|
||
|
||
attribute truncspectrum.carrier [coercion]
|
||
|
||
definition genspectrum_of_truncspectrum (n : ℤ)
|
||
: n-spectrum → gen_spectrum +ℤ :=
|
||
λ E, truncspectrum.carrier E
|
||
|
||
attribute genspectrum_of_truncspectrum [coercion]
|
||
|
||
section
|
||
|
||
open is_conn
|
||
|
||
definition is_conn_maxm1_of_maxm2 (A : Type*) (n : ℤ)
|
||
: is_conn (maxm2 n) A → is_conn (maxm1m1 n).+1 A :=
|
||
begin
|
||
intro H, induction n with n n,
|
||
{ exact H },
|
||
{ exact is_conn_minus_one A (tr pt) }
|
||
end
|
||
|
||
definition is_trunc_maxm2_of_maxm1 (A : Type*) (n : ℤ)
|
||
: is_trunc (maxm1m1 n).+1 A → is_trunc (maxm2 n) A :=
|
||
begin
|
||
intro H, induction n with n n,
|
||
{ exact H},
|
||
{ apply is_contr_of_merely_prop,
|
||
{ exact H },
|
||
{ exact tr pt } }
|
||
end
|
||
|
||
variables (A : Type*) (n : ℤ) [H : is_conn (maxm2 n) A]
|
||
include H
|
||
|
||
definition is_trunc_maxm2_ppi (k : ℤ) (P : A → (maxm2 (n+1+k))-Type*)
|
||
: is_trunc (maxm2 k) (Π*(a : A), P a) :=
|
||
is_trunc_maxm2_of_maxm1 (Π*(a : A), P a) k
|
||
(@is_trunc_ppi_of_is_conn A (maxm1m1 n)
|
||
(is_conn_maxm1_of_maxm2 A n H) (maxm1m1 k)
|
||
(λ a, ptrunctype.mk (P a) (is_trunc_of_le (P a) (maxm2_le n k)) pt))
|
||
|
||
definition is_strunc_spi_of_is_conn (k : ℤ) (P : A → (n+1+k)-spectrum)
|
||
: is_strunc k (spi A P) :=
|
||
begin
|
||
intro m, unfold spi,
|
||
exact is_trunc_maxm2_ppi A n (k+m)
|
||
(λ a, ptrunctype.mk (P a m)
|
||
(is_trunc_maxm2_change_int (P a m) (add.assoc (n+1) k m)
|
||
(truncspectrum.struct (P a) m)) pt)
|
||
end
|
||
|
||
end
|
||
|
||
definition is_strunc_spi (A : Type*) (k n : ℤ) (H : n ≤ k) (P : A → n-spectrum)
|
||
: is_strunc k (spi A P) :=
|
||
begin
|
||
assert K : n ≤ -[1+ 0] + 1 + k,
|
||
{ krewrite (int.zero_add k), exact H },
|
||
{ exact @is_strunc_spi_of_is_conn A (-[1+ 0])
|
||
(is_conn.is_conn_minus_two A) k
|
||
(λ a, truncspectrum.mk (P a) (is_strunc_of_le (P a) K
|
||
(truncspectrum.struct (P a)))) }
|
||
end
|
||
|
||
end spectrum
|