From c9af080cc2f3ff84f42f63d8d54be8bdbeea3db3 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 9 Sep 2016 16:43:39 -0400 Subject: [PATCH] feat(splice): prove a lemma on how to splice chain complexes together --- homotopy/splice.hlean | 142 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 142 insertions(+) create mode 100644 homotopy/splice.hlean diff --git a/homotopy/splice.hlean b/homotopy/splice.hlean new file mode 100644 index 0000000..0066390 --- /dev/null +++ b/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