feat(splice): prove a lemma on how to splice chain complexes together

homotopy/splice.hlean

@@ -0,0 +1,142 @@
+/-
+Copyright (c) 2016 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Floris van Doorn
+
+Given a sequence of LES's, we want to splice them together.
+... -> G_{1,k+1} -> G_{1,k} -> ... -> G_{1,1} -> G_{1,0}
+... -> G_{2,k+1} -> G_{2,k} -> ... -> G_{2,1} -> G_{2,0}
+...
+... -> G_{n,k+1} -> G_{n,k} -> ... -> G_{n,1} -> G_{n,0}
+...
+
+If we have equivalences:
+G_{n,m) = G_{n+1,m+k}
+G_{n,m+1) = G_{n+1,m+k+1}
+such that the evident squares commute, we can obtain a single sequence
+
+ ... -> G_{n,m} -> G_{n+1,m+k-1} -> ... -> G_{n+1,m} -> G_{n+2,m+k-1} -> ...
+
+However, in this formalization, we will only do this for k = 3, because we get more definitional
+equalities in this specific case than in the general case. The reason is that we need to check
+whether a term `x : fin (succ k)` represents `n`. If we do this in general using
+if x = n then ... else ...
+we don't get definitionally that x = n and the successor of x is 0, which means that when defining
+maps G_{n,m} -> G_{n+1,m+k-1} we need to transport along those paths, which is annoying.
+
+So far, the splicing seems to be only needed for k = 3, so it seems to be sufficient.
+
+-/
+
+import homotopy.chain_complex
+
+open prod prod.ops succ_str fin pointed nat algebra eq is_trunc equiv is_equiv
+
+/- fin -/
+
+  -- definition cyclic_pred {n : ℕ} (x : fin n) : fin n :=
+  -- begin
+  --   cases n with n,
+  --   { exfalso, apply not_lt_zero _ (is_lt x)},
+  --   { cases x with m H, cases m with m,
+  --     { exact fin.mk n !self_lt_succ},
+  --     { apply fin.mk m, exact lt.trans !self_lt_succ H}}
+  -- end
+
+  -- definition stratified_succ2 {N : succ_str} {n : ℕ} (x : stratified_type N n)
+  --   : stratified_type N n :=
+  -- (nat.cases_on (pr2 x) (S (pr1 x)) (λa, pr1 x), cyclic_pred (pr2 x))
+
+  -- definition stratified2 [reducible] [constructor] (N : succ_str) (n : ℕ) : succ_str :=
+  -- succ_str.mk (stratified_type N n) stratified_succ2
+
+
+namespace chain_complex
+
+definition stratified_succ_max {N : succ_str} {n : ℕ} (x : stratified N n) (p : val (pr2 x) = n)
+  : S x = (S (pr1 x), 0) :=
+begin
+  unfold [stratified, succ_str.S, stratified_succ],
+  apply prod_eq,
+  { exact if_pos p},
+  { exact dif_pos p}
+end
+
+--   definition splice_type {N M : succ_str} (G : N → chain_complex M) (k : ℕ) (m : M)
+--     (x : stratified N k) : Set* :=
+--   G x.1 (iterate S (val x.2) m)
+
+-- --   definition splice_map {N M : succ_str} (G : N → chain_complex M) (k : ℕ) (m : M)
+-- --     (x : stratified N k) : Set* :=
+-- --   G x.1 (iterate S (val x.2) m)
+
+--   definition splice (N M : succ_str) (G : N → chain_complex M) (k : ℕ) (m : M)
+--     (e0 : Πn, G n m ≃* G (S n) (S (iterate S k m))) :
+--     chain_complex (stratified N k) :=
+--   chain_complex.mk (splice_type G k m)
+--     begin
+--       intro x, cases x with n l, cases l with l H,
+--       refine if K : l = k then _ else _,
+--       { intro p, induction p, exact sorry},
+--       { exact sorry}
+--       -- cases l with l,
+--       -- { },
+--       -- { }
+--     end
+--     begin
+--       exact sorry
+--     end
+
+  definition succ_str.add [reducible] {N : succ_str} (n : N) (k : ℕ) : N :=
+  iterate S k n
+
+  infix ` +' `:65 := succ_str.add
+
+  definition splice_type [unfold 5] {N M : succ_str} (G : N → chain_complex M) (m : M)
+    (x : stratified N 2) : Set* :=
+  G x.1 (m +' val x.2)
+
+  definition splice_map {N M : succ_str} (G : N → chain_complex M) (m : M)
+    (e0 : Πn, G (S n) m ≃* G n (m +' 3)) :
+    Π(x : stratified N 2), splice_type G m (S x) →* splice_type G m x
+  | (n, fin.mk 0 H) := proof cc_to_fn (G n) m qed
+  | (n, fin.mk 1 H) := proof cc_to_fn (G n) (S m) qed
+  | (n, fin.mk 2 H) := proof cc_to_fn (G n) (S (S m)) ∘* e0 n qed
+  | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition is_chain_complex_splice_map {N M : succ_str} (G : N → chain_complex M) (m : M)
+    (e0 : Πn, G (S n) m ≃* G n (m +' 3)) (e1 : Πn, G (S n) (S m) ≃* G n (S (m +' 3)))
+    (p : Πn, e0 n ∘* cc_to_fn (G (S n)) m ~ cc_to_fn (G n) (m +' 3) ∘* e1 n) :
+    Π(x : stratified N 2) (y : splice_type G m (S (S x))),
+      splice_map G m e0 x (splice_map G m e0 (S x) y) = pt
+  | (n, fin.mk 0 H) y := proof cc_is_chain_complex (G n) m y qed
+  | (n, fin.mk 1 H) y := proof cc_is_chain_complex (G n) (S m) (e0 n y) qed
+  | (n, fin.mk 2 H) y := proof ap (cc_to_fn (G n) (S (S m))) (p n y) ⬝
+                               cc_is_chain_complex (G n) (S (S m)) (e1 n y) qed
+  | (n, fin.mk (k+3) H) y := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition splice [constructor] {N M : succ_str} (G : N → chain_complex M) (m : M)
+    (e0 : Πn, G (S n) m ≃* G n (m +' 3)) (e1 : Πn, G (S n) (S m) ≃* G n (S (m +' 3)))
+    (p : Πn, e0 n ∘* cc_to_fn (G (S n)) m ~ cc_to_fn (G n) (m +' 3) ∘* e1 n) :
+    chain_complex (stratified N 2) :=
+  chain_complex.mk (splice_type G m) (splice_map G m e0) (is_chain_complex_splice_map G m e0 e1 p)
+
+  definition is_exact_splice {N M : succ_str} (G : N → chain_complex M) (m : M)
+    (e0 : Πn, G (S n) m ≃* G n (m +' 3)) (e1 : Πn, G (S n) (S m) ≃* G n (S (m +' 3)))
+    (p : Πn, e0 n ∘* cc_to_fn (G (S n)) m ~ cc_to_fn (G n) (m +' 3) ∘* e1 n)
+    (H2 : Πn, is_exact (G n)) : Π(x : stratified N 2), is_exact_at (splice G m e0 e1 p) x
+  | (n, fin.mk 0 H) := proof H2 n m qed
+  | (n, fin.mk 1 H) := begin intro y q, induction H2 n (S m) proof y qed proof q qed with x r,
+    apply image.mk ((e0 n)⁻¹ᵉ x),
+    exact ap (pmap.to_fun (cc_to_fn (G n) (S (S m)))) (to_right_inv (e0 n) x) ⬝ r end
+  | (n, fin.mk 2 H) :=
+  begin intro y q, induction H2 n (S (S m)) proof e0 n y qed proof q qed with x r,
+    apply image.mk ((e1 n)⁻¹ᵉ x),
+    refine _ ⬝ to_left_inv (e0 n) y, refine _ ⬝ ap (e0 n)⁻¹ᵉ r, apply @eq_inv_of_eq _ _ (e0 n),
+    refine p n ((e1 n)⁻¹ᵉ x) ⬝ _, apply ap (cc_to_fn (G n) (m +' 3)), exact to_right_inv (e1 n) x
+  end
+  | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+
+end chain_complex