From 2de92db5b6a1c00b845fd70f6cd655ae4192932d Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 12 Apr 2016 17:59:15 -0400 Subject: [PATCH] some cleanup --- homotopy/LES_applications.hlean | 25 ++++++++++------------ homotopy/chain_complex.hlean | 38 +++++++++++---------------------- 2 files changed, 24 insertions(+), 39 deletions(-) diff --git a/homotopy/LES_applications.hlean b/homotopy/LES_applications.hlean index 3e9d5d3..502b465 100644 --- a/homotopy/LES_applications.hlean +++ b/homotopy/LES_applications.hlean @@ -43,7 +43,7 @@ namespace is_conn { /- k = 0 -/ change (is_equiv (trunc_functor 0 f)), apply is_equiv_trunc_functor_of_is_conn_fun, refine is_conn_fun_of_le f (zero_le_of_nat n)}, - { /- k > 0 even -/ + { /- k > 0 -/ have H2' : k ≤ n, from le.trans !self_le_succ H2, exact @is_equiv_of_trivial _ @@ -84,12 +84,6 @@ namespace hopf open sphere.ops susp circle sphere_index - -- definition complex_phopf : S. 3 →* S. 2 := - -- proof pmap.mk complex_hopf idp qed - - -- variable (A : Type) - -- variables [h_space A] [is_conn 0 A] - attribute hopf [unfold 4] -- definition phopf (x : psusp A) : Type* := -- pointed.MK (hopf A x) @@ -120,13 +114,16 @@ namespace hopf -- definition pjoin_pspheres (n m : ℕ) : join (S. n) (S. m) ≃ (S. (n + m + 1)) := -- join.spheres n m ⬝e begin esimp, apply equiv_of_eq, apply ap S, apply add_plus_one_of_nat end --- set_option pp.all true - -- definition pjoin_spheres_inv_base (n m : ℕ) - -- : (join.spheres 1 1)⁻¹ (cast proof idp qed (@sphere.base 3)) = inl base := - -- begin - -- exact sorry - -- end + definition part_of_complex_hopf : S (of_nat 3) → sigma (hopf S¹) := + begin + intro x, apply inv (hopf.total S¹), apply inv (join.spheres 1 1), exact x + end + definition part_of_complex_hopf_base2 + : (part_of_complex_hopf (@sphere.base 3)).2 = circle.base := + begin + exact sorry + end definition pfiber_complex_phopf : pfiber complex_phopf ≃* S. 1 := begin @@ -136,7 +133,7 @@ namespace hopf (join.spheres 1 1)⁻¹ᵉ _ ⬝e _, refine fiber.equiv_precompose (hopf.total S¹)⁻¹ᵉ ⬝e _, apply fiber_pr1}, - { exact sorry} + { esimp, refine _ ⬝ part_of_complex_hopf_base2, apply fiber_pr1_fun} end open int diff --git a/homotopy/chain_complex.hlean b/homotopy/chain_complex.hlean index 3e2c3b4..85f76ef 100644 --- a/homotopy/chain_complex.hlean +++ b/homotopy/chain_complex.hlean @@ -43,13 +43,6 @@ notation `-ℤ` := sint' definition stratified_type [reducible] (N : succ_str) (n : ℕ) : Type₀ := N × fin (succ n) --- definition stratified_succ' {N : succ_str} : Π{n : ℕ}, N → ifin n → stratified_type N n --- | (succ k) n (fz k) := (S n, ifin.max k) --- | (succ k) n (fs x) := (n, ifin.incl x) - --- definition stratified_succ {N : succ_str} {n : ℕ} (x : stratified_type N n) : stratified_type N n := --- stratified_succ' (pr1 x) (pr2 x) - definition stratified_succ {N : succ_str} {n : ℕ} (x : stratified_type N n) : stratified_type N n := (if val (pr2 x) = n then S (pr1 x) else pr1 x, my_succ (pr2 x)) @@ -57,8 +50,6 @@ definition stratified_succ {N : succ_str} {n : ℕ} (x : stratified_type N n) definition stratified [reducible] [constructor] (N : succ_str) (n : ℕ) : succ_str := succ_str.mk (stratified_type N n) stratified_succ ---example (n : ℕ) : flatten (n, (2 : ifin (nat.succ (nat.succ 4)))) = 6*n+2 := proof rfl qed - notation `+3ℕ` := stratified +ℕ 2 notation `-3ℕ` := stratified -ℕ 2 notation `+3ℤ` := stratified +ℤ 2 @@ -68,20 +59,6 @@ notation `-6ℕ` := stratified -ℕ 5 notation `+6ℤ` := stratified +ℤ 5 notation `-6ℤ` := stratified -ℤ 5 --- definition triple_type (N : succ_str) : Type₀ := N ⊎ N ⊎ N --- definition triple_succ {N : succ_str} : triple_type N → triple_type N --- | (inl n) := inr (inl n) --- | (inr (inl n)) := inr (inr n) --- | (inr (inr n)) := inl (S n) - --- definition triple [reducible] [constructor] (N : succ_str) : succ_str := --- succ_str.mk (triple_type N) triple_succ - --- notation `+3ℕ` := triple +ℕ --- notation `-3ℕ` := triple -ℕ --- notation `+3ℤ` := triple +ℤ --- notation `-3ℤ` := triple -ℤ - namespace chain_complex -- are chain complexes with the "set"-requirement removed interesting? @@ -510,7 +487,12 @@ namespace chain_complex : is_trunc n (ptrunctype.to_pType X) := trunctype.struct X - /- a group where the point in the pointed corresponds with 1 in the group -/ + /- + A group where the point in the pointed type corresponds with 1 in the group. + We need this structure because a chain complex is a sequence of pointed types, and we need + to assume for some of the theorems below that some of these pointed types are groups, where the + unit for multiplication is the point. + -/ structure pgroup [class] (X : Type*) extends semigroup X, has_inv X := (pt_mul : Πa, mul pt a = a) (mul_pt : Πa, mul a pt = a) @@ -533,7 +515,13 @@ namespace chain_complex mul_left_inv_pt := mul.left_inv⦄ end - -- the following theorems would also be true of the replace "is_contr" by "is_prop" + /- + The following theorems state that in a chain complex, if certain types are contractible, and + the chain complex is exact at the right spots, a map in the chain complex is an + embedding/surjection/equivalence. For the first and third we also need to assume that + the map is a group homomorphism (and hence that the two types around it are groups). + -/ + definition is_embedding_of_trivial (X : chain_complex N) {n : N} (H : is_exact_at X n) [HX : is_contr (X (S (S n)))] [pgroup (X n)] [pgroup (X (S n))] [is_homomorphism (cc_to_fn X n)]