small changes, remove old file
This commit is contained in:
Floris van Doorn
parent
5fbcbfe6e8
commit
a34606c64f
3 changed files with 78 additions and 805 deletions
|
|
@ -1,764 +0,0 @@
|
|||
/-
|
||||
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
|
||||
|
||||
The old formalization of the LES of homotopy groups, where all the odd levels have a composition
|
||||
with negation
|
||||
-/
|
||||
|
||||
import homotopy.LES_of_homotopy_groups
|
||||
|
||||
open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc algebra function
|
||||
|
||||
/--------------
|
||||
PART 1 is the same as the new formalization
|
||||
--------------/
|
||||
|
||||
namespace chain_complex
|
||||
|
||||
namespace old
|
||||
universe variable u
|
||||
variables {X Y : pType.{u}} (f : X →* Y) (n : ℕ)
|
||||
include f
|
||||
|
||||
|
||||
/--------------
|
||||
PART 2
|
||||
--------------/
|
||||
|
||||
/- Now we are ready to define the long exact sequence of homotopy groups.
|
||||
First we define its carrier -/
|
||||
definition homotopy_groups : ℕ → Type*
|
||||
| 0 := Y
|
||||
| 1 := X
|
||||
| 2 := pfiber f
|
||||
| (k+3) := Ω (homotopy_groups k)
|
||||
|
||||
definition homotopy_groups_add3 [unfold_full] :
|
||||
homotopy_groups f (n+3) = Ω (homotopy_groups f n) :=
|
||||
by reflexivity
|
||||
|
||||
definition homotopy_groups_mul3
|
||||
: Πn, homotopy_groups f (3 * n) = Ω[n] Y :> Type*
|
||||
| 0 := proof rfl qed
|
||||
| (k+1) := proof ap (λX, Ω X) (homotopy_groups_mul3 k) qed
|
||||
|
||||
definition homotopy_groups_mul3add1
|
||||
: Πn, homotopy_groups f (3 * n + 1) = Ω[n] X :> Type*
|
||||
| 0 := by reflexivity
|
||||
| (k+1) := proof ap (λX, Ω X) (homotopy_groups_mul3add1 k) qed
|
||||
|
||||
definition homotopy_groups_mul3add2
|
||||
: Πn, homotopy_groups f (3 * n + 2) = Ω[n] (pfiber f) :> Type*
|
||||
| 0 := by reflexivity
|
||||
| (k+1) := proof ap (λX, Ω X) (homotopy_groups_mul3add2 k) qed
|
||||
|
||||
/- The maps between the homotopy groups -/
|
||||
definition homotopy_groups_fun
|
||||
: Π(n : ℕ), homotopy_groups f (n+1) →* homotopy_groups f n
|
||||
| 0 := proof f qed
|
||||
| 1 := proof ppoint f qed
|
||||
| 2 := proof boundary_map f qed
|
||||
| 3 := proof ap1 f ∘* pinverse qed
|
||||
| 4 := proof ap1 (ppoint f) ∘* pinverse qed
|
||||
| 5 := proof ap1 (boundary_map f) ∘* pinverse qed
|
||||
| (k+6) := proof ap1 (ap1 (homotopy_groups_fun k)) qed
|
||||
|
||||
definition homotopy_groups_fun_add6 [unfold_full] :
|
||||
homotopy_groups_fun f (n + 6) = ap1 (ap1 (homotopy_groups_fun f n)) :=
|
||||
proof idp qed
|
||||
|
||||
/- this is a simpler defintion of the functions, but which are the same as the previous ones
|
||||
(there is a pointed homotopy) -/
|
||||
definition homotopy_groups_fun'
|
||||
: Π(n : ℕ), homotopy_groups f (n+1) →* homotopy_groups f n
|
||||
| 0 := proof f qed
|
||||
| 1 := proof ppoint f qed
|
||||
| 2 := proof boundary_map f qed
|
||||
| (k+3) := proof ap1 (homotopy_groups_fun' k) ∘* pinverse qed
|
||||
|
||||
definition homotopy_groups_fun'_add3 [unfold_full] :
|
||||
homotopy_groups_fun' f (n+3) = ap1 (homotopy_groups_fun' f n) ∘* pinverse :=
|
||||
proof idp qed
|
||||
|
||||
theorem homotopy_groups_fun_eq
|
||||
: Π(n : ℕ), homotopy_groups_fun f n ~* homotopy_groups_fun' f n
|
||||
| 0 := by reflexivity
|
||||
| 1 := by reflexivity
|
||||
| 2 := by reflexivity
|
||||
| 3 := by reflexivity
|
||||
| 4 := by reflexivity
|
||||
| 5 := by reflexivity
|
||||
| (k+6) :=
|
||||
begin
|
||||
rewrite [homotopy_groups_fun_add6 f k],
|
||||
replace (k + 6) with (k + 3 + 3),
|
||||
rewrite [homotopy_groups_fun'_add3 f (k+3)],
|
||||
rewrite [homotopy_groups_fun'_add3 f k],
|
||||
refine _ ⬝* pwhisker_right _ !ap1_compose⁻¹*,
|
||||
refine _ ⬝* !passoc⁻¹*,
|
||||
refine !comp_pid⁻¹* ⬝* _,
|
||||
refine pconcat2 _ _,
|
||||
/- Currently ap1_phomotopy is defined using function extensionality -/
|
||||
{ apply ap1_phomotopy, apply pap ap1, apply homotopy_groups_fun_eq},
|
||||
{ refine _ ⬝* (pwhisker_right _ ap1_pinverse)⁻¹*, fapply phomotopy.mk,
|
||||
{ intro q, esimp, exact !inv_inv⁻¹},
|
||||
{ reflexivity}}
|
||||
end
|
||||
|
||||
definition homotopy_groups_fun_add3 :
|
||||
homotopy_groups_fun f (n + 3) ~* ap1 (homotopy_groups_fun f n) ∘* pinverse :=
|
||||
begin
|
||||
refine homotopy_groups_fun_eq f (n+3) ⬝* _,
|
||||
exact pwhisker_right _ (ap1_phomotopy (homotopy_groups_fun_eq f n)⁻¹*),
|
||||
end
|
||||
|
||||
definition fiber_sequence_pequiv_homotopy_groups :
|
||||
Πn, fiber_sequence_carrier f n ≃* homotopy_groups f n
|
||||
| 0 := by reflexivity
|
||||
| 1 := by reflexivity
|
||||
| 2 := by reflexivity
|
||||
| (k+3) :=
|
||||
begin
|
||||
refine fiber_sequence_carrier_pequiv f k ⬝e* _,
|
||||
apply loop_pequiv_loop,
|
||||
exact fiber_sequence_pequiv_homotopy_groups k
|
||||
end
|
||||
|
||||
definition fiber_sequence_pequiv_homotopy_groups_add3
|
||||
: fiber_sequence_pequiv_homotopy_groups f (n + 3) =
|
||||
ap1 (fiber_sequence_pequiv_homotopy_groups f n) ∘* fiber_sequence_carrier_pequiv f n :=
|
||||
by reflexivity
|
||||
|
||||
definition fiber_sequence_pequiv_homotopy_groups_3_phomotopy
|
||||
: fiber_sequence_pequiv_homotopy_groups f 3 ~* fiber_sequence_carrier_pequiv f 0 :=
|
||||
begin
|
||||
refine fiber_sequence_pequiv_homotopy_groups_add3 f 0 ⬝p* _,
|
||||
refine pwhisker_right _ ap1_id ⬝* _,
|
||||
apply pid_comp
|
||||
end
|
||||
|
||||
theorem fiber_sequence_phomotopy_homotopy_groups' :
|
||||
Π(n : ℕ),
|
||||
fiber_sequence_pequiv_homotopy_groups f n ∘* fiber_sequence_fun f n ~*
|
||||
homotopy_groups_fun' f n ∘* fiber_sequence_pequiv_homotopy_groups f (n + 1)
|
||||
| 0 := by reflexivity
|
||||
| 1 := by reflexivity
|
||||
| 2 :=
|
||||
begin
|
||||
refine !pid_comp ⬝* _,
|
||||
replace homotopy_groups_fun' f 2 with boundary_map f,
|
||||
refine _ ⬝* pwhisker_left _ (fiber_sequence_pequiv_homotopy_groups_3_phomotopy f)⁻¹*,
|
||||
apply phomotopy_of_pinv_right_phomotopy,
|
||||
reflexivity
|
||||
end
|
||||
| (k+3) :=
|
||||
begin
|
||||
replace (k + 3 + 1) with (k + 1 + 3),
|
||||
rewrite [fiber_sequence_pequiv_homotopy_groups_add3 f k,
|
||||
fiber_sequence_pequiv_homotopy_groups_add3 f (k+1)],
|
||||
refine !passoc ⬝* _,
|
||||
refine pwhisker_left _ (fiber_sequence_fun_phomotopy f k) ⬝* _,
|
||||
refine !passoc⁻¹* ⬝* _ ⬝* !passoc,
|
||||
apply pwhisker_right,
|
||||
rewrite [homotopy_groups_fun'_add3],
|
||||
refine _ ⬝* !passoc⁻¹*,
|
||||
refine _ ⬝* pwhisker_left _ !ap1_compose_pinverse,
|
||||
refine !passoc⁻¹* ⬝* _ ⬝* !passoc,
|
||||
apply pwhisker_right,
|
||||
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose,
|
||||
apply ap1_phomotopy,
|
||||
exact fiber_sequence_phomotopy_homotopy_groups' k
|
||||
end
|
||||
|
||||
theorem fiber_sequence_phomotopy_homotopy_groups (n : ℕ)
|
||||
(x : fiber_sequence_carrier f (n + 1)) :
|
||||
fiber_sequence_pequiv_homotopy_groups f n (fiber_sequence_fun f n x) =
|
||||
homotopy_groups_fun f n (fiber_sequence_pequiv_homotopy_groups f (n + 1) x) :=
|
||||
begin
|
||||
refine fiber_sequence_phomotopy_homotopy_groups' f n x ⬝ _,
|
||||
exact (homotopy_groups_fun_eq f n _)⁻¹
|
||||
end
|
||||
|
||||
definition type_LES_of_homotopy_groups [constructor] : type_chain_complex +ℕ :=
|
||||
transfer_type_chain_complex
|
||||
(fiber_sequence f)
|
||||
(homotopy_groups_fun f)
|
||||
(fiber_sequence_pequiv_homotopy_groups f)
|
||||
(fiber_sequence_phomotopy_homotopy_groups f)
|
||||
|
||||
definition is_exact_type_LES_of_homotopy_groups : is_exact_t (type_LES_of_homotopy_groups f) :=
|
||||
begin
|
||||
intro n,
|
||||
apply is_exact_at_t_transfer,
|
||||
apply is_exact_fiber_sequence
|
||||
end
|
||||
|
||||
/- the long exact sequence of homotopy groups -/
|
||||
definition LES_of_homotopy_groups [constructor] : chain_complex +ℕ :=
|
||||
trunc_chain_complex
|
||||
(transfer_type_chain_complex
|
||||
(fiber_sequence f)
|
||||
(homotopy_groups_fun f)
|
||||
(fiber_sequence_pequiv_homotopy_groups f)
|
||||
(fiber_sequence_phomotopy_homotopy_groups f))
|
||||
|
||||
/- the fiber sequence is exact -/
|
||||
definition is_exact_LES_of_homotopy_groups : is_exact (LES_of_homotopy_groups f) :=
|
||||
begin
|
||||
intro n,
|
||||
apply is_exact_at_trunc,
|
||||
apply is_exact_type_LES_of_homotopy_groups
|
||||
end
|
||||
|
||||
/- for a numeral, the carrier of the fiber sequence is definitionally what we want
|
||||
(as pointed sets) -/
|
||||
example : LES_of_homotopy_groups f 6 = π*[2] Y :> Set* := by reflexivity
|
||||
example : LES_of_homotopy_groups f 7 = π*[2] X :> Set* := by reflexivity
|
||||
example : LES_of_homotopy_groups f 8 = π*[2] (pfiber f) :> Set* := by reflexivity
|
||||
|
||||
/- for a numeral, the functions of the fiber sequence is definitionally what we want
|
||||
(as pointed function). All these functions have at most one "pinverse" in them, and these
|
||||
inverses are inside the π→*[2*k].
|
||||
-/
|
||||
example : cc_to_fn (LES_of_homotopy_groups f) 6 = π→*[2] f
|
||||
:> (_ →* _) := by reflexivity
|
||||
example : cc_to_fn (LES_of_homotopy_groups f) 7 = π→*[2] (ppoint f)
|
||||
:> (_ →* _) := by reflexivity
|
||||
example : cc_to_fn (LES_of_homotopy_groups f) 8 = π→*[2] (boundary_map f)
|
||||
:> (_ →* _) := by reflexivity
|
||||
example : cc_to_fn (LES_of_homotopy_groups f) 9 = π→*[2] (ap1 f ∘* pinverse)
|
||||
:> (_ →* _) := by reflexivity
|
||||
example : cc_to_fn (LES_of_homotopy_groups f) 10 = π→*[2] (ap1 (ppoint f) ∘* pinverse)
|
||||
:> (_ →* _) := by reflexivity
|
||||
example : cc_to_fn (LES_of_homotopy_groups f) 11 = π→*[2] (ap1 (boundary_map f) ∘* pinverse)
|
||||
:> (_ →* _) := by reflexivity
|
||||
example : cc_to_fn (LES_of_homotopy_groups f) 12 = π→*[4] f
|
||||
:> (_ →* _) := by reflexivity
|
||||
|
||||
/- the carrier of the fiber sequence is what we want for natural numbers of the form
|
||||
3n, 3n+1 and 3n+2 -/
|
||||
definition LES_of_homotopy_groups_mul3 (n : ℕ)
|
||||
: LES_of_homotopy_groups f (3 * n) = π*[n] Y :> Set* :=
|
||||
begin
|
||||
apply ptrunctype_eq_of_pType_eq,
|
||||
exact ap (ptrunc 0) (homotopy_groups_mul3 f n)
|
||||
end
|
||||
|
||||
definition LES_of_homotopy_groups_mul3add1 (n : ℕ)
|
||||
: LES_of_homotopy_groups f (3 * n + 1) = π*[n] X :> Set* :=
|
||||
begin
|
||||
apply ptrunctype_eq_of_pType_eq,
|
||||
exact ap (ptrunc 0) (homotopy_groups_mul3add1 f n)
|
||||
end
|
||||
|
||||
definition LES_of_homotopy_groups_mul3add2 (n : ℕ)
|
||||
: LES_of_homotopy_groups f (3 * n + 2) = π*[n] (pfiber f) :> Set* :=
|
||||
begin
|
||||
apply ptrunctype_eq_of_pType_eq,
|
||||
exact ap (ptrunc 0) (homotopy_groups_mul3add2 f n)
|
||||
end
|
||||
|
||||
definition LES_of_homotopy_groups_mul3' (n : ℕ)
|
||||
: LES_of_homotopy_groups f (3 * n) = π*[n] Y :> Type :=
|
||||
begin
|
||||
exact ap (ptrunc 0) (homotopy_groups_mul3 f n)
|
||||
end
|
||||
|
||||
definition LES_of_homotopy_groups_mul3add1' (n : ℕ)
|
||||
: LES_of_homotopy_groups f (3 * n + 1) = π*[n] X :> Type :=
|
||||
begin
|
||||
exact ap (ptrunc 0) (homotopy_groups_mul3add1 f n)
|
||||
end
|
||||
|
||||
definition LES_of_homotopy_groups_mul3add2' (n : ℕ)
|
||||
: LES_of_homotopy_groups f (3 * n + 2) = π*[n] (pfiber f) :> Type :=
|
||||
begin
|
||||
exact ap (ptrunc 0) (homotopy_groups_mul3add2 f n)
|
||||
end
|
||||
|
||||
definition group_LES_of_homotopy_groups (n : ℕ) : group (LES_of_homotopy_groups f (n + 3)) :=
|
||||
group_homotopy_group 0 (homotopy_groups f n)
|
||||
|
||||
definition comm_group_LES_of_homotopy_groups (n : ℕ) : comm_group (LES_of_homotopy_groups f (n + 6)) :=
|
||||
comm_group_homotopy_group 0 (homotopy_groups f n)
|
||||
|
||||
end old end chain_complex
|
||||
|
||||
open group prod succ_str fin
|
||||
|
||||
/--------------
|
||||
PART 3
|
||||
--------------/
|
||||
|
||||
namespace chain_complex namespace old
|
||||
|
||||
section
|
||||
universe variable u
|
||||
parameters {X Y : pType.{u}} (f : X →* Y)
|
||||
|
||||
definition homotopy_groups2 [reducible] : +6ℕ → Type*
|
||||
| (n, fin.mk 0 H) := Ω[2*n] Y
|
||||
| (n, fin.mk 1 H) := Ω[2*n] X
|
||||
| (n, fin.mk 2 H) := Ω[2*n] (pfiber f)
|
||||
| (n, fin.mk 3 H) := Ω[2*n + 1] Y
|
||||
| (n, fin.mk 4 H) := Ω[2*n + 1] X
|
||||
| (n, fin.mk k H) := Ω[2*n + 1] (pfiber f)
|
||||
|
||||
definition homotopy_groups2_add1 (n : ℕ) : Π(x : fin (succ 5)),
|
||||
homotopy_groups2 (n+1, x) = Ω (Ω(homotopy_groups2 (n, x)))
|
||||
| (fin.mk 0 H) := by reflexivity
|
||||
| (fin.mk 1 H) := by reflexivity
|
||||
| (fin.mk 2 H) := by reflexivity
|
||||
| (fin.mk 3 H) := by reflexivity
|
||||
| (fin.mk 4 H) := by reflexivity
|
||||
| (fin.mk 5 H) := by reflexivity
|
||||
| (fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
|
||||
|
||||
definition homotopy_groups_fun2 : Π(n : +6ℕ), homotopy_groups2 (S n) →* homotopy_groups2 n
|
||||
| (n, fin.mk 0 H) := proof Ω→[2*n] f qed
|
||||
| (n, fin.mk 1 H) := proof Ω→[2*n] (ppoint f) qed
|
||||
| (n, fin.mk 2 H) :=
|
||||
proof Ω→[2*n] (boundary_map f) ∘* pcast (loop_space_succ_eq_in Y (2*n)) qed
|
||||
| (n, fin.mk 3 H) := proof Ω→[2*n + 1] f ∘* pinverse qed
|
||||
| (n, fin.mk 4 H) := proof Ω→[2*n + 1] (ppoint f) ∘* pinverse qed
|
||||
| (n, fin.mk 5 H) :=
|
||||
proof (Ω→[2*n + 1] (boundary_map f) ∘* pinverse) ∘* pcast (loop_space_succ_eq_in Y (2*n+1)) qed
|
||||
| (n, fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
|
||||
|
||||
definition homotopy_groups_fun2_add1_0 (n : ℕ) (H : 0 < succ 5)
|
||||
: homotopy_groups_fun2 (n+1, fin.mk 0 H) ~*
|
||||
cast proof idp qed ap1 (ap1 (homotopy_groups_fun2 (n, fin.mk 0 H))) :=
|
||||
by reflexivity
|
||||
|
||||
definition homotopy_groups_fun2_add1_1 (n : ℕ) (H : 1 < succ 5)
|
||||
: homotopy_groups_fun2 (n+1, fin.mk 1 H) ~*
|
||||
cast proof idp qed ap1 (ap1 (homotopy_groups_fun2 (n, fin.mk 1 H))) :=
|
||||
by reflexivity
|
||||
|
||||
definition homotopy_groups_fun2_add1_2 (n : ℕ) (H : 2 < succ 5)
|
||||
: homotopy_groups_fun2 (n+1, fin.mk 2 H) ~*
|
||||
cast proof idp qed ap1 (ap1 (homotopy_groups_fun2 (n, fin.mk 2 H))) :=
|
||||
begin
|
||||
esimp, refine _ ⬝* (ap1_phomotopy !ap1_compose)⁻¹*, refine _ ⬝* !ap1_compose⁻¹*,
|
||||
apply pwhisker_left,
|
||||
refine !pcast_ap_loop_space ⬝* ap1_phomotopy !pcast_ap_loop_space,
|
||||
end
|
||||
|
||||
definition homotopy_groups_fun2_add1_3 (n : ℕ) (H : 3 < succ 5)
|
||||
: homotopy_groups_fun2 (n+1, fin.mk 3 H) ~*
|
||||
cast proof idp qed ap1 (ap1 (homotopy_groups_fun2 (n, fin.mk 3 H))) :=
|
||||
begin
|
||||
esimp, refine _ ⬝* (ap1_phomotopy !ap1_compose)⁻¹*, refine _ ⬝* !ap1_compose⁻¹*,
|
||||
apply pwhisker_left,
|
||||
exact ap1_pinverse⁻¹* ⬝* ap1_phomotopy !ap1_pinverse⁻¹*
|
||||
end
|
||||
|
||||
definition homotopy_groups_fun2_add1_4 (n : ℕ) (H : 4 < succ 5)
|
||||
: homotopy_groups_fun2 (n+1, fin.mk 4 H) ~*
|
||||
cast proof idp qed ap1 (ap1 (homotopy_groups_fun2 (n, fin.mk 4 H))) :=
|
||||
begin
|
||||
esimp, refine _ ⬝* (ap1_phomotopy !ap1_compose)⁻¹*, refine _ ⬝* !ap1_compose⁻¹*,
|
||||
apply pwhisker_left,
|
||||
exact ap1_pinverse⁻¹* ⬝* ap1_phomotopy !ap1_pinverse⁻¹*
|
||||
end
|
||||
|
||||
definition homotopy_groups_fun2_add1_5 (n : ℕ) (H : 5 < succ 5)
|
||||
: homotopy_groups_fun2 (n+1, fin.mk 5 H) ~*
|
||||
cast proof idp qed ap1 (ap1 (homotopy_groups_fun2 (n, fin.mk 5 H))) :=
|
||||
begin
|
||||
esimp, refine _ ⬝* (ap1_phomotopy !ap1_compose)⁻¹*, refine _ ⬝* !ap1_compose⁻¹*,
|
||||
apply pconcat2,
|
||||
{ esimp, refine _ ⬝* (ap1_phomotopy !ap1_compose)⁻¹*, refine _ ⬝* !ap1_compose⁻¹*,
|
||||
apply pwhisker_left,
|
||||
exact ap1_pinverse⁻¹* ⬝* ap1_phomotopy !ap1_pinverse⁻¹*},
|
||||
{ refine !pcast_ap_loop_space ⬝* ap1_phomotopy !pcast_ap_loop_space}
|
||||
end
|
||||
|
||||
definition nat_of_str [unfold 2] [reducible] {n : ℕ} : ℕ × fin (succ n) → ℕ :=
|
||||
λx, succ n * pr1 x + val (pr2 x)
|
||||
|
||||
definition str_of_nat {n : ℕ} : ℕ → ℕ × fin (succ n) :=
|
||||
λm, (m / (succ n), mk_mod n m)
|
||||
|
||||
definition nat_of_str_6S [unfold 2] [reducible]
|
||||
: Π(x : stratified +ℕ 5), nat_of_str x + 1 = nat_of_str (@S (stratified +ℕ 5) x)
|
||||
| (n, fin.mk 0 H) := by reflexivity
|
||||
| (n, fin.mk 1 H) := by reflexivity
|
||||
| (n, fin.mk 2 H) := by reflexivity
|
||||
| (n, fin.mk 3 H) := by reflexivity
|
||||
| (n, fin.mk 4 H) := by reflexivity
|
||||
| (n, fin.mk 5 H) := by reflexivity
|
||||
| (n, fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
|
||||
|
||||
definition fin_prod_nat_equiv_nat [constructor] (n : ℕ) : ℕ × fin (succ n) ≃ ℕ :=
|
||||
equiv.MK nat_of_str str_of_nat
|
||||
abstract begin
|
||||
intro m, unfold [nat_of_str, str_of_nat, mk_mod],
|
||||
refine _ ⬝ (eq_div_mul_add_mod m (succ n))⁻¹,
|
||||
rewrite [mul.comm]
|
||||
end end
|
||||
abstract begin
|
||||
intro x, cases x with m k,
|
||||
cases k with k H,
|
||||
apply prod_eq: esimp [str_of_nat],
|
||||
{ rewrite [add.comm, add_mul_div_self_left _ _ (!zero_lt_succ),
|
||||
div_eq_zero_of_lt H, zero_add]},
|
||||
{ apply eq_of_veq, esimp [mk_mod],
|
||||
rewrite [add.comm, add_mul_mod_self_left, mod_eq_of_lt H]}
|
||||
end end
|
||||
|
||||
/-
|
||||
note: in the following theorem the (n+1) case is 6 times the same,
|
||||
so maybe this can be simplified
|
||||
-/
|
||||
definition homotopy_groups2_pequiv' : Π(n : ℕ) (x : fin (nat.succ 5)),
|
||||
homotopy_groups f (nat_of_str (n, x)) ≃* homotopy_groups2 (n, x)
|
||||
| 0 (fin.mk 0 H) := by reflexivity
|
||||
| 0 (fin.mk 1 H) := by reflexivity
|
||||
| 0 (fin.mk 2 H) := by reflexivity
|
||||
| 0 (fin.mk 3 H) := by reflexivity
|
||||
| 0 (fin.mk 4 H) := by reflexivity
|
||||
| 0 (fin.mk 5 H) := by reflexivity
|
||||
| (n+1) (fin.mk 0 H) :=
|
||||
begin
|
||||
-- uncomment the next two lines to have prettier subgoals
|
||||
-- esimp, replace (succ 5 * (n + 1) + 0) with (6*n+3+3),
|
||||
-- rewrite [+homotopy_groups_add3, homotopy_groups2_add1],
|
||||
apply loop_pequiv_loop, apply loop_pequiv_loop,
|
||||
rexact homotopy_groups2_pequiv' n (fin.mk 0 H)
|
||||
end
|
||||
| (n+1) (fin.mk 1 H) :=
|
||||
begin
|
||||
apply loop_pequiv_loop, apply loop_pequiv_loop,
|
||||
rexact homotopy_groups2_pequiv' n (fin.mk 1 H)
|
||||
end
|
||||
| (n+1) (fin.mk 2 H) :=
|
||||
begin
|
||||
apply loop_pequiv_loop, apply loop_pequiv_loop,
|
||||
rexact homotopy_groups2_pequiv' n (fin.mk 2 H)
|
||||
end
|
||||
| (n+1) (fin.mk 3 H) :=
|
||||
begin
|
||||
apply loop_pequiv_loop, apply loop_pequiv_loop,
|
||||
rexact homotopy_groups2_pequiv' n (fin.mk 3 H)
|
||||
end
|
||||
| (n+1) (fin.mk 4 H) :=
|
||||
begin
|
||||
apply loop_pequiv_loop, apply loop_pequiv_loop,
|
||||
rexact homotopy_groups2_pequiv' n (fin.mk 4 H)
|
||||
end
|
||||
| (n+1) (fin.mk 5 H) :=
|
||||
begin
|
||||
apply loop_pequiv_loop, apply loop_pequiv_loop,
|
||||
rexact homotopy_groups2_pequiv' n (fin.mk 5 H)
|
||||
end
|
||||
| n (fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
|
||||
|
||||
definition homotopy_groups2_pequiv : Π(x : +6ℕ),
|
||||
homotopy_groups f (nat_of_str x) ≃* homotopy_groups2 x
|
||||
| (n, x) := homotopy_groups2_pequiv' n x
|
||||
|
||||
/- all cases where n>0 are basically the same -/
|
||||
definition homotopy_groups_fun2_phomotopy (x : +6ℕ) :
|
||||
homotopy_groups2_pequiv x ∘* homotopy_groups_fun f (nat_of_str x) ~*
|
||||
(homotopy_groups_fun2 x ∘* homotopy_groups2_pequiv (S x))
|
||||
∘* pcast (ap (homotopy_groups f) (nat_of_str_6S x)) :=
|
||||
begin
|
||||
cases x with n x, cases x with k H,
|
||||
cases k with k, rotate 1, cases k with k, rotate 1, cases k with k, rotate 1,
|
||||
cases k with k, rotate 1, cases k with k, rotate 1, cases k with k, rotate 2,
|
||||
{ /-k=0-/
|
||||
induction n with n IH,
|
||||
{ refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
|
||||
reflexivity},
|
||||
{ refine _ ⬝* !comp_pid⁻¹*,
|
||||
refine _ ⬝* pwhisker_right _ (!homotopy_groups_fun2_add1_0)⁻¹*,
|
||||
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
|
||||
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
|
||||
exact IH ⬝* !comp_pid}},
|
||||
{ /-k=1-/
|
||||
induction n with n IH,
|
||||
{ refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
|
||||
reflexivity},
|
||||
{ refine _ ⬝* !comp_pid⁻¹*,
|
||||
refine _ ⬝* pwhisker_right _ (!homotopy_groups_fun2_add1_1)⁻¹*,
|
||||
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
|
||||
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
|
||||
exact IH ⬝* !comp_pid}},
|
||||
{ /-k=2-/
|
||||
induction n with n IH,
|
||||
{ refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
|
||||
refine _ ⬝* !comp_pid⁻¹*,
|
||||
reflexivity},
|
||||
{ refine _ ⬝* !comp_pid⁻¹*,
|
||||
refine _ ⬝* pwhisker_right _ (!homotopy_groups_fun2_add1_2)⁻¹*,
|
||||
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
|
||||
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
|
||||
exact IH ⬝* !comp_pid}},
|
||||
{ /-k=3-/
|
||||
induction n with n IH,
|
||||
{ refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
|
||||
reflexivity},
|
||||
{ refine _ ⬝* !comp_pid⁻¹*,
|
||||
refine _ ⬝* pwhisker_right _ (!homotopy_groups_fun2_add1_3)⁻¹*,
|
||||
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
|
||||
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
|
||||
exact IH ⬝* !comp_pid}},
|
||||
{ /-k=4-/
|
||||
induction n with n IH,
|
||||
{ refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
|
||||
reflexivity},
|
||||
{ refine _ ⬝* !comp_pid⁻¹*,
|
||||
refine _ ⬝* pwhisker_right _ (!homotopy_groups_fun2_add1_4)⁻¹*,
|
||||
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
|
||||
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
|
||||
exact IH ⬝* !comp_pid}},
|
||||
{ /-k=5-/
|
||||
induction n with n IH,
|
||||
{ refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
|
||||
refine !comp_pid⁻¹* ⬝* pconcat2 _ _,
|
||||
{ exact (comp_pid (ap1 (boundary_map f) ∘* pinverse))⁻¹*},
|
||||
{ refine cast (ap (λx, _ ~* loop_pequiv_loop x) !loop_pequiv_loop_rfl)⁻¹ _,
|
||||
refine cast (ap (λx, _ ~* x) !loop_pequiv_loop_rfl)⁻¹ _, reflexivity}},
|
||||
{ refine _ ⬝* !comp_pid⁻¹*,
|
||||
refine _ ⬝* pwhisker_right _ (!homotopy_groups_fun2_add1_5)⁻¹*,
|
||||
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
|
||||
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
|
||||
exact IH ⬝* !comp_pid}},
|
||||
{ /-k=k'+6-/ exfalso, apply lt_le_antisymm H, apply le_add_left}
|
||||
end
|
||||
|
||||
definition type_LES_of_homotopy_groups2 [constructor] : type_chain_complex +6ℕ :=
|
||||
transfer_type_chain_complex2
|
||||
(type_LES_of_homotopy_groups f)
|
||||
!fin_prod_nat_equiv_nat
|
||||
nat_of_str_6S
|
||||
@homotopy_groups_fun2
|
||||
@homotopy_groups2_pequiv
|
||||
begin
|
||||
intro m x,
|
||||
refine homotopy_groups_fun2_phomotopy m x ⬝ _,
|
||||
apply ap (homotopy_groups_fun2 m), apply ap (homotopy_groups2_pequiv (S m)),
|
||||
esimp, exact ap010 cast !ap_compose⁻¹ x
|
||||
end
|
||||
|
||||
definition is_exact_type_LES_of_homotopy_groups2 : is_exact_t (type_LES_of_homotopy_groups2) :=
|
||||
begin
|
||||
intro n,
|
||||
apply is_exact_at_t_transfer2,
|
||||
apply is_exact_type_LES_of_homotopy_groups
|
||||
end
|
||||
|
||||
definition LES_of_homotopy_groups2 [constructor] : chain_complex +6ℕ :=
|
||||
trunc_chain_complex type_LES_of_homotopy_groups2
|
||||
|
||||
/--------------
|
||||
PART 4
|
||||
--------------/
|
||||
|
||||
definition homotopy_groups3 [reducible] : +6ℕ → Set*
|
||||
| (n, fin.mk 0 H) := π*[2*n] Y
|
||||
| (n, fin.mk 1 H) := π*[2*n] X
|
||||
| (n, fin.mk 2 H) := π*[2*n] (pfiber f)
|
||||
| (n, fin.mk 3 H) := π*[2*n + 1] Y
|
||||
| (n, fin.mk 4 H) := π*[2*n + 1] X
|
||||
| (n, fin.mk k H) := π*[2*n + 1] (pfiber f)
|
||||
|
||||
definition homotopy_groups3eq2 [reducible]
|
||||
: Π(n : +6ℕ), ptrunc 0 (homotopy_groups2 n) ≃* homotopy_groups3 n
|
||||
| (n, fin.mk 0 H) := by reflexivity
|
||||
| (n, fin.mk 1 H) := by reflexivity
|
||||
| (n, fin.mk 2 H) := by reflexivity
|
||||
| (n, fin.mk 3 H) := by reflexivity
|
||||
| (n, fin.mk 4 H) := by reflexivity
|
||||
| (n, fin.mk 5 H) := by reflexivity
|
||||
| (n, fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
|
||||
|
||||
definition homotopy_groups_fun3 : Π(n : +6ℕ), homotopy_groups3 (S n) →* homotopy_groups3 n
|
||||
| (n, fin.mk 0 H) := proof π→*[2*n] f qed
|
||||
| (n, fin.mk 1 H) := proof π→*[2*n] (ppoint f) qed
|
||||
| (n, fin.mk 2 H) :=
|
||||
proof π→*[2*n] (boundary_map f) ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y (2*n))) qed
|
||||
| (n, fin.mk 3 H) := proof π→*[2*n + 1] f ∘* tinverse qed
|
||||
| (n, fin.mk 4 H) := proof π→*[2*n + 1] (ppoint f) ∘* tinverse qed
|
||||
| (n, fin.mk 5 H) :=
|
||||
proof (π→*[2*n + 1] (boundary_map f) ∘* tinverse)
|
||||
∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y (2*n+1))) qed
|
||||
| (n, fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
|
||||
|
||||
definition homotopy_groups_fun3eq2 [reducible]
|
||||
: Π(n : +6ℕ), homotopy_groups3eq2 n ∘* ptrunc_functor 0 (homotopy_groups_fun2 n) ~*
|
||||
homotopy_groups_fun3 n ∘* homotopy_groups3eq2 (S n)
|
||||
| (n, fin.mk 0 H) := by reflexivity
|
||||
| (n, fin.mk 1 H) := by reflexivity
|
||||
| (n, fin.mk 2 H) :=
|
||||
begin
|
||||
refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
|
||||
refine !ptrunc_functor_pcompose ⬝* _,
|
||||
apply pwhisker_left, apply ptrunc_functor_pcast,
|
||||
end
|
||||
| (n, fin.mk 3 H) :=
|
||||
begin
|
||||
refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
|
||||
refine !ptrunc_functor_pcompose ⬝* _,
|
||||
apply pwhisker_left, apply ptrunc_functor_pinverse
|
||||
end
|
||||
| (n, fin.mk 4 H) :=
|
||||
begin
|
||||
refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
|
||||
refine !ptrunc_functor_pcompose ⬝* _,
|
||||
apply pwhisker_left, apply ptrunc_functor_pinverse
|
||||
end
|
||||
| (n, fin.mk 5 H) :=
|
||||
begin
|
||||
refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
|
||||
refine !ptrunc_functor_pcompose ⬝* _,
|
||||
apply pconcat2,
|
||||
{ refine !ptrunc_functor_pcompose ⬝* _,
|
||||
apply pwhisker_left, apply ptrunc_functor_pinverse},
|
||||
{ apply ptrunc_functor_pcast}
|
||||
end
|
||||
| (n, fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
|
||||
|
||||
definition LES_of_homotopy_groups3 [constructor] : chain_complex +6ℕ :=
|
||||
transfer_chain_complex
|
||||
LES_of_homotopy_groups2
|
||||
homotopy_groups_fun3
|
||||
homotopy_groups3eq2
|
||||
homotopy_groups_fun3eq2
|
||||
|
||||
definition is_exact_LES_of_homotopy_groups3 : is_exact (LES_of_homotopy_groups3) :=
|
||||
begin
|
||||
intro n,
|
||||
apply is_exact_at_transfer,
|
||||
apply is_exact_at_trunc,
|
||||
apply is_exact_type_LES_of_homotopy_groups2
|
||||
end
|
||||
|
||||
end
|
||||
|
||||
open is_trunc
|
||||
universe variable u
|
||||
variables {X Y : pType.{u}} (f : X →* Y) (n : ℕ)
|
||||
include f
|
||||
|
||||
/- the carrier of the fiber sequence is definitionally what we want (as pointed sets) -/
|
||||
example : LES_of_homotopy_groups3 f (str_of_nat 6) = π*[2] Y :> Set* := by reflexivity
|
||||
example : LES_of_homotopy_groups3 f (str_of_nat 7) = π*[2] X :> Set* := by reflexivity
|
||||
example : LES_of_homotopy_groups3 f (str_of_nat 8) = π*[2] (pfiber f) :> Set* := by reflexivity
|
||||
example : LES_of_homotopy_groups3 f (str_of_nat 9) = π*[3] Y :> Set* := by reflexivity
|
||||
example : LES_of_homotopy_groups3 f (str_of_nat 10) = π*[3] X :> Set* := by reflexivity
|
||||
example : LES_of_homotopy_groups3 f (str_of_nat 11) = π*[3] (pfiber f) :> Set* := by reflexivity
|
||||
|
||||
definition LES_of_homotopy_groups3_0 : LES_of_homotopy_groups3 f (n, 0) = π*[2*n] Y :=
|
||||
by reflexivity
|
||||
definition LES_of_homotopy_groups3_1 : LES_of_homotopy_groups3 f (n, 1) = π*[2*n] X :=
|
||||
by reflexivity
|
||||
definition LES_of_homotopy_groups3_2 : LES_of_homotopy_groups3 f (n, 2) = π*[2*n] (pfiber f) :=
|
||||
by reflexivity
|
||||
definition LES_of_homotopy_groups3_3 : LES_of_homotopy_groups3 f (n, 3) = π*[2*n + 1] Y :=
|
||||
by reflexivity
|
||||
definition LES_of_homotopy_groups3_4 : LES_of_homotopy_groups3 f (n, 4) = π*[2*n + 1] X :=
|
||||
by reflexivity
|
||||
definition LES_of_homotopy_groups3_5 : LES_of_homotopy_groups3 f (n, 5) = π*[2*n + 1] (pfiber f):=
|
||||
by reflexivity
|
||||
|
||||
/- the functions of the fiber sequence is definitionally what we want (as pointed function).
|
||||
-/
|
||||
|
||||
definition LES_of_homotopy_groups_fun3_0 :
|
||||
cc_to_fn (LES_of_homotopy_groups3 f) (n, 0) = π→*[2*n] f :=
|
||||
by reflexivity
|
||||
definition LES_of_homotopy_groups_fun3_1 :
|
||||
cc_to_fn (LES_of_homotopy_groups3 f) (n, 1) = π→*[2*n] (ppoint f) :=
|
||||
by reflexivity
|
||||
definition LES_of_homotopy_groups_fun3_2 : cc_to_fn (LES_of_homotopy_groups3 f) (n, 2) =
|
||||
π→*[2*n] (boundary_map f) ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y (2*n))) :=
|
||||
by reflexivity
|
||||
definition LES_of_homotopy_groups_fun3_3 :
|
||||
cc_to_fn (LES_of_homotopy_groups3 f) (n, 3) = π→*[2*n + 1] f ∘* tinverse :=
|
||||
by reflexivity
|
||||
definition LES_of_homotopy_groups_fun3_4 :
|
||||
cc_to_fn (LES_of_homotopy_groups3 f) (n, 4) = π→*[2*n + 1] (ppoint f) ∘* tinverse :=
|
||||
by reflexivity
|
||||
definition LES_of_homotopy_groups_fun3_5 : cc_to_fn (LES_of_homotopy_groups3 f) (n, 5) =
|
||||
(π→*[2*n + 1] (boundary_map f) ∘* tinverse) ∘*
|
||||
pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y (2*n+1))) :=
|
||||
by reflexivity
|
||||
|
||||
definition group_LES_of_homotopy_groups3_0 :
|
||||
Π(k : ℕ) (H : k + 3 < succ 5), group (LES_of_homotopy_groups3 f (0, fin.mk (k+3) H))
|
||||
| 0 H := begin rexact group_homotopy_group 0 Y end
|
||||
| 1 H := begin rexact group_homotopy_group 0 X end
|
||||
| 2 H := begin rexact group_homotopy_group 0 (pfiber f) end
|
||||
| (k+3) H := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
|
||||
|
||||
definition comm_group_LES_of_homotopy_groups3 (n : ℕ) : Π(x : fin (succ 5)),
|
||||
comm_group (LES_of_homotopy_groups3 f (n + 1, x))
|
||||
| (fin.mk 0 H) := proof comm_group_homotopy_group (2*n) Y qed
|
||||
| (fin.mk 1 H) := proof comm_group_homotopy_group (2*n) X qed
|
||||
| (fin.mk 2 H) := proof comm_group_homotopy_group (2*n) (pfiber f) qed
|
||||
| (fin.mk 3 H) := proof comm_group_homotopy_group (2*n+1) Y qed
|
||||
| (fin.mk 4 H) := proof comm_group_homotopy_group (2*n+1) X qed
|
||||
| (fin.mk 5 H) := proof comm_group_homotopy_group (2*n+1) (pfiber f) qed
|
||||
| (fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
|
||||
|
||||
definition CommGroup_LES_of_homotopy_groups3 (n : +6ℕ) : CommGroup.{u} :=
|
||||
CommGroup.mk (LES_of_homotopy_groups3 f (pr1 n + 1, pr2 n))
|
||||
(comm_group_LES_of_homotopy_groups3 f (pr1 n) (pr2 n))
|
||||
exit
|
||||
definition homomorphism_LES_of_homotopy_groups_fun3 : Π(k : +6ℕ),
|
||||
CommGroup_LES_of_homotopy_groups3 f (S k) →g CommGroup_LES_of_homotopy_groups3 f k
|
||||
| (k, fin.mk 0 H) :=
|
||||
proof homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 0))
|
||||
(phomotopy_group_functor_mul _ _) qed
|
||||
| (k, fin.mk 1 H) :=
|
||||
proof homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 1))
|
||||
(phomotopy_group_functor_mul _ _) qed
|
||||
| (k, fin.mk 2 H) :=
|
||||
begin
|
||||
apply homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 2)),
|
||||
exact abstract begin rewrite [LES_of_homotopy_groups_fun3_2],
|
||||
refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[2 * (k + 1)] (boundary_map f)) _ _ _,
|
||||
{ apply group_homotopy_group ((2 * k) + 1)},
|
||||
{ apply phomotopy_group_functor_mul},
|
||||
{ rewrite [▸*, -ap_compose', ▸*],
|
||||
apply is_homomorphism_cast_loop_space_succ_eq_in} end end
|
||||
end
|
||||
| (k, fin.mk 3 H) :=
|
||||
begin
|
||||
apply homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 3)),
|
||||
exact abstract begin rewrite [LES_of_homotopy_groups_fun3_3],
|
||||
refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[2 * (k + 1) + 1] f) tinverse _ _,
|
||||
{ apply phomotopy_group_functor_mul},
|
||||
{ apply is_homomorphism_inverse} end end
|
||||
end
|
||||
| (k, fin.mk 4 H) :=
|
||||
begin
|
||||
apply homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 4)),
|
||||
exact abstract begin rewrite [LES_of_homotopy_groups_fun3_4],
|
||||
refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[2 * (k + 1) + 1] (ppoint f)) tinverse _ _,
|
||||
{ apply phomotopy_group_functor_mul},
|
||||
{ apply is_homomorphism_inverse} end end
|
||||
end
|
||||
| (k, fin.mk 5 H) :=
|
||||
begin
|
||||
apply homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 5)),
|
||||
exact abstract begin rewrite [LES_of_homotopy_groups_fun3_5],
|
||||
refine @is_homomorphism_compose _ _ _ _ _ _
|
||||
(π→*[2 * (k + 1) + 1] (boundary_map f) ∘ tinverse) _ _ _,
|
||||
{ refine @is_homomorphism_compose _ _ _ _ _ _
|
||||
(π→*[2 * (k + 1) + 1] (boundary_map f)) tinverse _ _,
|
||||
{ apply phomotopy_group_functor_mul},
|
||||
{ apply is_homomorphism_inverse}},
|
||||
{ rewrite [▸*, -ap_compose', ▸*],
|
||||
apply is_homomorphism_cast_loop_space_succ_eq_in} end end
|
||||
end
|
||||
| (k, fin.mk (l+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
|
||||
|
||||
--TODO: the maps 3, 4 and 5 are anti-homomorphisms.
|
||||
|
||||
end old
|
||||
end chain_complex
|
||||
|
|
@ -1,15 +1,57 @@
|
|||
import homotopy.sphere2 ..move_to_lib
|
||||
|
||||
open fin eq equiv group algebra sphere.ops pointed nat int trunc is_equiv function
|
||||
open fin eq equiv group algebra sphere.ops pointed nat int trunc is_equiv function circle
|
||||
|
||||
definition eq_one_or_eq_neg_one_of_mul_eq_one {n : ℤ} (m : ℤ) (p : n * m = 1) : n = 1 ⊎ n = -1 :=
|
||||
sorry
|
||||
definition eq_one_or_eq_neg_one_of_mul_eq_one {n : ℤ} (m : ℤ) (p : n * m = 1) : n = 1 ⊎ n = -1 :=
|
||||
sorry
|
||||
|
||||
definition endomorphism_int_unbundled (f : ℤ → ℤ) [is_add_homomorphism f] (n : ℤ) :
|
||||
f n = f 1 * n :=
|
||||
begin
|
||||
induction n using rec_nat_on with n IH n IH,
|
||||
{ refine respect_zero f ⬝ _, exact !mul_zero⁻¹ },
|
||||
{ refine respect_add f n 1 ⬝ _, rewrite IH,
|
||||
rewrite [↑int.succ, left_distrib], apply ap (λx, _ + x), exact !mul_one⁻¹},
|
||||
{ rewrite [neg_nat_succ], refine respect_add f (-n) (- 1) ⬝ _,
|
||||
rewrite [IH, ↑int.pred, mul_sub_left_distrib], apply ap (λx, _ + x),
|
||||
refine _ ⬝ ap neg !mul_one⁻¹, exact respect_neg f 1 }
|
||||
end
|
||||
|
||||
namespace sphere
|
||||
|
||||
definition πnSn_surf (n : ℕ) : πnSn n (tr surf) = 1 :> ℤ :=
|
||||
sorry
|
||||
attribute fundamental_group_of_circle fg_carrier_equiv_int [constructor]
|
||||
attribute untrunc_of_is_trunc [unfold 4]
|
||||
|
||||
definition surf_eq_loop : @surf 1 = circle.loop := sorry
|
||||
|
||||
-- definition π2S2_surf : π2S2 (tr surf) = 1 :> ℤ :=
|
||||
-- begin
|
||||
-- unfold [π2S2, chain_complex.LES_of_homotopy_groups],
|
||||
-- end
|
||||
|
||||
check (pmap.to_fun
|
||||
(chain_complex.cc_to_fn
|
||||
(chain_complex.LES_of_homotopy_groups
|
||||
hopf.complex_phopf)
|
||||
(pair 1 2))
|
||||
(tr surf))
|
||||
|
||||
-- eval (pmap.to_fun
|
||||
-- (chain_complex.cc_to_fn
|
||||
-- (chain_complex.LES_of_homotopy_groups
|
||||
-- hopf.complex_phopf)
|
||||
-- (pair 1 2))
|
||||
-- (tr surf))
|
||||
|
||||
-- definition πnSn_surf (n : ℕ) : πnSn n (tr surf) = 1 :> ℤ :=
|
||||
-- begin
|
||||
-- cases n with n IH,
|
||||
-- { refine ap (πnSn _ ∘ tr) surf_eq_loop ⬝ _, apply transport_code_loop },
|
||||
-- { unfold [πnSn], }
|
||||
-- end
|
||||
-- set_option pp.all true
|
||||
|
||||
exit
|
||||
definition deg {n : ℕ} [H : is_succ n] (f : S. n →* S. n) : ℤ :=
|
||||
by induction H with n; exact πnSn n ((π→g[n+1] f) (tr surf))
|
||||
|
||||
|
|
@ -24,19 +66,10 @@ namespace sphere
|
|||
exact ap (πnSn n) (phomotopy_group_functor_phomotopy (succ n) p (tr surf)),
|
||||
end
|
||||
|
||||
-- this is super ugly and should be changed
|
||||
definition endomorphism_int (f : gℤ →g gℤ) (n : ℤ) : f n = f (1 : ℤ) *[ℤ] n :=
|
||||
begin
|
||||
induction n using rec_nat_on with n IH n IH,
|
||||
{ refine respect_one f ⬝ _, esimp, exact !mul_zero⁻¹ },
|
||||
{ refine respect_mul f n (1 : ℤ) ⬝ _, rewrite IH,
|
||||
rewrite [↑int.succ, left_distrib], apply ap (λx, _ + x), exact !mul_one⁻¹},
|
||||
{ rewrite [neg_nat_succ], refine respect_mul f (-n : ℤ) (- 1 : ℤ) ⬝ _,
|
||||
rewrite [IH, ↑int.pred, mul_sub_left_distrib], apply ap (λx, _ + x),
|
||||
refine _ ⬝ ap neg !mul_one⁻¹, exact to_respect_inv f (1 : ℤ) }
|
||||
end
|
||||
@endomorphism_int_unbundled f (homomorphism.addstruct f) n
|
||||
|
||||
definition endomorphism_equiv_Z {X : Group} (e : X ≃g gℤ) {one : X}
|
||||
definition endomorphism_equiv_Z {i : signature} {X : Group i} (e : X ≃g gℤ) {one : X}
|
||||
(p : e one = 1 :> ℤ) (φ : X →g X) (x : X) : e (φ x) = e (φ one) *[ℤ] e x :=
|
||||
begin
|
||||
revert x, refine equiv_rect' (equiv_of_isomorphism e) _ _,
|
||||
|
|
|
|||
|
|
@ -20,13 +20,13 @@ open sigma
|
|||
|
||||
namespace group
|
||||
open is_trunc
|
||||
definition pSet_of_Group (G : Group) : Set* := ptrunctype.mk G _ 1
|
||||
definition pSet_of_Group {i : signature} (G : Group i) : Set* := ptrunctype.mk G _ 1
|
||||
|
||||
definition pmap_of_isomorphism [constructor] {G₁ G₂ : Group} (φ : G₁ ≃g G₂) :
|
||||
pType_of_Group G₁ →* pType_of_Group G₂ :=
|
||||
definition pmap_of_isomorphism [constructor] {i j : signature} {G₁ : Group i} {G₂ : Group j}
|
||||
(φ : G₁ ≃g G₂) : pType_of_Group G₁ →* pType_of_Group G₂ :=
|
||||
pequiv_of_isomorphism φ
|
||||
|
||||
definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) :
|
||||
definition pequiv_of_isomorphism_of_eq {i : signature} {G₁ G₂ : Group i} (p : G₁ = G₂) :
|
||||
pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) :=
|
||||
begin
|
||||
induction p,
|
||||
|
|
@ -36,8 +36,8 @@ namespace group
|
|||
{ apply is_prop.elim}
|
||||
end
|
||||
|
||||
definition homomorphism_change_fun [constructor] {G₁ G₂ : Group} (φ : G₁ →g G₂) (f : G₁ → G₂)
|
||||
(p : φ ~ f) : G₁ →g G₂ :=
|
||||
definition homomorphism_change_fun [constructor] {i j : signature} {G₁ : Group i} {G₂ : Group j}
|
||||
(φ : G₁ →g G₂) (f : G₁ → G₂) (p : φ ~ f) : G₁ →g G₂ :=
|
||||
homomorphism.mk f (λg h, (p (g * h))⁻¹ ⬝ to_respect_mul φ g h ⬝ ap011 mul (p g) (p h))
|
||||
|
||||
end group open group
|
||||
|
|
@ -156,6 +156,28 @@ namespace pointed
|
|||
definition ap1_pconst (A B : Type*) : Ω→(pconst A B) ~* pconst (Ω A) (Ω B) :=
|
||||
phomotopy.mk (λp, idp_con _ ⬝ ap_constant p pt) rfl
|
||||
|
||||
definition loop_ppi_commute {A : Type} (B : A → Type*) : Ω(ppi B) ≃* Π*a, Ω (B a) :=
|
||||
pequiv_of_equiv eq_equiv_homotopy rfl
|
||||
|
||||
definition equiv_ppi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a)
|
||||
: (Π*a, P a) ≃* (Π*a, Q a) :=
|
||||
pequiv_of_equiv (pi_equiv_pi_right g)
|
||||
begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end
|
||||
|
||||
definition pcast_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a)
|
||||
{a₁ a₂ : A} (p : a₁ = a₂) : pcast (ap C p) ∘* f a₁ ~* f a₂ ∘* pcast (ap B p) :=
|
||||
phomotopy.mk
|
||||
begin induction p, reflexivity end
|
||||
begin induction p, esimp, refine !idp_con ⬝ !idp_con ⬝ !ap_id⁻¹ end
|
||||
|
||||
definition pequiv_of_eq_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a)
|
||||
{a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) :=
|
||||
pcast_commute f p
|
||||
|
||||
end pointed
|
||||
|
||||
namespace fiber
|
||||
|
||||
definition pfiber_loop_space {A B : Type*} (f : A →* B) : pfiber (Ω→ f) ≃* Ω (pfiber f) :=
|
||||
pequiv_of_equiv
|
||||
(calc pfiber (Ω→ f) ≃ Σ(p : Point A = Point A), ap1 f p = rfl : (fiber.sigma_char (ap1 f) (Point (Ω B)))
|
||||
|
|
@ -206,25 +228,7 @@ namespace pointed
|
|||
... ≃* pfiber (g ∘* h) : pfiber_equiv_of_phomotopy s
|
||||
... ≃* pfiber g : pequiv_precompose
|
||||
|
||||
definition loop_ppi_commute {A : Type} (B : A → Type*) : Ω(ppi B) ≃* Π*a, Ω (B a) :=
|
||||
pequiv_of_equiv eq_equiv_homotopy rfl
|
||||
|
||||
definition equiv_ppi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a)
|
||||
: (Π*a, P a) ≃* (Π*a, Q a) :=
|
||||
pequiv_of_equiv (pi_equiv_pi_right g)
|
||||
begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end
|
||||
|
||||
definition pcast_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a)
|
||||
{a₁ a₂ : A} (p : a₁ = a₂) : pcast (ap C p) ∘* f a₁ ~* f a₂ ∘* pcast (ap B p) :=
|
||||
phomotopy.mk
|
||||
begin induction p, reflexivity end
|
||||
begin induction p, esimp, refine !idp_con ⬝ !idp_con ⬝ !ap_id⁻¹ end
|
||||
|
||||
definition pequiv_of_eq_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a)
|
||||
{a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) :=
|
||||
pcast_commute f p
|
||||
|
||||
end pointed
|
||||
end fiber
|
||||
|
||||
namespace eq --algebra.homotopy_group
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue