michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add computing version of the LES of homotopy groups.

Browse source 
Start on applications of the LES.
Also finish proofs in sec83 (I've also included them in the latest pull request for the Lean-HoTT library).
This commit is contained in:
Floris van Doorn 2016-02-17 18:27:26 -05:00
parent b7f2b9d689
commit a578b1c42e
9 changed files with 1352 additions and 264 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

96
group_theory/basic.hlean
View file

@ -21,12 +21,9 @@ set_option class.force_new true
namespace group
definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one
definition pType_of_Group (G : Group) : Type* := pointed.mk' G
definition pType_of_Group [reducible] (G : Group) : Type* := pointed.mk' G
definition Set_of_Group (G : Group) : Set := trunctype.mk G _
-- print Type*
-- print pType
definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group :=
Group.mk G _
@ -34,30 +31,79 @@ namespace group
: comm_group (Group_of_CommGroup G) :=
begin esimp, exact _ end
definition group_pType_of_Group [instance] (G : Group) : group (pType_of_Group G) :=
Group.struct G
/- group homomorphisms -/
structure homomorphism (G₁ G₂ : Group) : Type :=
(φ : G₁ → G₂)
(p : Π(g h : G₁), φ (g * h) = φ g * φ h)
definition is_homomorphism [class] [reducible]
{G₁ G₂ : Type} [group G₁] [group G₂] (φ : G₁ → G₂) : Type :=
Π(g h : G₁), φ (g * h) = φ g * φ h
attribute homomorphism.φ [coercion]
abbreviation group_fun [unfold 3] := @homomorphism.φ
abbreviation respect_mul := @homomorphism.p
infix ` →g `:55 := homomorphism
section
variables {G G₁ G₂ G₃ : Type} {g h : G₁} (ψ : G₂ → G₃) {φ₁ φ₂ : G₁ → G₂} (φ : G₁ → G₂)
[group G] [group G₁] [group G₂] [group G₃]
[is_homomorphism ψ] [is_homomorphism φ₁] [is_homomorphism φ₂] [is_homomorphism φ]
variables {G G₁ G₂ G₃ : Group} {g h : G₁} {ψ : G₂ →g G₃} {φ φ' : G₁ →g G₂}
definition respect_mul /- φ -/ : Π(g h : G₁), φ (g * h) = φ g * φ h :=
by assumption
theorem respect_one (φ : G₁ →g G₂) : φ 1 = 1 :=
theorem respect_one /- φ -/ : φ 1 = 1 :=
mul.right_cancel
(calc
φ 1 * φ 1 = φ (1 * 1) : respect_mul
φ 1 * φ 1 = φ (1 * 1) : respect_mul φ
... = φ 1 : ap φ !one_mul
... = 1 * φ 1 : one_mul)
theorem respect_inv (φ : G₁ →g G₂) (g : G₁) : φ g⁻¹ = (φ g)⁻¹ :=
theorem respect_inv /- φ -/ (g : G₁) : φ g⁻¹ = (φ g)⁻¹ :=
eq_inv_of_mul_eq_one (!respect_mul⁻¹ ⬝ ap φ !mul.left_inv ⬝ !respect_one)
definition is_set_homomorphism [instance] (G₁ G₂ : Group) : is_set (homomorphism G₁ G₂) :=
definition is_embedding_homomorphism /- φ -/ (H : Π{g}, φ g = 1 → g = 1) : is_embedding φ :=
begin
apply function.is_embedding_of_is_injective,
intro g g' p,
apply eq_of_mul_inv_eq_one,
apply H,
refine !respect_mul ⬝ _,
rewrite [respect_inv φ, p],
apply mul.right_inv
end
definition is_homomorphism_compose {ψ : G₂ → G₃} {φ : G₁ → G₂}
(H1 : is_homomorphism ψ) (H2 : is_homomorphism φ) : is_homomorphism (ψ ∘ φ) :=
λg h, ap ψ !respect_mul ⬝ !respect_mul
definition is_homomorphism_id (G : Type) [group G] : is_homomorphism (@id G) :=
λg h, idp
end
structure homomorphism (G₁ G₂ : Group) : Type :=
(φ : G₁ → G₂)
(p : is_homomorphism φ)
infix ` →g `:55 := homomorphism
definition group_fun [unfold 3] [coercion] := @homomorphism.φ
definition homomorphism.struct [instance] [priority 2000] {G₁ G₂ : Group} (φ : G₁ →g G₂)
: is_homomorphism φ :=
homomorphism.p φ
variables {G G₁ G₂ G₃ : Group} {g h : G₁} {ψ : G₂ →g G₃} {φ₁ φ₂ : G₁ →g G₂} (φ : G₁ →g G₂)
definition to_respect_mul /- φ -/ (g h : G₁) : φ (g * h) = φ g * φ h :=
respect_mul φ g h
theorem to_respect_one /- φ -/ : φ 1 = 1 :=
respect_one φ
theorem to_respect_inv /- φ -/ (g : G₁) : φ g⁻¹ = (φ g)⁻¹ :=
respect_inv φ g
definition to_is_embedding_homomorphism /- φ -/ (H : Π{g}, φ g = 1 → g = 1) : is_embedding φ :=
is_embedding_homomorphism φ @H
definition is_set_homomorphism [instance] (G₁ G₂ : Group) : is_set (G₁ →g G₂) :=
begin
assert H : G₁ →g G₂ ≃ Σ(f : G₁ → G₂), Π(g₁ g₂ : G₁), f (g₁ * g₂) = f g₁ * f g₂,
{ fapply equiv.MK,
@ -68,23 +114,23 @@ namespace group
apply is_trunc_equiv_closed_rev, exact H
end
definition pmap_of_homomorphism [constructor] (φ : G₁ →g G₂)
: pType_of_Group G₁ →* pType_of_Group G₂ :=
pmap.mk φ !respect_one
local attribute group_pType_of_Group pointed.mk' [reducible]
definition pmap_of_homomorphism [constructor] /- φ -/ : pType_of_Group G₁ →* pType_of_Group G₂ :=
pmap.mk φ (respect_one φ)
definition homomorphism_eq (p : group_fun φ ~ group_fun φ') : φ = φ' :=
definition homomorphism_eq (p : group_fun φ₁ ~ group_fun φ₂) : φ₁ = φ₂ :=
begin
induction φ with φ q, induction φ' with φ' q', esimp at p, induction p,
exact ap (homomorphism.mk φ) !is_prop.elim
induction φ₁ with φ₁ q₁, induction φ₂ with φ₂ q₂, esimp at p, induction p,
exact ap (homomorphism.mk φ₁) !is_prop.elim
end
/- categorical structure of groups + homomorphisms -/
definition homomorphism_compose [constructor] (ψ : G₂ →g G₃) (φ : G₁ →g G₂) : G₁ →g G₃ :=
homomorphism.mk (ψ ∘ φ) (λg h, ap ψ !respect_mul ⬝ !respect_mul)
homomorphism.mk (ψ ∘ φ) (is_homomorphism_compose _ _)
definition homomorphism_id [constructor] (G : Group) : G →g G :=
homomorphism.mk id (λg h, idp)
homomorphism.mk (@id G) (is_homomorphism_id G)
infixr ` ∘g `:75 := homomorphism_compose
notation 1 := homomorphism_id _
@ -104,7 +150,7 @@ namespace group
homomorphism.mk φ⁻¹
abstract begin
intro g₁ g₂, apply eq_of_fn_eq_fn' φ,
rewrite [respect_mul, +right_inv φ]
rewrite [respect_mul φ, +right_inv φ]
end end
definition isomorphism.refl [refl] [constructor] (G : Group) : G ≃g G :=

30
group_theory/constructions.hlean
View file

@ -416,10 +416,10 @@ namespace group
{ intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul},
{ intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp,
induction l with s l IH,
{ esimp [foldl], exact !respect_one⁻¹},
{ esimp [foldl], exact (respect_one φ)⁻¹},
{ rewrite [foldl_cons, fgh_helper_mul],
refine _ ⬝ (respect_mul φ (class_of [s]) (class_of l))⁻¹,
rewrite [IH], induction s: rewrite [▸*, one_mul], rewrite [-respect_inv]}}
rewrite [IH], induction s: rewrite [▸*, one_mul], rewrite [-respect_inv φ]}}
end
/- Free Commutative Group of a set -/
@ -589,11 +589,11 @@ namespace group
{ intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul},
{ intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp,
induction l with s l IH,
{ esimp [foldl], exact !respect_one⁻¹},
{ esimp [foldl], symmetry, exact to_respect_one φ},
{ rewrite [foldl_cons, fgh_helper_mul],
refine _ ⬝ (respect_mul φ (class_of [s]) (class_of l))⁻¹,
refine _ ⬝ (to_respect_mul φ (class_of [s]) (class_of l))⁻¹,
rewrite [▸*,IH], induction s: rewrite [▸*, one_mul], apply ap (λx, x * _),
exact !respect_inv⁻¹}}
exact !to_respect_inv⁻¹}}
end
/- Free Commutative Group of a set -/
@ -631,7 +631,7 @@ namespace group
begin
esimp at *,
exact calc
φ (g * h) = (φ g) * (φ h) : respect_mul
φ (g * h) = (φ g) * (φ h) : to_respect_mul
... = 1 * (φ h) : H₁
... = 1 * 1 : H₂
... = 1 : one_mul
@ -641,12 +641,12 @@ namespace group
begin
esimp at *,
exact calc
φ g⁻¹ = (φ g)⁻¹ : respect_inv
φ g⁻¹ = (φ g)⁻¹ : to_respect_inv
... = 1⁻¹ : H
... = 1 : one_inv
end
definition kernel_subgroup [constructor] (φ : G₁ →g G₂) : subgroup_rel G₁ :=
definition subgroup_kernel [constructor] (φ : G₁ →g G₂) : subgroup_rel G₁ :=
⦃ subgroup_rel,
R := kernel φ,
Rone := respect_one φ,
@ -654,24 +654,24 @@ namespace group
Rinv := kernel_inv φ
⦄
theorem kernel_subgroup_isnormal (φ : G₁ →g G₂) (g : G₁) (h : G₁)
theorem is_normal_subgroup_kernel (φ : G₁ →g G₂) (g : G₁) (h : G₁)
: kernel φ g → kernel φ (h * g * h⁻¹) :=
begin
esimp at *,
intro p,
exact calc
φ (h * g * h⁻¹) = (φ (h * g)) * φ (h⁻¹) : respect_mul
... = (φ h) * (φ g) * (φ h⁻¹) : respect_mul
φ (h * g * h⁻¹) = (φ (h * g)) * φ (h⁻¹) : to_respect_mul
... = (φ h) * (φ g) * (φ h⁻¹) : to_respect_mul
... = (φ h) * 1 * (φ h⁻¹) : p
... = (φ h) * (φ h⁻¹) : mul_one
... = (φ h) * (φ h)⁻¹ : respect_inv
... = (φ h) * (φ h)⁻¹ : to_respect_inv
... = 1 : mul.right_inv
end
definition kernel_normal_subgroup [constructor] (φ : G₁ →g G₂) : normal_subgroup_rel G₁ :=
definition normal_subgroup_kernel [constructor] (φ : G₁ →g G₂) : normal_subgroup_rel G₁ :=
⦃ normal_subgroup_rel,
kernel_subgroup φ,
is_normal := kernel_subgroup_isnormal φ
subgroup_kernel φ,
is_normal := is_normal_subgroup_kernel φ
⦄
end kernels

17
homotopy/LES_applications.hlean Normal file
View file

@ -0,0 +1,17 @@
import .LES_of_homotopy_groups homotopy.connectedness homotopy.homotopy_group
open eq is_trunc pointed homotopy is_equiv fiber equiv trunc nat
namespace is_conn
theorem is_contr_HG_fiber_of_is_connected {A B : Type*} (n k : ℕ) (f : A →* B)
[H : is_conn_map n f] (H2 : k ≤ n) : is_contr (π[k] (pfiber f)) :=
@(trivial_homotopy_group_of_is_conn (pfiber f) H2) (H pt)
theorem is_equiv_π_of_is_connected {A B : Type*} (n k : ℕ) (f : A →* B)
[H : is_conn_map n f] (H : k ≤ n) : is_equiv (π→[k] f) :=
begin
exact sorry
end
end is_conn

615
homotopy/LES_of_homotopy_groups.hlean
View file

@ -35,12 +35,15 @@ f'(n+6) := Ω²(f'(n))
We can show that these sequences are equivalent, hence the sequence (X',f') is an exact
sequence. Now we get the fiber sequence by taking the set-truncation of this sequence.
-/
import .chain_complex algebra.homotopy_group
open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc equiv.ops nat trunc algebra
open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc equiv.ops nat trunc algebra function
/--------------
PART 1
--------------/
namespace chain_complex
@ -64,7 +67,7 @@ namespace chain_complex
(fiber_sequence_helpern ⟨X, Y, f⟩ n).2.2
/- Definition 8.4.3 -/
definition fiber_sequence : left_type_chain_complex.{u} :=
definition fiber_sequence : type_chain_complex.{0 u} +ℕ :=
begin
fconstructor,
{ exact fiber_sequence_carrier f},
@ -74,7 +77,7 @@ namespace chain_complex
{ exact point_eq x}}
end
definition is_exact_fiber_sequence : is_exact_lt (fiber_sequence f) :=
definition is_exact_fiber_sequence : is_exact_t (fiber_sequence f) :=
λn x p, fiber.mk (fiber.mk x p) rfl
/- (generalization of) Lemma 8.4.4(i)(ii) -/
@ -221,6 +224,10 @@ namespace chain_complex
definition boundary_map : Ω Y →* pfiber f :=
fiber_sequence_fun f 2 ∘* (fiber_sequence_carrier_pequiv f 0)⁻¹ᵉ*
/--------------
PART 2
--------------/
/- Now we are ready to define the long exact sequence of homotopy groups.
First we define its carrier -/
definition homotopy_groups : ℕ → Type*
@ -231,7 +238,7 @@ namespace chain_complex
definition homotopy_groups_add3 [unfold_full] :
homotopy_groups f (n+3) = Ω (homotopy_groups f n) :=
proof idp qed
by reflexivity
definition homotopy_groups_mul3
: Πn, homotopy_groups f (3 * n) = Ω[n] Y :> Type*
@ -240,12 +247,12 @@ namespace chain_complex
definition homotopy_groups_mul3add1
: Πn, homotopy_groups f (3 * n + 1) = Ω[n] X :> Type*
| 0 := proof rfl qed
| 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 := proof rfl qed
| 0 := by reflexivity
| (k+1) := proof ap (λX, Ω X) (homotopy_groups_mul3add2 k) qed
/- The maps between the homotopy groups -/
@ -278,12 +285,12 @@ namespace chain_complex
theorem homotopy_groups_fun_eq
: Π(n : ℕ), homotopy_groups_fun f n ~* homotopy_groups_fun' f n
| 0 := proof phomotopy.rfl qed
| 1 := proof phomotopy.rfl qed
| 2 := proof phomotopy.rfl qed
| 3 := proof phomotopy.rfl qed
| 4 := proof phomotopy.rfl qed
| 5 := proof phomotopy.rfl qed
| 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],
@ -301,11 +308,18 @@ namespace chain_complex
{ 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 := proof pequiv.rfl qed
| 1 := proof pequiv.rfl qed
| 2 := proof pequiv.rfl qed
| 0 := by reflexivity
| 1 := by reflexivity
| 2 := by reflexivity
| (k+3) :=
begin
refine fiber_sequence_carrier_pequiv f k ⬝e* _,
@ -368,22 +382,35 @@ namespace chain_complex
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] : left_chain_complex :=
trunc_left_chain_complex
(transfer_left_type_chain_complex
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_l (LES_of_homotopy_groups f) :=
definition is_exact_LES_of_homotopy_groups : is_exact (LES_of_homotopy_groups f) :=
begin
intro n,
apply is_exact_at_l_trunc,
apply is_exact_at_lt_transfer,
apply is_exact_fiber_sequence
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
@ -396,30 +423,32 @@ namespace chain_complex
(as pointed function). All these functions have at most one "pinverse" in them, and these
inverses are inside the π→*[2*k].
-/
example : lcc_to_fn (LES_of_homotopy_groups f) 6 = π→*[2] f
example : cc_to_fn (LES_of_homotopy_groups f) 6 = π→*[2] f
:> (_ →* _) := by reflexivity
example : lcc_to_fn (LES_of_homotopy_groups f) 7 = π→*[2] (ppoint f)
example : cc_to_fn (LES_of_homotopy_groups f) 7 = π→*[2] (ppoint f)
:> (_ →* _) := by reflexivity
example : lcc_to_fn (LES_of_homotopy_groups f) 8 = π→*[2] (boundary_map f)
example : cc_to_fn (LES_of_homotopy_groups f) 8 = π→*[2] (boundary_map f)
:> (_ →* _) := by reflexivity
example : lcc_to_fn (LES_of_homotopy_groups f) 9 = π→*[2] (ap1 f ∘* pinverse)
example : cc_to_fn (LES_of_homotopy_groups f) 9 = π→*[2] (ap1 f ∘* pinverse)
:> (_ →* _) := by reflexivity
example : lcc_to_fn (LES_of_homotopy_groups f) 10 = π→*[2] (ap1 (ppoint f) ∘* pinverse)
example : cc_to_fn (LES_of_homotopy_groups f) 10 = π→*[2] (ap1 (ppoint f) ∘* pinverse)
:> (_ →* _) := by reflexivity
example : lcc_to_fn (LES_of_homotopy_groups f) 11 = π→*[2] (ap1 (boundary_map f) ∘* pinverse)
example : cc_to_fn (LES_of_homotopy_groups f) 11 = π→*[2] (ap1 (boundary_map f) ∘* pinverse)
:> (_ →* _) := by reflexivity
example : lcc_to_fn (LES_of_homotopy_groups f) 12 = π→*[4] f
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* :=
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* :=
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)
@ -432,12 +461,530 @@ namespace chain_complex
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)
-- TODO: the pointed maps are what we want for 3n, 3n+1 and 3n+2
-- TODO: they are group homomorphisms for n+3
end chain_complex
open group prod succ_str fin
/--------------
PART 3
--------------/
namespace chain_complex
--TODO: move
definition tr_mul_tr {A : Type*} (n : ℕ) (p q : Ω[n + 1] A) :
tr p *[πg[n+1] A] tr q = tr (p ⬝ q) :=
by reflexivity
definition is_homomorphism_cast_loop_space_succ_eq_in {A : Type*} (n : ℕ) :
is_homomorphism
(cast (ap (trunc 0 ∘ pointed.carrier) (loop_space_succ_eq_in A (succ n)))
: πg[n+1+1] A → πg[n+1] Ω A) :=
begin
intro g h, induction g with g, induction h with h,
xrewrite [tr_mul_tr, - + fn_cast_eq_cast_fn _ (λn, tr), tr_mul_tr, ↑cast, -tr_compose,
loop_space_succ_eq_in_concat, - + tr_compose],
end
definition is_homomorphism_inverse (A : Type*) (n : ℕ)
: is_homomorphism (λp, p⁻¹ : πag[n+2] A → πag[n+2] A) :=
begin
intro g h, rewrite mul.comm,
induction g with g, induction h with h,
exact ap tr !con_inv
end
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_space_pequiv, apply loop_space_pequiv,
rexact homotopy_groups2_pequiv' n (fin.mk 0 H)
end
| (n+1) (fin.mk 1 H) :=
begin
apply loop_space_pequiv, apply loop_space_pequiv,
rexact homotopy_groups2_pequiv' n (fin.mk 1 H)
end
| (n+1) (fin.mk 2 H) :=
begin
apply loop_space_pequiv, apply loop_space_pequiv,
rexact homotopy_groups2_pequiv' n (fin.mk 2 H)
end
| (n+1) (fin.mk 3 H) :=
begin
apply loop_space_pequiv, apply loop_space_pequiv,
rexact homotopy_groups2_pequiv' n (fin.mk 3 H)
end
| (n+1) (fin.mk 4 H) :=
begin
apply loop_space_pequiv, apply loop_space_pequiv,
rexact homotopy_groups2_pequiv' n (fin.mk 4 H)
end
| (n+1) (fin.mk 5 H) :=
begin
apply loop_space_pequiv, apply loop_space_pequiv,
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⁻¹*},
{ refine cast (ap (λx, _ ~* loop_space_pequiv x) !loop_space_pequiv_rfl)⁻¹ _,
refine cast (ap (λx, _ ~* x) !loop_space_pequiv_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_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_4 :
Π(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))
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 group_homotopy_group (2 * (k+1))},
{ 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 group_homotopy_group (2 * (k+1))},
{ 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 group_homotopy_group (2 * (k+1))},
{ 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 chain_complex

600
homotopy/chain_complex.hlean
View file

@ -5,10 +5,10 @@ Authors: Floris van Doorn
-/
import types.int types.pointed2 types.trunc
open eq pointed int unit is_equiv equiv is_trunc trunc equiv.ops
import types.int types.pointed2 types.trunc algebra.hott ..group_theory.basic .fin
open eq pointed int unit is_equiv equiv is_trunc trunc equiv.ops function algebra group sigma.ops
sum prod nat bool fin
namespace eq
definition transport_eq_Fl_idp_left {A B : Type} {a : A} {b : B} (f : A → B) (q : f a = b)
: transport_eq_Fl idp q = !idp_con⁻¹ :=
@ -21,89 +21,131 @@ namespace eq
end eq open eq
structure succ_str : Type :=
(carrier : Type)
(succ : carrier → carrier)
attribute succ_str.carrier [coercion]
definition succ_str.S {X : succ_str} : X → X := succ_str.succ X
open succ_str
definition snat [reducible] [constructor] : succ_str := succ_str.mk ℕ nat.succ
definition snat' [reducible] [constructor] : succ_str := succ_str.mk ℕ nat.pred
definition sint [reducible] [constructor] : succ_str := succ_str.mk ℤ int.succ
definition sint' [reducible] [constructor] : succ_str := succ_str.mk ℤ int.pred
notation `+ℕ` := snat
notation `-ℕ` := snat'
notation `+ℤ` := sint
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))
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
notation `-3ℤ` := stratified -ℤ 2
notation `+6ℕ` := stratified +ℕ 5
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?
structure type_chain_complex : Type :=
(car : ℤ → Type*)
(fn : Π(n : ℤ), car (n + 1) →* car n)
(is_chain_complex : Π{n : ℤ} (x : car ((n + 1) + 1)), fn n (fn (n+1) x) = pt)
structure type_chain_complex (N : succ_str) : Type :=
(car : N → Type*)
(fn : Π(n : N), car (S n) →* car n)
(is_chain_complex : Π(n : N) (x : car (S (S n))), fn n (fn (S n) x) = pt)
structure left_type_chain_complex : Type := -- chain complex on the naturals with maps going down
(car : ℕ → Type*)
(fn : Π(n : ℕ), car (n + 1) →* car n)
(is_chain_complex : Π{n : ℕ} (x : car ((n + 1) + 1)), fn n (fn (n+1) x) = pt)
section
variables {N : succ_str} (X : type_chain_complex N) (n : N)
structure right_type_chain_complex : Type := -- chain complex on the naturals with maps going up
(car : ℕ → Type*)
(fn : Π(n : ℕ), car n →* car (n + 1))
(is_chain_complex : Π{n : ℕ} (x : car n), fn (n+1) (fn n x) = pt)
definition tcc_to_car [unfold 1] [coercion] := @type_chain_complex.car
definition tcc_to_fn [unfold 1] := @type_chain_complex.fn
definition tcc_is_chain_complex [unfold 1] := @type_chain_complex.is_chain_complex
definition ltcc_to_car [unfold 1] [coercion] := @left_type_chain_complex.car
definition ltcc_to_fn [unfold 1] := @left_type_chain_complex.fn
definition ltcc_is_chain_complex [unfold 1] := @left_type_chain_complex.is_chain_complex
definition rtcc_to_car [unfold 1] [coercion] := @right_type_chain_complex.car
definition rtcc_to_fn [unfold 1] := @right_type_chain_complex.fn
definition rtcc_is_chain_complex [unfold 1] := @right_type_chain_complex.is_chain_complex
definition tcc_to_car [unfold 2] [coercion] := @type_chain_complex.car
definition tcc_to_fn [unfold 2] : X (S n) →* X n := type_chain_complex.fn X n
definition tcc_is_chain_complex [unfold 2]
: Π(x : X (S (S n))), tcc_to_fn X n (tcc_to_fn X (S n) x) = pt :=
type_chain_complex.is_chain_complex X n
-- important: these notions are shifted by one! (this is to avoid transports)
definition is_exact_at_t [reducible] (X : type_chain_complex) (n : ℤ) : Type :=
Π(x : X (n + 1)), tcc_to_fn X n x = pt → fiber (tcc_to_fn X (n+1)) x
definition is_exact_at_lt [reducible] (X : left_type_chain_complex) (n : ℕ) : Type :=
Π(x : X (n + 1)), ltcc_to_fn X n x = pt → fiber (ltcc_to_fn X (n+1)) x
definition is_exact_at_rt [reducible] (X : right_type_chain_complex) (n : ℕ) : Type :=
Π(x : X (n + 1)), rtcc_to_fn X (n+1) x = pt → fiber (rtcc_to_fn X n) x
definition is_exact_at_t [reducible] /- X n -/ : Type :=
Π(x : X (S n)), tcc_to_fn X n x = pt → fiber (tcc_to_fn X (S n)) x
definition is_exact_t [reducible] (X : type_chain_complex) : Type :=
Π(n : ℤ), is_exact_at_t X n
definition is_exact_lt [reducible] (X : left_type_chain_complex) : Type :=
Π(n : ℕ), is_exact_at_lt X n
definition is_exact_rt [reducible] (X : right_type_chain_complex) : Type :=
Π(n : ℕ), is_exact_at_rt X n
definition is_exact_t [reducible] /- X -/ : Type :=
Π(n : N), is_exact_at_t X n
definition type_chain_complex_from_left (X : left_type_chain_complex) : type_chain_complex :=
type_chain_complex.mk (int.rec X (λn, punit))
begin
intro n, fconstructor,
{ induction n with n n,
{ exact @ltcc_to_fn X n},
{ esimp, intro x, exact star}},
{ induction n with n n,
{ apply respect_pt},
{ reflexivity}}
end
begin
intro n, induction n with n n,
{ exact ltcc_is_chain_complex X},
{ esimp, intro x, reflexivity}
end
-- definition type_chain_complex_from_left (X : type_chain_complex) : type_chain_complex :=
-- type_chain_complex.mk (int.rec X (λn, punit))
-- begin
-- intro n, fconstructor,
-- { induction n with n n,
-- { exact @ltcc_to_fn X n},
-- { esimp, intro x, exact star}},
-- { induction n with n n,
-- { apply respect_pt},
-- { reflexivity}}
-- end
-- begin
-- intro n, induction n with n n,
-- { exact ltcc_is_chain_complex X},
-- { esimp, intro x, reflexivity}
-- end
definition is_exact_t_from_left {X : left_type_chain_complex} {n : ℕ} (H : is_exact_at_lt X n)
: is_exact_at_t (type_chain_complex_from_left X) n :=
H
-- definition is_exact_t_from_left {X : type_chain_complex} {n : ℕ} (H : is_exact_at_lt X n)
-- : is_exact_at_t (type_chain_complex_from_left X) n :=
-- H
definition transfer_left_type_chain_complex [constructor] (X : left_type_chain_complex)
{Y : ℕ → Type*} (g : Π{n : ℕ}, Y (n + 1) →* Y n) (e : Π{n}, X n ≃* Y n)
(p : Π{n} (x : X (n + 1)), e (ltcc_to_fn X n x) = g (e x)) : left_type_chain_complex :=
left_type_chain_complex.mk Y @g
begin
definition transfer_type_chain_complex [constructor]
{Y : N → Type*} (g : Π{n : N}, Y (S n) →* Y n) (e : Π{n}, X n ≃* Y n)
(p : Π{n} (x : X (S n)), e (tcc_to_fn X n x) = g (e x)) : type_chain_complex N :=
type_chain_complex.mk Y @g
abstract begin
intro n, apply equiv_rect (equiv_of_pequiv e), intro x,
refine ap g (p x)⁻¹ ⬝ _,
refine (p _)⁻¹ ⬝ _,
refine ap e (ltcc_is_chain_complex X _) ⬝ _,
refine ap e (tcc_is_chain_complex X n _) ⬝ _,
apply respect_pt
end
end end
definition is_exact_at_lt_transfer {X : left_type_chain_complex} {Y : ℕ → Type*}
{g : Π{n : ℕ}, Y (n + 1) →* Y n} (e : Π{n}, X n ≃* Y n)
(p : Π{n} (x : X (n + 1)), e (ltcc_to_fn X n x) = g (e x)) {n : ℕ}
(H : is_exact_at_lt X n) : is_exact_at_lt (transfer_left_type_chain_complex X @g @e @p) n :=
theorem is_exact_at_t_transfer {X : type_chain_complex N} {Y : N → Type*}
{g : Π{n : N}, Y (S n) →* Y n} (e : Π{n}, X n ≃* Y n)
(p : Π{n} (x : X (S n)), e (tcc_to_fn X n x) = g (e x)) {n : N}
(H : is_exact_at_t X n) : is_exact_at_t (transfer_type_chain_complex X @g @e @p) n :=
begin
intro y q, esimp at *,
assert H2 : ltcc_to_fn X n (e⁻¹ᵉ* y) = pt,
assert H2 : tcc_to_fn X n (e⁻¹ᵉ* y) = pt,
{ refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
refine ap _ q ⬝ _,
exact respect_pt e⁻¹ᵉ*},
@ -114,97 +156,142 @@ namespace chain_complex
apply right_inv
end
definition trunc_left_type_chain_complex [constructor] (X : left_type_chain_complex)
(k : trunc_index) : left_type_chain_complex :=
left_type_chain_complex.mk
(λn, ptrunc k (X n))
(λn, ptrunc_functor k (ltcc_to_fn X n))
-- move to init.equiv. This is inv_commute for A ≡ unit
definition inv_commute1' {B C : Type} (f : B → C) [is_equiv f] (h : B → B) (h' : C → C)
(p : Π(b : B), f (h b) = h' (f b)) (c : C) : f⁻¹ (h' c) = h (f⁻¹ c) :=
eq_of_fn_eq_fn' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹)
definition inv_commute1 {B C : Type} (f : B ≃ C) (h : B → B) (h' : C → C)
(p : Π(b : B), f (h b) = h' (f b)) (c : C) : f⁻¹ (h' c) = h (f⁻¹ c) :=
inv_commute1' (to_fun f) h h' p c
definition fn_cast_eq_cast_fn {A : Type} {P Q : A → Type} {x y : A} (p : x = y)
(f : Πx, P x → Q x) (z : P x) : f y (cast (ap P p) z) = cast (ap Q p) (f x z) :=
by induction p; reflexivity
definition cast_cast_inv {A : Type} {P : A → Type} {x y : A} (p : x = y) (z : P y) :
cast (ap P p) (cast (ap P p⁻¹) z) = z :=
by induction p; reflexivity
definition cast_inv_cast {A : Type} {P : A → Type} {x y : A} (p : x = y) (z : P x) :
cast (ap P p⁻¹) (cast (ap P p) z) = z :=
by induction p; reflexivity
-- more general transfer, where the base type can also change by an equivalence.
definition transfer_type_chain_complex2 [constructor] {M : succ_str} {Y : M → Type*}
(f : M ≃ N) (c : Π(m : M), S (f m) = f (S m))
(g : Π{m : M}, Y (S m) →* Y m) (e : Π{m}, X (f m) ≃* Y m)
(p : Π{m} (x : X (S (f m))), e (tcc_to_fn X (f m) x) = g (e (cast (ap (λx, X x) (c m)) x)))
: type_chain_complex M :=
type_chain_complex.mk Y @g
begin
intro n x, esimp at *,
refine trunc.rec _ x, -- why doesn't induction work here?
clear x, intro x, esimp,
exact ap tr (ltcc_is_chain_complex X x)
end
/- actual (set) chain complexes -/
structure chain_complex : Type :=
(car : ℤ → Set*)
(fn : Π(n : ℤ), car (n + 1) →* car n)
(is_chain_complex : Π{n : ℤ} (x : car ((n + 1) + 1)), fn n (fn (n+1) x) = pt)
structure left_chain_complex : Type := -- chain complex on the naturals with maps going down
(car : ℕ → Set*)
(fn : Π(n : ℕ), car (n + 1) →* car n)
(is_chain_complex : Π{n : ℕ} (x : car ((n + 1) + 1)), fn n (fn (n+1) x) = pt)
structure right_chain_complex : Type := -- chain complex on the naturals with maps going up
(car : ℕ → Set*)
(fn : Π(n : ℕ), car n →* car (n + 1))
(is_chain_complex : Π{n : ℕ} (x : car n), fn (n+1) (fn n x) = pt)
definition cc_to_car [unfold 1] [coercion] := @chain_complex.car
definition cc_to_fn [unfold 1] := @chain_complex.fn
definition cc_is_chain_complex [unfold 1] := @chain_complex.is_chain_complex
definition lcc_to_car [unfold 1] [coercion] := @left_chain_complex.car
definition lcc_to_fn [unfold 1] := @left_chain_complex.fn
definition lcc_is_chain_complex [unfold 1] := @left_chain_complex.is_chain_complex
definition rcc_to_car [unfold 1] [coercion] := @right_chain_complex.car
definition rcc_to_fn [unfold 1] := @right_chain_complex.fn
definition rcc_is_chain_complex [unfold 1] := @right_chain_complex.is_chain_complex
-- important: these notions are shifted by one! (this is to avoid transports)
definition is_exact_at [reducible] (X : chain_complex) (n : ℤ) : Type :=
Π(x : X (n + 1)), cc_to_fn X n x = pt → image (cc_to_fn X (n+1)) x
definition is_exact_at_l [reducible] (X : left_chain_complex) (n : ℕ) : Type :=
Π(x : X (n + 1)), lcc_to_fn X n x = pt → image (lcc_to_fn X (n+1)) x
definition is_exact_at_r [reducible] (X : right_chain_complex) (n : ℕ) : Type :=
Π(x : X (n + 1)), rcc_to_fn X (n+1) x = pt → image (rcc_to_fn X n) x
definition is_exact [reducible] (X : chain_complex) : Type := Π(n : ℤ), is_exact_at X n
definition is_exact_l [reducible] (X : left_chain_complex) : Type := Π(n : ℕ), is_exact_at_l X n
definition is_exact_r [reducible] (X : right_chain_complex) : Type := Π(n : ℕ), is_exact_at_r X n
definition chain_complex_from_left (X : left_chain_complex) : chain_complex :=
chain_complex.mk (int.rec X (λn, punit))
begin
intro n, fconstructor,
{ induction n with n n,
{ exact @lcc_to_fn X n},
{ esimp, intro x, exact star}},
{ induction n with n n,
{ apply respect_pt},
{ reflexivity}}
end
begin
intro n, induction n with n n,
{ exact lcc_is_chain_complex X},
{ esimp, intro x, reflexivity}
end
definition is_exact_from_left {X : left_chain_complex} {n : ℕ} (H : is_exact_at_l X n)
: is_exact_at (chain_complex_from_left X) n :=
H
definition transfer_left_chain_complex [constructor] (X : left_chain_complex) {Y : ℕ → Set*}
(g : Π{n : ℕ}, Y (n + 1) →* Y n) (e : Π{n}, X n ≃* Y n)
(p : Π{n} (x : X (n + 1)), e (lcc_to_fn X n x) = g (e x)) : left_chain_complex :=
left_chain_complex.mk Y @g
begin
intro n, apply equiv_rect (equiv_of_pequiv e), intro x,
refine ap g (p x)⁻¹ ⬝ _,
intro m,
apply equiv_rect (equiv_of_pequiv e),
apply equiv_rect (equiv_of_eq (ap (λx, X x) (c (S m)))), esimp,
apply equiv_rect (equiv_of_eq (ap (λx, X (S x)) (c m))), esimp,
intro x, refine ap g (p _)⁻¹ ⬝ _,
refine ap g (ap e (fn_cast_eq_cast_fn (c m) (tcc_to_fn X) x)) ⬝ _,
refine (p _)⁻¹ ⬝ _,
refine ap e (lcc_is_chain_complex X _) ⬝ _,
refine ap e (tcc_is_chain_complex X (f m) _) ⬝ _,
apply respect_pt
end
definition transfer_is_exact_at_l (X : left_chain_complex) {Y : ℕ → Set*}
(g : Π{n : ℕ}, Y (n + 1) →* Y n) (e : Π{n}, X n ≃* Y n)
(p : Π{n} (x : X (n + 1)), e (lcc_to_fn X n x) = g (e x))
{n : ℕ} (H : is_exact_at_l X n) : is_exact_at_l (transfer_left_chain_complex X @g @e @p) n :=
definition is_exact_at_transfer2 {X : type_chain_complex N} {M : succ_str} {Y : M → Type*}
(f : M ≃ N) (c : Π(m : M), S (f m) = f (S m))
(g : Π{m : M}, Y (S m) →* Y m) (e : Π{m}, X (f m) ≃* Y m)
(p : Π{m} (x : X (S (f m))), e (tcc_to_fn X (f m) x) = g (e (cast (ap (λx, X x) (c m)) x)))
{m : M} (H : is_exact_at_t X (f m))
: is_exact_at_t (transfer_type_chain_complex2 X f c @g @e @p) m :=
begin
intro y q, esimp at *,
assert H2 : lcc_to_fn X n (e⁻¹ᵉ* y) = pt,
assert H2 : tcc_to_fn X (f m) ((equiv_of_eq (ap (λx, X x) (c m)))⁻¹ᵉ (e⁻¹ y)) = pt,
{ refine _ ⬝ ap e⁻¹ᵉ* q ⬝ (respect_pt (e⁻¹ᵉ*)), apply eq_inv_of_eq, clear q, revert y,
refine inv_homotopy_of_homotopy (pequiv.to_equiv e) _,
apply inv_homotopy_of_homotopy, apply p},
induction (H _ H2) with x r,
refine fiber.mk (e (cast (ap (λx, X x) (c (S m))) (cast (ap (λx, X (S x)) (c m)) x))) _,
refine (p _)⁻¹ ⬝ _,
refine ap e (fn_cast_eq_cast_fn (c m) (tcc_to_fn X) x) ⬝ _,
refine ap (λx, e (cast _ x)) r ⬝ _,
esimp [equiv.symm], rewrite [-ap_inv],
refine ap e !cast_cast_inv ⬝ _,
apply right_inv
end
-- definition trunc_type_chain_complex [constructor] (X : type_chain_complex N)
-- (k : trunc_index) : type_chain_complex N :=
-- type_chain_complex.mk
-- (λn, ptrunc k (X n))
-- (λn, ptrunc_functor k (tcc_to_fn X n))
-- begin
-- intro n x, esimp at *,
-- refine trunc.rec _ x, -- why doesn't induction work here?
-- clear x, intro x, esimp,
-- exact ap tr (tcc_is_chain_complex X n x)
-- end
end
/- actual (set) chain complexes -/
structure chain_complex (N : succ_str) : Type :=
(car : N → Set*)
(fn : Π(n : N), car (S n) →* car n)
(is_chain_complex : Π(n : N) (x : car (S (S n))), fn n (fn (S n) x) = pt)
section
variables {N : succ_str} (X : chain_complex N) (n : N)
definition cc_to_car [unfold 2] [coercion] := @chain_complex.car
definition cc_to_fn [unfold 2] : X (S n) →* X n := @chain_complex.fn N X n
definition cc_is_chain_complex [unfold 2]
: Π(x : X (S (S n))), cc_to_fn X n (cc_to_fn X (S n) x) = pt :=
@chain_complex.is_chain_complex N X n
-- important: these notions are shifted by one! (this is to avoid transports)
definition is_exact_at [reducible] /- X n -/ : Type :=
Π(x : X (S n)), cc_to_fn X n x = pt → image (cc_to_fn X (S n)) x
definition is_exact [reducible] /- X -/ : Type := Π(n : N), is_exact_at X n
-- definition chain_complex_from_left (X : chain_complex) : chain_complex :=
-- chain_complex.mk (int.rec X (λn, punit))
-- begin
-- intro n, fconstructor,
-- { induction n with n n,
-- { exact @lcc_to_fn X n},
-- { esimp, intro x, exact star}},
-- { induction n with n n,
-- { apply respect_pt},
-- { reflexivity}}
-- end
-- begin
-- intro n, induction n with n n,
-- { exact lcc_is_chain_complex X},
-- { esimp, intro x, reflexivity}
-- end
-- definition is_exact_from_left {X : chain_complex} {n : ℕ} (H : is_exact_at_l X n)
-- : is_exact_at (chain_complex_from_left X) n :=
-- H
definition transfer_chain_complex [constructor] {Y : N → Set*}
(g : Π{n : N}, Y (S n) →* Y n) (e : Π{n}, X n ≃* Y n)
(p : Π{n} (x : X (S n)), e (cc_to_fn X n x) = g (e x)) : chain_complex N :=
chain_complex.mk Y @g
abstract begin
intro n, apply equiv_rect (equiv_of_pequiv e), intro x,
refine ap g (p x)⁻¹ ⬝ _,
refine (p _)⁻¹ ⬝ _,
refine ap e (cc_is_chain_complex X n _) ⬝ _,
apply respect_pt
end end
theorem is_exact_at_transfer {X : chain_complex N} {Y : N → Set*}
(g : Π{n : N}, Y (S n) →* Y n) (e : Π{n}, X n ≃* Y n)
(p : Π{n} (x : X (S n)), e (cc_to_fn X n x) = g (e x))
{n : N} (H : is_exact_at X n) : is_exact_at (transfer_chain_complex X @g @e @p) n :=
begin
intro y q, esimp at *,
assert H2 : cc_to_fn X n (e⁻¹ᵉ* y) = pt,
{ refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
refine ap _ q ⬝ _,
exact respect_pt e⁻¹ᵉ*},
@ -216,20 +303,20 @@ namespace chain_complex
apply right_inv
end
definition trunc_left_chain_complex [constructor] (X : left_type_chain_complex)
: left_chain_complex :=
left_chain_complex.mk
definition trunc_chain_complex [constructor] (X : type_chain_complex N)
: chain_complex N :=
chain_complex.mk
(λn, ptrunc 0 (X n))
(λn, ptrunc_functor 0 (ltcc_to_fn X n))
(λn, ptrunc_functor 0 (tcc_to_fn X n))
begin
intro n x, esimp at *,
refine @trunc.rec _ _ _ (λH, !is_trunc_eq) _ x,
clear x, intro x, esimp,
exact ap tr (ltcc_is_chain_complex X x)
exact ap tr (tcc_is_chain_complex X n x)
end
definition is_exact_at_l_trunc (X : left_type_chain_complex) {n : ℕ}
(H : is_exact_at_lt X n) : is_exact_at_l (trunc_left_chain_complex X) n :=
definition is_exact_at_trunc (X : type_chain_complex N) {n : N}
(H : is_exact_at_t X n) : is_exact_at (trunc_chain_complex X) n :=
begin
intro x p, esimp at *,
induction x with x, esimp at *,
@ -240,4 +327,199 @@ namespace chain_complex
esimp, exact ap tr r
end
definition transfer_chain_complex2' [constructor] {M : succ_str} {Y : M → Set*}
(f : N ≃ M) (c : Π(n : N), f (S n) = S (f n))
(g : Π{m : M}, Y (S m) →* Y m) (e : Π{n}, X n ≃* Y (f n))
(p : Π{n} (x : X (S n)), e (cc_to_fn X n x) = g (c n ▸ e x)) : chain_complex M :=
chain_complex.mk Y @g
begin
refine equiv_rect f _ _, intro n,
assert H : Π (x : Y (f (S (S n)))), g (c n ▸ g (c (S n) ▸ x)) = pt,
{ apply equiv_rect (equiv_of_pequiv e), intro x,
refine ap (λx, g (c n ▸ x)) (@p (S n) x)⁻¹ᵖ ⬝ _,
refine (p _)⁻¹ ⬝ _,
refine ap e (cc_is_chain_complex X n _) ⬝ _,
apply respect_pt},
refine pi.pi_functor _ _ H,
{ intro x, exact (c (S n))⁻¹ ▸ (c n)⁻¹ ▸ x}, -- with implicit arguments, this is:
-- transport (λx, Y x) (c (S n))⁻¹ (transport (λx, Y (S x)) (c n)⁻¹ x)
{ intro x, intro p, refine _ ⬝ p, rewrite [tr_inv_tr, fn_tr_eq_tr_fn (c n)⁻¹ @g, tr_inv_tr]}
end
definition is_exact_at_transfer2' {X : chain_complex N} {M : succ_str} {Y : M → Set*}
(f : N ≃ M) (c : Π(n : N), f (S n) = S (f n))
(g : Π{m : M}, Y (S m) →* Y m) (e : Π{n}, X n ≃* Y (f n))
(p : Π{n} (x : X (S n)), e (cc_to_fn X n x) = g (c n ▸ e x))
{n : N} (H : is_exact_at X n) : is_exact_at (transfer_chain_complex2' X f c @g @e @p) (f n) :=
begin
intro y q, esimp at *,
assert H2 : cc_to_fn X n (e⁻¹ᵉ* ((c n)⁻¹ ▸ y)) = pt,
{ refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
rewrite [tr_inv_tr, q],
exact respect_pt e⁻¹ᵉ*},
induction (H _ H2) with x,
induction x with x r,
refine image.mk (c n ▸ c (S n) ▸ e x) _,
rewrite [fn_tr_eq_tr_fn (c n) @g],
refine ap (λx, c n ▸ x) (p x)⁻¹ ⬝ _,
refine ap (λx, c n ▸ e x) r ⬝ _,
refine ap (λx, c n ▸ x) !right_inv ⬝ _,
apply tr_inv_tr,
end
-- structure group_chain_complex : Type :=
-- (car : N → Group)
-- (fn : Π(n : N), car (S n) →g car n)
-- (is_chain_complex : Π{n : N} (x : car ((S n) + 1)), fn n (fn (S n) x) = 1)
-- structure group_chain_complex : Type := -- chain complex on the naturals with maps going down
-- (car : N → Group)
-- (fn : Π(n : N), car (S n) →g car n)
-- (is_chain_complex : Π{n : N} (x : car ((S n) + 1)), fn n (fn (S n) x) = 1)
-- structure right_group_chain_complex : Type := -- chain complex on the naturals with maps going up
-- (car : N → Group)
-- (fn : Π(n : N), car n →g car (S n))
-- (is_chain_complex : Π{n : N} (x : car n), fn (S n) (fn n x) = 1)
-- definition gcc_to_car [unfold 1] [coercion] := @group_chain_complex.car
-- definition gcc_to_fn [unfold 1] := @group_chain_complex.fn
-- definition gcc_is_chain_complex [unfold 1] := @group_chain_complex.is_chain_complex
-- definition lgcc_to_car [unfold 1] [coercion] := @left_group_chain_complex.car
-- definition lgcc_to_fn [unfold 1] := @left_group_chain_complex.fn
-- definition lgcc_is_chain_complex [unfold 1] := @left_group_chain_complex.is_chain_complex
-- definition rgcc_to_car [unfold 1] [coercion] := @right_group_chain_complex.car
-- definition rgcc_to_fn [unfold 1] := @right_group_chain_complex.fn
-- definition rgcc_is_chain_complex [unfold 1] := @right_group_chain_complex.is_chain_complex
-- -- important: these notions are shifted by one! (this is to avoid transports)
-- definition is_exact_at_g [reducible] (X : group_chain_complex) (n : N) : Type :=
-- Π(x : X (S n)), gcc_to_fn X n x = 1 → image (gcc_to_fn X (S n)) x
-- definition is_exact_at_lg [reducible] (X : left_group_chain_complex) (n : N) : Type :=
-- Π(x : X (S n)), lgcc_to_fn X n x = 1 → image (lgcc_to_fn X (S n)) x
-- definition is_exact_at_rg [reducible] (X : right_group_chain_complex) (n : N) : Type :=
-- Π(x : X (S n)), rgcc_to_fn X (S n) x = 1 → image (rgcc_to_fn X n) x
-- definition is_exact_g [reducible] (X : group_chain_complex) : Type :=
-- Π(n : N), is_exact_at_g X n
-- definition is_exact_lg [reducible] (X : left_group_chain_complex) : Type :=
-- Π(n : N), is_exact_at_lg X n
-- definition is_exact_rg [reducible] (X : right_group_chain_complex) : Type :=
-- Π(n : N), is_exact_at_rg X n
-- definition group_chain_complex_from_left (X : left_group_chain_complex) : group_chain_complex :=
-- group_chain_complex.mk (int.rec X (λn, G0))
-- begin
-- intro n, fconstructor,
-- { induction n with n n,
-- { exact @lgcc_to_fn X n},
-- { esimp, intro x, exact star}},
-- { induction n with n n,
-- { apply respect_mul},
-- { intro g h, reflexivity}}
-- end
-- begin
-- intro n, induction n with n n,
-- { exact lgcc_is_chain_complex X},
-- { esimp, intro x, reflexivity}
-- end
-- definition is_exact_g_from_left {X : left_group_chain_complex} {n : N} (H : is_exact_at_lg X n)
-- : is_exact_at_g (group_chain_complex_from_left X) n :=
-- H
-- definition transfer_left_group_chain_complex [constructor] (X : left_group_chain_complex)
-- {Y : N → Group} (g : Π{n : N}, Y (S n) →g Y n) (e : Π{n}, X n ≃* Y n)
-- (p : Π{n} (x : X (S n)), e (lgcc_to_fn X n x) = g (e x)) : left_group_chain_complex :=
-- left_group_chain_complex.mk Y @g
-- begin
-- intro n, apply equiv_rect (pequiv_of_equiv e), intro x,
-- refine ap g (p x)⁻¹ ⬝ _,
-- refine (p _)⁻¹ ⬝ _,
-- refine ap e (lgcc_is_chain_complex X _) ⬝ _,
-- exact respect_pt
-- end
-- definition is_exact_at_t_transfer {X : left_group_chain_complex} {Y : N → Type*}
-- {g : Π{n : N}, Y (S n) →* Y n} (e : Π{n}, X n ≃* Y n)
-- (p : Π{n} (x : X (S n)), e (lgcc_to_fn X n x) = g (e x)) {n : N}
-- (H : is_exact_at_lg X n) : is_exact_at_lg (transfer_left_group_chain_complex X @g @e @p) n :=
-- begin
-- intro y q, esimp at *,
-- assert H2 : lgcc_to_fn X n (e⁻¹ᵉ* y) = pt,
-- { refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
-- refine ap _ q ⬝ _,
-- exact respect_pt e⁻¹ᵉ*},
-- cases (H _ H2) with x r,
-- refine image.mk (e x) _,
-- refine (p x)⁻¹ ⬝ _,
-- refine ap e r ⬝ _,
-- apply right_inv
-- end
-- TODO: move
definition is_trunc_ptrunctype [instance] {n : trunc_index} (X : ptrunctype n)
: is_trunc n (ptrunctype.to_pType X) :=
trunctype.struct X
/- a group where the point in the pointed corresponds with 1 in the group -/
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)
(mul_left_inv_pt : Πa, mul (inv a) a = pt)
definition group_of_pgroup [reducible] [instance] (X : Type*) [H : pgroup X]
: group X :=
⦃group, H,
one := pt,
one_mul := pgroup.pt_mul ,
mul_one := pgroup.mul_pt,
mul_left_inv := pgroup.mul_left_inv_pt⦄
definition pgroup_of_group (X : Type*) [H : group X] (p : one = pt :> X) : pgroup X :=
begin
cases X with X x, esimp at *, induction p,
exact ⦃pgroup, H,
pt_mul := one_mul,
mul_pt := mul_one,
mul_left_inv_pt := mul.left_inv⦄
end
definition is_embedding_of_trivial (X : chain_complex N) {n : N}
(H : is_exact_at X n) [HX : is_prop (X (S (S n)))]
[pgroup (X n)] [pgroup (X (S n))] [is_homomorphism (cc_to_fn X n)]
: is_embedding (cc_to_fn X n) :=
begin
apply is_embedding_homomorphism,
intro g p,
induction H g p with v,
induction v with x q,
assert r : pt = x, exact @is_prop.elim _ HX _ _,
induction r,
refine q⁻¹ ⬝ _,
apply respect_pt
end
definition is_surjective_of_trivial (X : chain_complex N) {n : N}
(H : is_exact_at X n) [HX : is_prop (X n)] : is_surjective (cc_to_fn X (S n)) :=
begin
intro g,
refine trunc.elim _ (H g (@is_prop.elim _ HX _ _)),
apply tr
end
definition is_equiv_of_trivial (X : chain_complex N) {n : N}
(H1 : is_exact_at X n) (H2 : is_exact_at X (S n))
[HX1 : is_prop (X n)] [HX2 : is_prop (X (S (S (S n))))]
[pgroup (X (S n))] [pgroup (X (S (S n)))] [is_homomorphism (cc_to_fn X (S n))]
: is_equiv (cc_to_fn X (S n)) :=
begin
apply is_equiv_of_is_surjective_of_is_embedding,
{ apply is_embedding_of_trivial X, apply H2},
{ apply is_surjective_of_trivial X, apply H1},
end
end
end chain_complex

59
homotopy/fin.hlean Normal file
View file

@ -0,0 +1,59 @@
/-
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
Finite ordinal types.
-/
import types.fin
open eq nat fin algebra
inductive is_succ [class] : ℕ → Type :=
| mk : Πn, is_succ (succ n)
attribute is_succ.mk [instance]
definition is_succ_add_right [instance] (n m : ℕ) [H : is_succ m] : is_succ (n+m) :=
by induction H with m; constructor
definition is_succ_add_left (n m : ℕ) [H : is_succ n] : is_succ (n+m) :=
by induction H with n; cases m with m: constructor
definition is_succ_bit0 [instance] (n : ℕ) [H : is_succ n] : is_succ (bit0 n) :=
by induction H with n; constructor
namespace fin
definition my_succ {n : ℕ} (x : fin n) : fin n :=
begin
cases n with n,
{ exfalso, apply not_lt_zero _ (is_lt x)},
{ exact
if H : val x = n
then fin.mk 0 !zero_lt_succ
else fin.mk (nat.succ (val x)) (succ_lt_succ (lt_of_le_of_ne (le_of_lt_succ (is_lt x)) H))}
end
protected definition add {n : ℕ} (x y : fin n) : fin n :=
iterate my_succ (val y) x
definition has_zero_fin [instance] (n : ℕ) [H : is_succ n] : has_zero (fin n) :=
by induction H with n; exact has_zero.mk (fin.zero n)
definition has_one_fin [instance] (n : ℕ) [H : is_succ n] : has_one (fin n) :=
by induction H with n; exact has_one.mk (my_succ (fin.zero n))
definition has_add_fin [instance] (n : ℕ) : has_add (fin n) :=
has_add.mk fin.add
-- definition my_succ_eq_zero {n : ℕ} (x : fin (nat.succ n)) (p : val x = n) : my_succ x = 0 :=
-- if H : val x = n
-- then fin.mk 0 !zero_lt_succ
-- else fin.mk (nat.succ (val x)) (succ_lt_succ (lt_of_le_of_ne (le_of_lt_succ (is_lt x)) H))
end fin

97
homotopy/homotopy_groups.hlean Normal file
View file

@ -0,0 +1,97 @@
/-
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
-/
-- to be moved to algebra/homotopy_group in the Lean library
import group_theory.basic algebra.homotopy_group
open eq algebra pointed group trunc is_trunc nat algebra equiv equiv.ops is_equiv
namespace my
section
variables {A B C : Type*}
definition apn_compose (n : ℕ) (g : B →* C) (f : A →* B) : apn n (g ∘* f) ~* apn n g ∘* apn n f :=
begin
induction n with n IH,
{ reflexivity},
{ refine ap1_phomotopy IH ⬝* _, apply ap1_compose}
end
theorem ap1_con (f : A →* B) (p q : Ω A) : ap1 f (p ⬝ q) = ap1 f p ⬝ ap1 f q :=
begin
rewrite [▸*, ap_con, +con.assoc, con_inv_cancel_left]
end
definition apn_con {n : ℕ} (f : A →* B) (p q : Ω[n + 1] A)
: apn (n+1) f (p ⬝ q) = apn (n+1) f p ⬝ apn (n+1) f q :=
ap1_con (apn n f) p q
definition tr_mul {n : ℕ} (p q : Ω[n + 1] A) : @mul (πg[n+1] A) _ (tr p ) (tr q) = tr (p ⬝ q) :=
by reflexivity
end
section
parameters {A B : Type} (f : A ≃ B) [group A]
definition group_equiv_mul (b b' : B) : B := f (f⁻¹ᶠ b * f⁻¹ᶠ b')
definition group_equiv_one : B := f one
definition group_equiv_inv (b : B) : B := f (f⁻¹ᶠ b)⁻¹
local infix * := my.group_equiv_mul f
local postfix ^ := my.group_equiv_inv f
local notation 1 := my.group_equiv_one f
theorem group_equiv_mul_assoc (b₁ b₂ b₃ : B) : (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) :=
by rewrite [↑group_equiv_mul, +left_inv f, mul.assoc]
theorem group_equiv_one_mul (b : B) : 1 * b = b :=
by rewrite [↑group_equiv_mul, ↑group_equiv_one, left_inv f, one_mul, right_inv f]
theorem group_equiv_mul_one (b : B) : b * 1 = b :=
by rewrite [↑group_equiv_mul, ↑group_equiv_one, left_inv f, mul_one, right_inv f]
theorem group_equiv_mul_left_inv (b : B) : b^ * b = 1 :=
by rewrite [↑group_equiv_mul, ↑group_equiv_one, ↑group_equiv_inv,
+left_inv f, mul.left_inv]
definition group_equiv_closed : group B :=
⦃group,
mul := group_equiv_mul,
mul_assoc := group_equiv_mul_assoc,
one := group_equiv_one,
one_mul := group_equiv_one_mul,
mul_one := group_equiv_mul_one,
inv := group_equiv_inv,
mul_left_inv := group_equiv_mul_left_inv,
is_set_carrier := is_trunc_equiv_closed 0 f⦄
end
end my open my
namespace eq
local attribute mul [unfold 2]
definition homotopy_group_homomorphism [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
: πg[n+1] A →g πg[n+1] B :=
begin
fconstructor,
{ exact phomotopy_group_functor (n+1) f},
{ intro g,
refine @trunc.rec _ _ _ (λx, !is_trunc_eq) _, intro h,
refine @trunc.rec _ _ _ (λx, !is_trunc_eq) _ g, clear g, intro g,
rewrite [tr_mul, ▸*],
apply ap tr, apply apn_con}
end
notation `π→g[`:95 n:0 ` +1] `:0 f:95 := homotopy_group_homomorphism n f
end eq

57
homotopy/sec83.hlean
View file

@ -2,48 +2,43 @@
import types.trunc types.pointed homotopy.connectedness homotopy.sphere homotopy.circle algebra.group algebra.homotopy_group
open eq is_trunc is_equiv nat equiv trunc function circle algebra pointed is_trunc.trunc_index homotopy
open eq is_trunc is_equiv nat equiv trunc function circle algebra pointed trunc_index homotopy
notation `Floris` := sorry
-- Lemma 8.3.1
definition homotopy_group_of_is_trunc (A : Type*) (n : ℕ) (p : is_trunc n A) : ∀(k : ℕ), πG[n+k+1] A = G0 :=
theorem trivial_homotopy_group_of_is_trunc (A : Type*) (n k : ℕ) [is_trunc n A] (H : n ≤ k)
: is_contr (πg[k+1] A) :=
begin
intro k,
apply @trivial_group_of_is_contr,
apply is_trunc_trunc_of_is_trunc,
apply is_contr_loop_of_is_trunc,
apply @is_trunc_of_leq A n _,
induction k with k IHk,
{
apply is_trunc.trunc_index.le.refl
},
{
induction n with n IHn,
{
constructor
},
{
exact Floris
}
}
apply @is_trunc_of_le A n _,
exact of_nat_le_of_nat H
end
-- Lemma 8.3.2
definition trunc_trunc (n k : ℕ₋₂) (p : k ≤ n) (A : Type)
: trunc k (trunc n A) ≃ trunc k A :=
sorry
definition zero_trunc_of_iterated_loop_space (k : ℕ) (A : Type*)
: trunc 0 (Ω[k] A) ≃ Ω[k](pointed.MK (trunc k A) (tr pt)) :=
sorry
definition homotopy_group_of_is_conn (A : Type*) (n : ℕ) (p : is_conn n A) : ∀(k : ℕ), (k ≤ n) → is_contr(π[k] A) :=
theorem trivial_homotopy_group_of_is_conn (A : Type*) {k n : ℕ} (H : k ≤ n) [is_conn n A]
: is_contr (π[k] A) :=
begin
intros k H,
exact Floris
have H2 : of_nat k ≤ of_nat n, from of_nat_le_of_nat H,
have H3 : is_contr (ptrunc k A),
begin
fapply is_contr_equiv_closed,
{ apply trunc_trunc_equiv_left _ k n H2}
end,
have H4 : is_contr (Ω[k](ptrunc k A)),
from !is_trunc_loop_of_is_trunc,
apply is_trunc_equiv_closed_rev,
{ apply equiv_of_pequiv (phomotopy_group_pequiv_loop_ptrunc k A)}
end
-- Corollary 8.3.3
open sphere.ops sphere_index
theorem homotopy_group_sphere_le (n k : ℕ) (H : k < n) : is_contr (π[k] (S. n)) :=
begin
cases n with n,
{ exfalso, apply not_lt_zero, exact H},
{ have H2 : k ≤ n, from le_of_lt_succ H,
apply @(trivial_homotopy_group_of_is_conn _ H2),
rewrite [-trunc_index.of_sphere_index_of_nat, -trunc_index.succ_sub_one], apply is_conn_sphere}
end

45
homotopy/sec86.hlean Normal file
View file

@ -0,0 +1,45 @@
import homotopy.wedge types.pi
open eq homotopy is_trunc pointed susp nat pi equiv equiv.ops is_equiv trunc
section freudenthal
parameters {A : Type*} (n : ℕ) [is_conn n A]
--set_option pp.notation false
protected definition my_wedge_extension.ext : Π {A : Type*} {B : Type*} (n m : ℕ) [cA : is_conn n (carrier A)] [cB : is_conn m (carrier B)]
(P : carrier A → carrier B → (m+n)-Type) (f : Π (a : carrier A), trunctype.carrier (P a (Point B)))
(g : Π (b : carrier B), trunctype.carrier (P (Point A) b)),
f (Point A) = g (Point B) → (Π (a : carrier A) (b : carrier B), trunctype.carrier (P a b)) :=
sorry
definition code_fun (a : A) (q : north = north :> susp A)
: trunc (n * 2) (fiber (pmap.to_fun (loop_susp_unit A)) q) → trunc (n * 2) (fiber merid (q ⬝ merid a)) :=
begin
intro x, induction x with x,
esimp at *, cases x with a' p,
-- apply my_wedge_extension.ext n n,
exact sorry
end
definition code (y : susp A) : north = y → Type :=
susp.rec_on y
(λp, trunc (2*n) (fiber (loop_susp_unit A) p))
(λq, trunc (2*n) (fiber merid q))
begin
intros,
apply arrow_pathover_constant_right,
intro q, rewrite [transport_eq_r],
apply ua,
exact sorry
end
definition freudenthal_suspension : is_conn_map (n*2) (loop_susp_unit A) :=
sorry
end freudenthal