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

move files to the HoTT library and update after changes in the HoTT library

Browse source
This commit is contained in:
Floris van Doorn 2016-04-25 19:51:17 -04:00
parent 0af9c0ecc7
commit ba7b25d00f
10 changed files with 11 additions and 2527 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
group_theory/constructions.hlean → algebra/group_constructions.hlean
View file

@ -3,10 +3,10 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
Constructions of groups
Constructions with groups
-/
import .basic hit.set_quotient types.sigma types.list types.sum
import algebra.group_theory hit.set_quotient types.sigma types.list types.sum
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
equiv

202
group_theory/basic.hlean
View file

@ -1,202 +0,0 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
Basic group theory
-/
/-
Groups are defined in the HoTT library in algebra/group, as part of the algebraic hierarchy.
However, there is currently no group theory.
The only relevant defintions are the trivial group (in types/unit) and some files in algebra/
-/
import types.pointed types.pi algebra.bundled algebra.category.category
open eq algebra pointed function is_trunc pi category equiv is_equiv
set_option class.force_new true
namespace group
definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one
definition pType_of_Group [reducible] (G : Group) : Type* := pointed.mk' G
definition Set_of_Group (G : Group) : Set := trunctype.mk G _
definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group :=
Group.mk G _
definition comm_group_Group_of_CommGroup [instance] [constructor] (G : CommGroup)
: 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 -/
definition is_homomorphism [class] [reducible]
{G₁ G₂ : Type} [group G₁] [group G₂] (φ : G₁ → G₂) : Type :=
Π(g h : G₁), φ (g * h) = φ g * φ h
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 φ]
definition respect_mul /- φ -/ : Π(g h : G₁), φ (g * h) = φ g * φ h :=
by assumption
theorem respect_one /- φ -/ : φ 1 = 1 :=
mul.right_cancel
(calc
φ 1 * φ 1 = φ (1 * 1) : respect_mul φ
... = φ 1 : ap φ !one_mul
... = 1 * φ 1 : one_mul)
theorem respect_inv /- φ -/ (g : G₁) : φ g⁻¹ = (φ g)⁻¹ :=
eq_inv_of_mul_eq_one (!respect_mul⁻¹ ⬝ ap φ !mul.left_inv ⬝ !respect_one)
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
have H : G₁ →g G₂ ≃ Σ(f : G₁ → G₂), Π(g₁ g₂ : G₁), f (g₁ * g₂) = f g₁ * f g₂,
begin
fapply equiv.MK,
{ intro φ, induction φ, constructor, assumption},
{ intro v, induction v, constructor, assumption},
{ intro v, induction v, reflexivity},
{ intro φ, induction φ, reflexivity}
end,
apply is_trunc_equiv_closed_rev, exact H
end
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 φ₂) : φ₁ = φ₂ :=
begin
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 (ψ ∘ φ) (is_homomorphism_compose _ _)
definition homomorphism_id [constructor] (G : Group) : G →g G :=
homomorphism.mk (@id G) (is_homomorphism_id G)
infixr ` ∘g `:75 := homomorphism_compose
notation 1 := homomorphism_id _
structure isomorphism (A B : Group) :=
(to_hom : A →g B)
(is_equiv_to_hom : is_equiv to_hom)
infix ` ≃g `:25 := isomorphism
attribute isomorphism.to_hom [coercion]
attribute isomorphism.is_equiv_to_hom [instance]
definition equiv_of_isomorphism [constructor] (φ : G₁ ≃g G₂) : G₁ ≃ G₂ :=
equiv.mk φ _
definition to_ginv [constructor] (φ : G₁ ≃g G₂) : G₂ →g G₁ :=
homomorphism.mk φ⁻¹
abstract begin
intro g₁ g₂, apply eq_of_fn_eq_fn' φ,
rewrite [respect_mul φ, +right_inv φ]
end end
definition isomorphism.refl [refl] [constructor] (G : Group) : G ≃g G :=
isomorphism.mk 1 !is_equiv_id
definition isomorphism.symm [symm] [constructor] (φ : G₁ ≃g G₂) : G₂ ≃g G₁ :=
isomorphism.mk (to_ginv φ) !is_equiv_inv
definition isomorphism.trans [trans] [constructor] (φ : G₁ ≃g G₂) (ψ : G₂ ≃g G₃)
: G₁ ≃g G₃ :=
isomorphism.mk (ψ ∘g φ) !is_equiv_compose
postfix `⁻¹ᵍ`:(max + 1) := isomorphism.symm
infixl ` ⬝g `:75 := isomorphism.trans
-- TODO
-- definition Group_univalence (G₁ G₂ : Group) : (G₁ ≃g G₂) ≃ (G₁ = G₂) :=
-- begin
-- fapply equiv.MK,
-- { intro φ, fapply Group_eq, apply equiv_of_isomorphism φ, apply respect_mul},
-- { intro p, apply transport _ p, reflexivity},
-- { intro p, induction p, esimp, },
-- { }
-- end
/- category of groups -/
definition precategory_group [constructor] : precategory Group :=
precategory.mk homomorphism
@homomorphism_compose
@homomorphism_id
(λG₁ G₂ G₃ G₄ φ₃ φ₂ φ₁, homomorphism_eq (λg, idp))
(λG₁ G₂ φ, homomorphism_eq (λg, idp))
(λG₁ G₂ φ, homomorphism_eq (λg, idp))
-- TODO
-- definition category_group : category Group :=
-- category.mk precategory_group
-- begin
-- intro G₁ G₂,
-- fapply adjointify,
-- { intro φ, fapply Group_eq, },
-- { },
-- { }
-- end
end group

365
homotopy/LES_applications.hlean
View file

@ -1,365 +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
-/
import .LES_of_homotopy_groups homotopy.connectedness homotopy.homotopy_group homotopy.join
homotopy.complex_hopf types.lift
open eq is_trunc pointed is_conn is_equiv fiber equiv trunc nat chain_complex fin algebra
group trunc_index function join pushout prod sigma sigma.ops
namespace nat
open sigma sum
definition eq_even_or_eq_odd (n : ℕ) : (Σk, 2 * k = n) ⊎ (Σk, 2 * k + 1 = n) :=
begin
induction n with n IH,
{ exact inl ⟨0, idp⟩},
{ induction IH with H H: induction H with k p: induction p,
{ exact inr ⟨k, idp⟩},
{ refine inl ⟨k+1, idp⟩}}
end
definition rec_on_even_odd {P : ℕ → Type} (n : ℕ) (H : Πk, P (2 * k)) (H2 : Πk, P (2 * k + 1))
: P n :=
begin
cases eq_even_or_eq_odd n with v v: induction v with k p: induction p,
{ exact H k},
{ exact H2 k}
end
end nat
open nat
namespace pointed
definition apn_phomotopy {A B : Type*} {f g : A →* B} (n : ℕ) (p : f ~* g)
: apn n f ~* apn n g :=
begin
induction n with n IH,
{ exact p},
{ exact ap1_phomotopy IH}
end
end pointed open pointed
namespace chain_complex
section
universe variable u
parameters {F X Y : pType.{u}} (f : X →* Y) (g : F →* X) (e : pfiber f ≃* F)
(p : ppoint f ~* g ∘* e)
include f p
open succ_str
definition fibration_sequence_car [reducible] : +3ℕ → Type*
| (n, fin.mk 0 H) := Ω[n] Y
| (n, fin.mk 1 H) := Ω[n] X
| (n, fin.mk k H) := Ω[n] F
definition fibration_sequence_fun
: Π(n : +3ℕ), fibration_sequence_car (S n) →* fibration_sequence_car n
| (n, fin.mk 0 H) := proof Ω→[n] f qed
| (n, fin.mk 1 H) := proof Ω→[n] g qed
| (n, fin.mk 2 H) := proof Ω→[n] (e ∘* boundary_map f) ∘* pcast (loop_space_succ_eq_in Y n) qed
| (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition fibration_sequence_pequiv : Π(x : +3ℕ),
loop_spaces2 f x ≃* fibration_sequence_car x
| (n, fin.mk 0 H) := by reflexivity
| (n, fin.mk 1 H) := by reflexivity
| (n, fin.mk 2 H) := loopn_pequiv_loopn n e
| (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition fibration_sequence_fun_phomotopy : Π(x : +3ℕ),
fibration_sequence_pequiv x ∘* loop_spaces_fun2 f x ~*
(fibration_sequence_fun x ∘* fibration_sequence_pequiv (S x))
| (n, fin.mk 0 H) := by reflexivity
| (n, fin.mk 1 H) :=
begin refine !pid_comp ⬝* _, refine apn_phomotopy n p ⬝* _,
refine !apn_compose ⬝* _, reflexivity end
| (n, fin.mk 2 H) := begin refine !passoc⁻¹* ⬝* _ ⬝* !comp_pid⁻¹*, apply pwhisker_right,
refine _ ⬝* !apn_compose⁻¹*, reflexivity end
| (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition type_fibration_sequence [constructor] : type_chain_complex +3ℕ :=
transfer_type_chain_complex
(LES_of_loop_spaces2 f)
fibration_sequence_fun
fibration_sequence_pequiv
fibration_sequence_fun_phomotopy
definition is_exact_type_fibration_sequence : is_exact_t type_fibration_sequence :=
begin
intro n,
apply is_exact_at_t_transfer,
apply is_exact_LES_of_loop_spaces2
end
definition fibration_sequence [constructor] : chain_complex +3ℕ :=
trunc_chain_complex type_fibration_sequence
end
end chain_complex
namespace lift
definition pup [constructor] {A : Type*} : A →* plift A :=
pmap.mk up idp
definition pdown [constructor] {A : Type*} : plift A →* A :=
pmap.mk down idp
definition plift_functor_phomotopy [constructor] {A B : Type*} (f : A →* B)
: pdown ∘* plift_functor f ∘* pup ~* f :=
begin
fapply phomotopy.mk,
{ reflexivity},
{ esimp, refine !idp_con ⬝ _, refine _ ⬝ ap02 down !idp_con⁻¹,
refine _ ⬝ !ap_compose, exact !ap_id⁻¹}
end
definition equiv_lift [constructor] (A : Type) : A ≃ lift A :=
equiv.MK up down up_down down_up
definition pequiv_plift [constructor] (A : Type*) : A ≃* plift A :=
pequiv_of_equiv (equiv_lift A) idp
end lift open lift
namespace is_conn
local attribute comm_group.to_group [coercion]
local attribute is_equiv_tinverse [instance]
-- TODO: generalize this to arbitrary maps using lifts,
-- using that up : A → lift A and down : lift A → A are equivalences
theorem is_equiv_π_of_is_connected'.{u} {A B : pType.{u}} {n k : ℕ} (f : A →* B)
(H2 : k ≤ n) [H : is_conn_fun n f] : is_equiv (π→[k] f) :=
begin
cases k with k,
{ /- k = 0 -/
change (is_equiv (trunc_functor 0 f)), apply is_equiv_trunc_functor_of_is_conn_fun,
refine is_conn_fun_of_le f (zero_le_of_nat n)},
{ /- k > 0 -/
have H2' : k ≤ n, from le.trans !self_le_succ H2,
exact
@is_equiv_of_trivial _
(LES_of_homotopy_groups f) _
(is_exact_LES_of_homotopy_groups f (k, 2))
(is_exact_LES_of_homotopy_groups f (succ k, 0))
(@is_contr_HG_fiber_of_is_connected A B k n f H H2')
(@is_contr_HG_fiber_of_is_connected A B (succ k) n f H H2)
(@pgroup_of_group _ (group_LES_of_homotopy_groups f k 0) idp)
(@pgroup_of_group _ (group_LES_of_homotopy_groups f k 1) idp)
(homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun f (k, 0)))},
end
-- MOVE
-- Remark: ⁻¹ʰ conflicts with the inverse of a homomorphism
infix ` ⬝h `:75 := homotopy.trans
postfix `⁻¹ʰ`:(max+1) := homotopy.symm
-- MOVE
definition trunc_functor_homotopy [unfold 7] {X Y : Type} (n : ℕ₋₂) {f g : X → Y}
(p : f ~ g) (x : trunc n X) : trunc_functor n f x = trunc_functor n g x :=
begin
induction x with x, esimp, exact ap tr (p x)
end
-- MOVE
definition ptrunc_functor_phomotopy [constructor] {X Y : Type*} (n : ℕ₋₂) {f g : X →* Y}
(p : f ~* g) : ptrunc_functor n f ~* ptrunc_functor n g :=
begin
fapply phomotopy.mk,
{ exact trunc_functor_homotopy n p},
{ esimp, refine !ap_con⁻¹ ⬝ _, exact ap02 tr !to_homotopy_pt},
end
-- MOVE
definition phomotopy_group_functor_phomotopy [constructor] (n : ℕ) {A B : Type*} {f g : A →* B}
(p : f ~* g) : π→*[n] f ~* π→*[n] g :=
ptrunc_functor_phomotopy 0 (apn_phomotopy n p)
-- MOVE
definition phomotopy_group_functor_compose [constructor] (n : ℕ) {A B C : Type*} (g : B →* C)
(f : A →* B) : π→*[n] (g ∘* f) ~* π→*[n] g ∘* π→*[n] f :=
ptrunc_functor_phomotopy 0 !apn_compose ⬝* !ptrunc_functor_pcompose
-- MOVE
definition is_equiv_homotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
[is_equiv f] : is_equiv (π→[n] f) :=
@(is_equiv_trunc_functor 0 _) !is_equiv_apn
-- MOVE this to init.equiv, and incorporate it in `is_equiv_ap`
theorem eq_of_fn_eq_fn'_ap {A B : Type} (f : A → B) [is_equiv f] {x y : A} (q : x = y)
: eq_of_fn_eq_fn' f (ap f q) = q :=
by induction q; apply con.left_inv
-- MOVE
definition fiber_lift_functor {A B : Type} (f : A → B) (b : B) :
fiber (lift_functor f) (up b) ≃ fiber f b :=
begin
fapply equiv.MK: intro v; cases v with a p,
{ cases a with a, exact fiber.mk a (eq_of_fn_eq_fn' up p)},
{ exact fiber.mk (up a) (ap up p)},
{ esimp, apply ap (fiber.mk a), apply eq_of_fn_eq_fn'_ap},
{ cases a with a, esimp, apply ap (fiber.mk (up a)), apply ap_eq_of_fn_eq_fn'}
end
-- MOVE
definition is_conn_fun_lift_functor (n : ℕ₋₂) {A B : Type} (f : A → B) [is_conn_fun n f] :
is_conn_fun n (lift_functor f) :=
begin
intro b, cases b with b, apply is_trunc_equiv_closed_rev,
{ apply trunc_equiv_trunc, apply fiber_lift_functor}
end
theorem is_equiv_π_of_is_connected.{u v} {A : pType.{u}} {B : pType.{v}} {n k : ℕ} (f : A →* B)
(H2 : k ≤ n) [H : is_conn_fun n f] : is_equiv (π→[k] f) :=
begin
have π→*[k] pdown.{v u} ∘* π→*[k] (plift_functor f) ∘* π→*[k] pup.{u v} ~* π→*[k] f,
begin
refine pwhisker_left _ !phomotopy_group_functor_compose⁻¹* ⬝* _,
refine !phomotopy_group_functor_compose⁻¹* ⬝* _,
apply phomotopy_group_functor_phomotopy, apply plift_functor_phomotopy
end,
have π→[k] pdown.{v u} ∘ π→[k] (plift_functor f) ∘ π→[k] pup.{u v} ~ π→[k] f, from this,
apply is_equiv.homotopy_closed, rotate 1,
{ exact this},
{ do 2 apply is_equiv_compose,
{ apply is_equiv_homotopy_group_functor, apply to_is_equiv !equiv_lift},
{ refine @(is_equiv_π_of_is_connected' _ H2) _, apply is_conn_fun_lift_functor},
{ apply is_equiv_homotopy_group_functor, apply to_is_equiv !equiv_lift⁻¹ᵉ}}
end
theorem is_surjective_π_of_is_connected.{u} {A B : pType.{u}} (n : ℕ) (f : A →* B)
[H : is_conn_fun n f] : is_surjective (π→[n + 1] f) :=
@is_surjective_of_trivial _
(LES_of_homotopy_groups f) _
(is_exact_LES_of_homotopy_groups f (n, 2))
(@is_contr_HG_fiber_of_is_connected A B n n f H !le.refl)
-- TODO: move and rename?
definition natural_square2 {A B X : Type} {f : A → X} {g : B → X} (h : Πa b, f a = g b)
{a a' : A} {b b' : B} (p : a = a') (q : b = b')
: square (ap f p) (ap g q) (h a b) (h a' b') :=
by induction p; induction q; exact hrfl
end is_conn
namespace sigma
definition ppr1 [constructor] {A : Type*} {B : A → Type*} : (Σ*(x : A), B x) →* A :=
pmap.mk pr1 idp
definition ppr2 [unfold_full] {A : Type*} (B : A → Type*) (v : (Σ*(x : A), B x)) : B (ppr1 v) :=
pr2 v
end sigma
namespace hopf
open sphere.ops susp circle sphere_index
attribute hopf [unfold 4]
-- maybe define this as a composition of pointed maps?
definition complex_phopf [constructor] : S. 3 →* S. 2 :=
proof pmap.mk complex_hopf idp qed
definition fiber_pr1_fun {A : Type} {B : A → Type} {a : A} (b : B a)
: fiber_pr1 B a (fiber.mk ⟨a, b⟩ idp) = b :=
idp
--TODO: in fiber.equiv_precompose, make f explicit
open sphere sphere.ops
definition add_plus_one_of_nat (n m : ℕ) : (n +1+ m) = sphere_index.of_nat (n + m + 1) :=
begin
induction m with m IH,
{ reflexivity },
{ exact ap succ IH}
end
-- definition pjoin_pspheres (n m : ℕ) : join (S. n) (S. m) ≃ (S. (n + m + 1)) :=
-- join.spheres n m ⬝e begin esimp, apply equiv_of_eq, apply ap S, apply add_plus_one_of_nat end
definition part_of_complex_hopf : S (of_nat 3) → sigma (hopf S¹) :=
begin
intro x, apply inv (hopf.total S¹), apply inv (join.spheres 1 1), exact x
end
definition part_of_complex_hopf_base2
: (part_of_complex_hopf (@sphere.base 3)).2 = circle.base :=
begin
exact sorry
end
definition pfiber_complex_phopf : pfiber complex_phopf ≃* S. 1 :=
begin
fapply pequiv_of_equiv,
{ esimp, unfold [complex_hopf],
refine @fiber.equiv_precompose _ _ (sigma.pr1 ∘ (hopf.total S¹)⁻¹ᵉ) _ _
(join.spheres 1 1)⁻¹ᵉ _ ⬝e _,
refine fiber.equiv_precompose (hopf.total S¹)⁻¹ᵉ ⬝e _,
apply fiber_pr1},
{ esimp, refine _ ⬝ part_of_complex_hopf_base2, apply fiber_pr1_fun}
end
open int
definition one_le_succ (n : ℕ) : 1 ≤ succ n :=
nat.succ_le_succ !zero_le
definition π2S2 : πg[1+1] (S. 2) = gℤ :=
begin
refine _ ⬝ fundamental_group_of_circle,
refine _ ⬝ ap (λx, π₁ x) (eq_of_pequiv pfiber_complex_phopf),
fapply Group_eq,
{ fapply equiv.mk,
{ exact cc_to_fn (LES_of_homotopy_groups complex_phopf) (1, 2)},
{ refine @is_equiv_of_trivial _
_ _
(is_exact_LES_of_homotopy_groups _ (1, 1))
(is_exact_LES_of_homotopy_groups _ (1, 2))
_
_
(@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp)
(@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp)
_,
{ rewrite [LES_of_homotopy_groups_1, ▸*],
have H : 1 ≤[ℕ] 2, from !one_le_succ,
apply trivial_homotopy_group_of_is_conn, exact H, rexact is_conn_psphere 3},
{ refine tr_rev (λx, is_contr (ptrunctype._trans_of_to_pType x))
(LES_of_homotopy_groups_1 complex_phopf 2) _,
apply trivial_homotopy_group_of_is_conn, apply le.refl, rexact is_conn_psphere 3},
{ exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (0, 2))}}},
{ exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (0, 2))}
end
open circle
definition πnS3_eq_πnS2 (n : ℕ) : πg[n+2 +1] (S. 3) = πg[n+2 +1] (S. 2) :=
begin
fapply Group_eq,
{ fapply equiv.mk,
{ exact cc_to_fn (LES_of_homotopy_groups complex_phopf) (n+3, 0)},
{ have H : is_trunc 1 (pfiber complex_phopf),
from @(is_trunc_equiv_closed_rev _ pfiber_complex_phopf) is_trunc_circle,
refine @is_equiv_of_trivial _
_ _
(is_exact_LES_of_homotopy_groups _ (n+2, 2))
(is_exact_LES_of_homotopy_groups _ (n+3, 0))
_
_
(@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp)
(@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp)
_,
{ rewrite [▸*, LES_of_homotopy_groups_2 _ (n +[ℕ] 2)],
have H : 1 ≤[ℕ] n + 1, from !one_le_succ,
apply trivial_homotopy_group_of_is_trunc _ _ _ H},
{ refine tr_rev (λx, is_contr (ptrunctype._trans_of_to_pType x))
(LES_of_homotopy_groups_2 complex_phopf _) _,
have H : 1 ≤[ℕ] n + 2, from !one_le_succ,
apply trivial_homotopy_group_of_is_trunc _ _ _ H},
{ exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (n+2, 0))}}},
{ exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (n+2, 0))}
end
end hopf

807
homotopy/LES_of_homotopy_groups.hlean
View file

@ -1,807 +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
We define the fiber sequence of a pointed map f : X →* Y. We mostly follow the proof in section 8.4
of the book.
PART 1:
We define a sequence fiber_sequence as in Definition 8.4.3.
It has types X(n) : Type*
X(0) := Y,
X(1) := X,
X(n+1) := fiber (f(n))
with functions f(n) : X(n+1) →* X(n)
f(0) := f
f(n+1) := point (f(n)) [this is the first projection]
We prove that this is an exact sequence.
Then we prove Lemma 8.4.3, by showing that X(n+3) ≃* Ω(X(n)) and that this equivalence sends
the pointed map f(n+3) to -Ω(f(n)), i.e. the composition of Ω(f(n)) with path inversion.
Using this equivalence we get a boundary_map : Ω(Y) → pfiber f.
PART 2:
Now we can define a new fiber sequence X'(n) : Type*, and here we slightly diverge from the book.
We define it as
X'(0) := Y,
X'(1) := X,
X'(2) := fiber f
X'(n+3) := Ω(X'(n))
with maps f'(n) : X'(n+1) →* X'(n)
f'(0) := f
f'(1) := point f
f'(2) := boundary_map
f'(n+3) := Ω(f'(n))
This sequence is not equivalent to the previous sequence. The difference is in the signs.
The sequence f has negative signs (i.e. is composed with the inverse maps) for n ≡ 3, 4, 5 mod 6.
This sign information is captured by e : X'(n) ≃* X'(n) such that
e(k) := 1 for k = 0,1,2,3
e(k+3) := Ω(e(k)) ∘ (-)⁻¹ for k > 0
Now the sequence (X', f' ∘ e) is equivalent to (X, f), Hence (X', f' ∘ e) is an exact sequence.
We then prove that (X', f') is an exact sequence by using that there are other equivalences
eₗ and eᵣ such that
f' = eᵣ ∘ f' ∘ e
f' ∘ eₗ = e ∘ f'.
(this fact is type_chain_complex_cancel_aut and is_exact_at_t_cancel_aut in the file chain_complex)
eₗ and eᵣ are almost the same as e, except that the places where the inverse is taken is
slightly shifted:
eᵣ = (-)⁻¹ for n ≡ 3, 4, 5 mod 6 and eᵣ = 1 otherwise
e = (-)⁻¹ for n ≡ 4, 5, 6 mod 6 (except for n = 0) and e = 1 otherwise
eₗ = (-)⁻¹ for n ≡ 5, 6, 7 mod 6 (except for n = 0, 1) and eₗ = 1 otherwise
PART 3:
We change the type over which the sequence of types and maps are indexed from ℕ to ℕ × 3
(where 3 is the finite type with 3 elements). The reason is that we have that X'(3n) = Ωⁿ(Y), but
this equality is not definitionally true. Hence we cannot even state whether f'(3n) = Ωⁿ(f) without
using transports. This gets ugly. However, if we use as index type ℕ × 3, we can do this. We can
define
Y : ℕ × 3 → Type* as
Y(n, 0) := Ωⁿ(Y)
Y(n, 1) := Ωⁿ(X)
Y(n, 2) := Ωⁿ(fiber f)
with maps g(n) : Y(S n) →* Y(n) (where the successor is defined in the obvious way)
g(n, 0) := Ωⁿ(f)
g(n, 1) := Ωⁿ(point f)
g(n, 2) := Ωⁿ(boundary_map) ∘ cast
Here "cast" is the transport over the equality Ωⁿ⁺¹(Y) = Ωⁿ(Ω(Y)). We show that the sequence
(ℕ, X', f') is equivalent to (ℕ × 3, Y, g).
PART 4:
We get the long exact sequence of homotopy groups by taking the set-truncation of (Y, g).
-/
import .chain_complex algebra.homotopy_group
open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc algebra function sum
section MOVE
-- TODO: MOVE
open group chain_complex
definition pinverse_pinverse (A : Type*) : pinverse ∘* pinverse ~* pid (Ω A) :=
begin
fapply phomotopy.mk,
{ apply inv_inv},
{ reflexivity}
end
definition to_pmap_pequiv_of_pmap {A B : Type*} (f : A →* B) (H : is_equiv f)
: pequiv.to_pmap (pequiv_of_pmap f H) = f :=
by cases f; reflexivity
definition to_pmap_pequiv_trans {A B C : Type*} (f : A ≃* B) (g : B ≃* C)
: pequiv.to_pmap (f ⬝e* g) = g ∘* f :=
!to_pmap_pequiv_of_pmap
definition pequiv_pinverse (A : Type*) : Ω A ≃* Ω A :=
pequiv_of_pmap pinverse !is_equiv_eq_inverse
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
end MOVE
/--------------
PART 1
--------------/
namespace chain_complex
definition fiber_sequence_helper [constructor] (v : Σ(X Y : Type*), X →* Y)
: Σ(Z X : Type*), Z →* X :=
⟨pfiber v.2.2, v.1, ppoint v.2.2⟩
definition fiber_sequence_helpern (v : Σ(X Y : Type*), X →* Y) (n : ℕ)
: Σ(Z X : Type*), Z →* X :=
iterate fiber_sequence_helper n v
section
universe variable u
parameters {X Y : pType.{u}} (f : X →* Y)
include f
definition fiber_sequence_carrier (n : ℕ) : Type* :=
(fiber_sequence_helpern ⟨X, Y, f⟩ n).2.1
definition fiber_sequence_fun (n : ℕ)
: fiber_sequence_carrier (n + 1) →* fiber_sequence_carrier n :=
(fiber_sequence_helpern ⟨X, Y, f⟩ n).2.2
/- Definition 8.4.3 -/
definition fiber_sequence : type_chain_complex.{0 u} +ℕ :=
begin
fconstructor,
{ exact fiber_sequence_carrier},
{ exact fiber_sequence_fun},
{ intro n x, cases n with n,
{ exact point_eq x},
{ exact point_eq x}}
end
definition is_exact_fiber_sequence : is_exact_t fiber_sequence :=
λn x p, fiber.mk (fiber.mk x p) rfl
/- (generalization of) Lemma 8.4.4(i)(ii) -/
definition fiber_sequence_carrier_equiv (n : ℕ)
: fiber_sequence_carrier (n+3) ≃ Ω(fiber_sequence_carrier n) :=
calc
fiber_sequence_carrier (n+3) ≃ fiber (fiber_sequence_fun (n+1)) pt : erfl
... ≃ Σ(x : fiber_sequence_carrier _), fiber_sequence_fun (n+1) x = pt
: fiber.sigma_char
... ≃ Σ(x : fiber (fiber_sequence_fun n) pt), fiber_sequence_fun _ x = pt
: erfl
... ≃ Σ(v : Σ(x : fiber_sequence_carrier _), fiber_sequence_fun _ x = pt),
fiber_sequence_fun _ (fiber.mk v.1 v.2) = pt
: by exact sigma_equiv_sigma !fiber.sigma_char (λa, erfl)
... ≃ Σ(v : Σ(x : fiber_sequence_carrier _), fiber_sequence_fun _ x = pt),
v.1 = pt
: erfl
... ≃ Σ(v : Σ(x : fiber_sequence_carrier _), x = pt),
fiber_sequence_fun _ v.1 = pt
: sigma_assoc_comm_equiv
... ≃ fiber_sequence_fun _ !center.1 = pt
: @(sigma_equiv_of_is_contr_left _) !is_contr_sigma_eq'
... ≃ fiber_sequence_fun _ pt = pt
: erfl
... ≃ pt = pt
: by exact !equiv_eq_closed_left !respect_pt
... ≃ Ω(fiber_sequence_carrier n) : erfl
/- computation rule -/
definition fiber_sequence_carrier_equiv_eq (n : ℕ)
(x : fiber_sequence_carrier (n+1)) (p : fiber_sequence_fun n x = pt)
(q : fiber_sequence_fun (n+1) (fiber.mk x p) = pt)
: fiber_sequence_carrier_equiv n (fiber.mk (fiber.mk x p) q)
= !respect_pt⁻¹ ⬝ ap (fiber_sequence_fun n) q⁻¹ ⬝ p :=
begin
refine _ ⬝ !con.assoc⁻¹,
apply whisker_left,
refine transport_eq_Fl _ _ ⬝ _,
apply whisker_right,
refine inverse2 !ap_inv ⬝ !inv_inv ⬝ _,
refine ap_compose (fiber_sequence_fun n) pr₁ _ ⬝
ap02 (fiber_sequence_fun n) !ap_pr1_center_eq_sigma_eq',
end
definition fiber_sequence_carrier_equiv_inv_eq (n : ℕ)
(p : Ω(fiber_sequence_carrier n)) : (fiber_sequence_carrier_equiv n)⁻¹ᵉ p =
fiber.mk (fiber.mk pt (respect_pt (fiber_sequence_fun n) ⬝ p)) idp :=
begin
apply inv_eq_of_eq,
refine _ ⬝ !fiber_sequence_carrier_equiv_eq⁻¹, esimp,
exact !inv_con_cancel_left⁻¹
end
definition fiber_sequence_carrier_pequiv (n : ℕ)
: fiber_sequence_carrier (n+3) ≃* Ω(fiber_sequence_carrier n) :=
pequiv_of_equiv (fiber_sequence_carrier_equiv n)
begin
esimp,
apply con.left_inv
end
definition fiber_sequence_carrier_pequiv_eq (n : ℕ)
(x : fiber_sequence_carrier (n+1)) (p : fiber_sequence_fun n x = pt)
(q : fiber_sequence_fun (n+1) (fiber.mk x p) = pt)
: fiber_sequence_carrier_pequiv n (fiber.mk (fiber.mk x p) q)
= !respect_pt⁻¹ ⬝ ap (fiber_sequence_fun n) q⁻¹ ⬝ p :=
fiber_sequence_carrier_equiv_eq n x p q
definition fiber_sequence_carrier_pequiv_inv_eq (n : ℕ)
(p : Ω(fiber_sequence_carrier n)) : (fiber_sequence_carrier_pequiv n)⁻¹ᵉ* p =
fiber.mk (fiber.mk pt (respect_pt (fiber_sequence_fun n) ⬝ p)) idp :=
by rexact fiber_sequence_carrier_equiv_inv_eq n p
/- Lemma 8.4.4(iii) -/
definition fiber_sequence_fun_eq_helper (n : ℕ)
(p : Ω(fiber_sequence_carrier (n + 1))) :
fiber_sequence_carrier_pequiv n
(fiber_sequence_fun (n + 3)
((fiber_sequence_carrier_pequiv (n + 1))⁻¹ᵉ* p)) =
ap1 (fiber_sequence_fun n) p⁻¹ :=
begin
refine ap (λx, fiber_sequence_carrier_pequiv n (fiber_sequence_fun (n + 3) x))
(fiber_sequence_carrier_pequiv_inv_eq (n+1) p) ⬝ _,
/- the following three lines are rewriting some reflexivities: -/
-- replace (n + 3) with (n + 2 + 1),
-- refine ap (fiber_sequence_carrier_pequiv n)
-- (fiber_sequence_fun_eq1 (n+2) _ idp) ⬝ _,
refine fiber_sequence_carrier_pequiv_eq n pt (respect_pt (fiber_sequence_fun n)) _ ⬝ _,
esimp,
apply whisker_right,
apply whisker_left,
apply ap02, apply inverse2, apply idp_con,
end
theorem fiber_sequence_carrier_pequiv_eq_point_eq_idp (n : ℕ) :
fiber_sequence_carrier_pequiv_eq n
(Point (fiber_sequence_carrier (n+1)))
(respect_pt (fiber_sequence_fun n))
(respect_pt (fiber_sequence_fun (n + 1))) = idp :=
begin
apply con_inv_eq_idp,
refine ap (λx, whisker_left _ (_ ⬝ x)) _ ⬝ _,
{ reflexivity},
{ reflexivity},
refine ap (whisker_left _)
(transport_eq_Fl_idp_left (fiber_sequence_fun n)
(respect_pt (fiber_sequence_fun n))) ⬝ _,
apply whisker_left_idp_con_eq_assoc
end
theorem fiber_sequence_fun_phomotopy_helper (n : ℕ) :
(fiber_sequence_carrier_pequiv n ∘*
fiber_sequence_fun (n + 3)) ∘*
(fiber_sequence_carrier_pequiv (n + 1))⁻¹ᵉ* ~*
ap1 (fiber_sequence_fun n) ∘* pinverse :=
begin
fapply phomotopy.mk,
{ exact chain_complex.fiber_sequence_fun_eq_helper f n},
{ esimp, rewrite [idp_con], refine _ ⬝ whisker_left _ !idp_con⁻¹,
apply whisker_right,
apply whisker_left,
exact chain_complex.fiber_sequence_carrier_pequiv_eq_point_eq_idp f n}
end
theorem fiber_sequence_fun_eq (n : ℕ) : Π(x : fiber_sequence_carrier (n + 4)),
fiber_sequence_carrier_pequiv n (fiber_sequence_fun (n + 3) x) =
ap1 (fiber_sequence_fun n) (fiber_sequence_carrier_pequiv (n + 1) x)⁻¹ :=
begin
apply homotopy_of_inv_homotopy_pre (fiber_sequence_carrier_pequiv (n + 1)),
apply fiber_sequence_fun_eq_helper n
end
theorem fiber_sequence_fun_phomotopy (n : ℕ) :
fiber_sequence_carrier_pequiv n ∘*
fiber_sequence_fun (n + 3) ~*
(ap1 (fiber_sequence_fun n) ∘* pinverse) ∘* fiber_sequence_carrier_pequiv (n + 1) :=
begin
apply phomotopy_of_pinv_right_phomotopy,
apply fiber_sequence_fun_phomotopy_helper
end
definition boundary_map : Ω Y →* pfiber f :=
fiber_sequence_fun 2 ∘* (fiber_sequence_carrier_pequiv 0)⁻¹ᵉ*
/--------------
PART 2
--------------/
/- Now we are ready to define the long exact sequence of homotopy groups.
First we define its carrier -/
definition loop_spaces : ℕ → Type*
| 0 := Y
| 1 := X
| 2 := pfiber f
| (k+3) := Ω (loop_spaces k)
/- The maps between the homotopy groups -/
definition loop_spaces_fun
: Π(n : ℕ), loop_spaces (n+1) →* loop_spaces n
| 0 := proof f qed
| 1 := proof ppoint f qed
| 2 := proof boundary_map qed
| (k+3) := proof ap1 (loop_spaces_fun k) qed
definition loop_spaces_fun_add3 [unfold_full] (n : ℕ) :
loop_spaces_fun (n + 3) = ap1 (loop_spaces_fun n) :=
proof idp qed
definition fiber_sequence_pequiv_loop_spaces :
Πn, fiber_sequence_carrier n ≃* loop_spaces n
| 0 := by reflexivity
| 1 := by reflexivity
| 2 := by reflexivity
| (k+3) :=
begin
refine fiber_sequence_carrier_pequiv k ⬝e* _,
apply loop_pequiv_loop,
exact fiber_sequence_pequiv_loop_spaces k
end
definition fiber_sequence_pequiv_loop_spaces_add3 (n : ℕ)
: fiber_sequence_pequiv_loop_spaces (n + 3) =
ap1 (fiber_sequence_pequiv_loop_spaces n) ∘* fiber_sequence_carrier_pequiv n :=
by reflexivity
definition fiber_sequence_pequiv_loop_spaces_3_phomotopy
: fiber_sequence_pequiv_loop_spaces 3 ~* proof fiber_sequence_carrier_pequiv nat.zero qed :=
begin
refine pwhisker_right _ ap1_id ⬝* _,
apply pid_comp
end
definition pid_or_pinverse : Π(n : ℕ), loop_spaces n ≃* loop_spaces n
| 0 := pequiv.rfl
| 1 := pequiv.rfl
| 2 := pequiv.rfl
| 3 := pequiv.rfl
| (k+4) := !pequiv_pinverse ⬝e* loop_pequiv_loop (pid_or_pinverse (k+1))
definition pid_or_pinverse_add4 (n : ℕ)
: pid_or_pinverse (n + 4) = !pequiv_pinverse ⬝e* loop_pequiv_loop (pid_or_pinverse (n + 1)) :=
by reflexivity
definition pid_or_pinverse_add4_rev : Π(n : ℕ),
pid_or_pinverse (n + 4) ~* pinverse ∘* Ω→(pid_or_pinverse (n + 1))
| 0 := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans],
replace pid_or_pinverse (0 + 1) with pequiv.refl X,
rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _,
exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end
| 1 := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans],
replace pid_or_pinverse (1 + 1) with pequiv.refl (pfiber f),
rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _,
exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end
| 2 := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans],
replace pid_or_pinverse (2 + 1) with pequiv.refl (Ω Y),
rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _,
exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end
| (k+3) :=
begin
replace (k + 3 + 1) with (k + 4),
rewrite [+ pid_or_pinverse_add4, + to_pmap_pequiv_trans],
refine _ ⬝* pwhisker_left _ !ap1_compose⁻¹*,
refine _ ⬝* !passoc,
apply pconcat2,
{ refine ap1_phomotopy (pid_or_pinverse_add4_rev k) ⬝* _,
refine !ap1_compose ⬝* _, apply pwhisker_right, apply ap1_pinverse},
{ refine !ap1_pinverse⁻¹*}
end
theorem fiber_sequence_phomotopy_loop_spaces : Π(n : ℕ),
fiber_sequence_pequiv_loop_spaces n ∘* fiber_sequence_fun n ~*
(loop_spaces_fun n ∘* pid_or_pinverse (n + 1)) ∘* fiber_sequence_pequiv_loop_spaces (n + 1)
| 0 := proof proof phomotopy.rfl qed ⬝* pwhisker_right _ !comp_pid⁻¹* qed
| 1 := by reflexivity
| 2 :=
begin
refine !pid_comp ⬝* _,
replace loop_spaces_fun 2 with boundary_map,
refine _ ⬝* pwhisker_left _ fiber_sequence_pequiv_loop_spaces_3_phomotopy⁻¹*,
apply phomotopy_of_pinv_right_phomotopy,
exact !pid_comp⁻¹*
end
| (k+3) :=
begin
replace (k + 3 + 1) with (k + 1 + 3),
rewrite [fiber_sequence_pequiv_loop_spaces_add3 k,
fiber_sequence_pequiv_loop_spaces_add3 (k+1)],
refine !passoc ⬝* _,
refine pwhisker_left _ (fiber_sequence_fun_phomotopy k) ⬝* _,
refine !passoc⁻¹* ⬝* _ ⬝* !passoc,
apply pwhisker_right,
replace (k + 1 + 3) with (k + 4),
xrewrite [loop_spaces_fun_add3, pid_or_pinverse_add4, to_pmap_pequiv_trans],
refine _ ⬝* !passoc⁻¹*,
refine _ ⬝* pwhisker_left _ !passoc⁻¹*,
refine _ ⬝* pwhisker_left _ (pwhisker_left _ !ap1_compose_pinverse),
refine !passoc⁻¹* ⬝* _ ⬝* !passoc ⬝* !passoc,
apply pwhisker_right,
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose ⬝* pwhisker_right _ !ap1_compose,
apply ap1_phomotopy,
exact fiber_sequence_phomotopy_loop_spaces k
end
definition pid_or_pinverse_right : Π(n : ℕ), loop_spaces n →* loop_spaces n
| 0 := !pid
| 1 := !pid
| 2 := !pid
| (k+3) := Ω→(pid_or_pinverse_right k) ∘* pinverse
definition pid_or_pinverse_left : Π(n : ℕ), loop_spaces n →* loop_spaces n
| 0 := pequiv.rfl
| 1 := pequiv.rfl
| 2 := pequiv.rfl
| 3 := pequiv.rfl
| 4 := pequiv.rfl
| (k+5) := Ω→(pid_or_pinverse_left (k+2)) ∘* pinverse
definition pid_or_pinverse_right_add3 (n : ℕ)
: pid_or_pinverse_right (n + 3) = Ω→(pid_or_pinverse_right n) ∘* pinverse :=
by reflexivity
definition pid_or_pinverse_left_add5 (n : ℕ)
: pid_or_pinverse_left (n + 5) = Ω→(pid_or_pinverse_left (n+2)) ∘* pinverse :=
by reflexivity
theorem pid_or_pinverse_commute_right : Π(n : ℕ),
loop_spaces_fun n ~* pid_or_pinverse_right n ∘* loop_spaces_fun n ∘* pid_or_pinverse (n + 1)
| 0 := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed
| 1 := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed
| 2 := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed
| (k+3) :=
begin
replace (k + 3 + 1) with (k + 4),
rewrite [pid_or_pinverse_right_add3, loop_spaces_fun_add3],
refine _ ⬝* pwhisker_left _ (pwhisker_left _ !pid_or_pinverse_add4_rev⁻¹*),
refine ap1_phomotopy (pid_or_pinverse_commute_right k) ⬝* _,
refine !ap1_compose ⬝* _ ⬝* !passoc⁻¹*,
apply pwhisker_left,
refine !ap1_compose ⬝* _ ⬝* !passoc ⬝* !passoc,
apply pwhisker_right,
refine _ ⬝* pwhisker_right _ !ap1_compose_pinverse,
refine _ ⬝* !passoc⁻¹*,
refine !comp_pid⁻¹* ⬝* pwhisker_left _ _,
symmetry, apply pinverse_pinverse
end
theorem pid_or_pinverse_commute_left : Π(n : ℕ),
loop_spaces_fun n ∘* pid_or_pinverse_left (n + 1) ~* pid_or_pinverse n ∘* loop_spaces_fun n
| 0 := proof !comp_pid ⬝* !pid_comp⁻¹* qed
| 1 := proof !comp_pid ⬝* !pid_comp⁻¹* qed
| 2 := proof !comp_pid ⬝* !pid_comp⁻¹* qed
| 3 := proof !comp_pid ⬝* !pid_comp⁻¹* qed
| (k+4) :=
begin
replace (k + 4 + 1) with (k + 5),
rewrite [pid_or_pinverse_left_add5, pid_or_pinverse_add4, to_pmap_pequiv_trans],
replace (k + 4) with (k + 1 + 3),
rewrite [loop_spaces_fun_add3],
refine !passoc⁻¹* ⬝* _ ⬝* !passoc⁻¹*,
refine _ ⬝* pwhisker_left _ !ap1_compose_pinverse,
refine _ ⬝* !passoc,
apply pwhisker_right,
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose,
exact ap1_phomotopy (pid_or_pinverse_commute_left (k+1))
end
definition LES_of_loop_spaces' [constructor] : type_chain_complex +ℕ :=
transfer_type_chain_complex
fiber_sequence
(λn, loop_spaces_fun n ∘* pid_or_pinverse (n + 1))
fiber_sequence_pequiv_loop_spaces
fiber_sequence_phomotopy_loop_spaces
definition LES_of_loop_spaces [constructor] : type_chain_complex +ℕ :=
type_chain_complex_cancel_aut
LES_of_loop_spaces'
loop_spaces_fun
pid_or_pinverse
pid_or_pinverse_right
(λn x, idp)
pid_or_pinverse_commute_right
definition is_exact_LES_of_loop_spaces : is_exact_t LES_of_loop_spaces :=
begin
intro n,
refine is_exact_at_t_cancel_aut n pid_or_pinverse_left _ _ pid_or_pinverse_commute_left _,
apply is_exact_at_t_transfer,
apply is_exact_fiber_sequence
end
open prod succ_str fin
/--------------
PART 3
--------------/
definition loop_spaces2 [reducible] : +3ℕ → Type*
| (n, fin.mk 0 H) := Ω[n] Y
| (n, fin.mk 1 H) := Ω[n] X
| (n, fin.mk k H) := Ω[n] (pfiber f)
definition loop_spaces2_add1 (n : ℕ) : Π(x : fin 3),
loop_spaces2 (n+1, x) = Ω (loop_spaces2 (n, x))
| (fin.mk 0 H) := by reflexivity
| (fin.mk 1 H) := by reflexivity
| (fin.mk 2 H) := by reflexivity
| (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition loop_spaces_fun2 : Π(n : +3ℕ), loop_spaces2 (S n) →* loop_spaces2 n
| (n, fin.mk 0 H) := proof Ω→[n] f qed
| (n, fin.mk 1 H) := proof Ω→[n] (ppoint f) qed
| (n, fin.mk 2 H) := proof Ω→[n] boundary_map ∘* pcast (loop_space_succ_eq_in Y n) qed
| (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition loop_spaces_fun2_add1_0 (n : ℕ) (H : 0 < succ 2)
: loop_spaces_fun2 (n+1, fin.mk 0 H) ~*
cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 0 H)) :=
by reflexivity
definition loop_spaces_fun2_add1_1 (n : ℕ) (H : 1 < succ 2)
: loop_spaces_fun2 (n+1, fin.mk 1 H) ~*
cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 1 H)) :=
by reflexivity
definition loop_spaces_fun2_add1_2 (n : ℕ) (H : 2 < succ 2)
: loop_spaces_fun2 (n+1, fin.mk 2 H) ~*
cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 2 H)) :=
begin
esimp,
refine _ ⬝* !ap1_compose⁻¹*,
apply pwhisker_left,
apply 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_3S [unfold 2] [reducible]
: Π(x : stratified +ℕ 2), nat_of_str x + 1 = nat_of_str (@S (stratified +ℕ 2) 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 (k+3) 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 3 times the same,
so maybe this can be simplified
-/
definition loop_spaces2_pequiv' : Π(n : ℕ) (x : fin (nat.succ 2)),
loop_spaces (nat_of_str (n, x)) ≃* loop_spaces2 (n, x)
| 0 (fin.mk 0 H) := by reflexivity
| 0 (fin.mk 1 H) := by reflexivity
| 0 (fin.mk 2 H) := by reflexivity
| (n+1) (fin.mk 0 H) :=
begin
apply loop_pequiv_loop,
rexact loop_spaces2_pequiv' n (fin.mk 0 H)
end
| (n+1) (fin.mk 1 H) :=
begin
apply loop_pequiv_loop,
rexact loop_spaces2_pequiv' n (fin.mk 1 H)
end
| (n+1) (fin.mk 2 H) :=
begin
apply loop_pequiv_loop,
rexact loop_spaces2_pequiv' n (fin.mk 2 H)
end
| n (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition loop_spaces2_pequiv : Π(x : +3ℕ),
loop_spaces (nat_of_str x) ≃* loop_spaces2 x
| (n, x) := loop_spaces2_pequiv' n x
local attribute loop_pequiv_loop [reducible]
/- all cases where n>0 are basically the same -/
definition loop_spaces_fun2_phomotopy (x : +3ℕ) :
loop_spaces2_pequiv x ∘* loop_spaces_fun (nat_of_str x) ~*
(loop_spaces_fun2 x ∘* loop_spaces2_pequiv (S x))
∘* pcast (ap (loop_spaces) (nat_of_str_3S x)) :=
begin
cases x with n x, cases x with k H,
do 3 (cases k with k; rotate 1),
{ /-k≥3-/ exfalso, apply lt_le_antisymm H, apply le_add_left},
{ /-k=0-/
induction n with n IH,
{ refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
reflexivity},
{ refine _ ⬝* !comp_pid⁻¹*,
refine _ ⬝* pwhisker_right _ !loop_spaces_fun2_add1_0⁻¹*,
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 _ !loop_spaces_fun2_add1_1⁻¹*,
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
exact IH ⬝* !comp_pid}},
{ /-k=2-/
induction n with n IH,
{ refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
refine !comp_pid⁻¹* ⬝* pconcat2 _ _,
{ exact (comp_pid (chain_complex.boundary_map f))⁻¹*},
{ refine cast (ap (λx, _ ~* x) !loop_pequiv_loop_rfl)⁻¹ _, reflexivity}},
{ refine _ ⬝* !comp_pid⁻¹*,
refine _ ⬝* pwhisker_right _ !loop_spaces_fun2_add1_2⁻¹*,
refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
exact IH ⬝* !comp_pid}},
end
definition LES_of_loop_spaces2 [constructor] : type_chain_complex +3ℕ :=
transfer_type_chain_complex2
LES_of_loop_spaces
!fin_prod_nat_equiv_nat
nat_of_str_3S
@loop_spaces_fun2
@loop_spaces2_pequiv
begin
intro m x,
refine loop_spaces_fun2_phomotopy m x ⬝ _,
apply ap (loop_spaces_fun2 m), apply ap (loop_spaces2_pequiv (S m)),
esimp, exact ap010 cast !ap_compose⁻¹ x
end
definition is_exact_LES_of_loop_spaces2 : is_exact_t LES_of_loop_spaces2 :=
begin
intro n,
apply is_exact_at_t_transfer2,
apply is_exact_LES_of_loop_spaces
end
definition LES_of_homotopy_groups' [constructor] : chain_complex +3ℕ :=
trunc_chain_complex LES_of_loop_spaces2
/--------------
PART 4
--------------/
definition homotopy_groups [reducible] : +3ℕ → Set*
| (n, fin.mk 0 H) := π*[n] Y
| (n, fin.mk 1 H) := π*[n] X
| (n, fin.mk k H) := π*[n] (pfiber f)
definition homotopy_groups_pequiv_loop_spaces2 [reducible]
: Π(n : +3ℕ), ptrunc 0 (loop_spaces2 n) ≃* homotopy_groups 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 (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition homotopy_groups_fun : Π(n : +3ℕ), homotopy_groups (S n) →* homotopy_groups n
| (n, fin.mk 0 H) := proof π→*[n] f qed
| (n, fin.mk 1 H) := proof π→*[n] (ppoint f) qed
| (n, fin.mk 2 H) :=
proof π→*[n] boundary_map ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y n)) qed
| (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition homotopy_groups_fun_phomotopy_loop_spaces_fun2 [reducible]
: Π(n : +3ℕ), homotopy_groups_pequiv_loop_spaces2 n ∘* ptrunc_functor 0 (loop_spaces_fun2 n) ~*
homotopy_groups_fun n ∘* homotopy_groups_pequiv_loop_spaces2 (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 (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition LES_of_homotopy_groups [constructor] : chain_complex +3ℕ :=
transfer_chain_complex
LES_of_homotopy_groups'
homotopy_groups_fun
homotopy_groups_pequiv_loop_spaces2
homotopy_groups_fun_phomotopy_loop_spaces_fun2
definition is_exact_LES_of_homotopy_groups : is_exact LES_of_homotopy_groups :=
begin
intro n,
apply is_exact_at_transfer,
apply is_exact_at_trunc,
apply is_exact_LES_of_loop_spaces2
end
variable (n : ℕ)
/- the carrier of the fiber sequence is definitionally what we want (as pointed sets) -/
example : LES_of_homotopy_groups (str_of_nat 6) = π*[2] Y :> Set* := by reflexivity
example : LES_of_homotopy_groups (str_of_nat 7) = π*[2] X :> Set* := by reflexivity
example : LES_of_homotopy_groups (str_of_nat 8) = π*[2] (pfiber f) :> Set* := by reflexivity
example : LES_of_homotopy_groups (str_of_nat 9) = π*[3] Y :> Set* := by reflexivity
example : LES_of_homotopy_groups (str_of_nat 10) = π*[3] X :> Set* := by reflexivity
example : LES_of_homotopy_groups (str_of_nat 11) = π*[3] (pfiber f) :> Set* := by reflexivity
definition LES_of_homotopy_groups_0 : LES_of_homotopy_groups (n, 0) = π*[n] Y :=
by reflexivity
definition LES_of_homotopy_groups_1 : LES_of_homotopy_groups (n, 1) = π*[n] X :=
by reflexivity
definition LES_of_homotopy_groups_2 : LES_of_homotopy_groups (n, 2) = π*[n] (pfiber f) :=
by reflexivity
/-
the functions of the fiber sequence is definitionally what we want (as pointed function).
-/
definition LES_of_homotopy_groups_fun_0 :
cc_to_fn LES_of_homotopy_groups (n, 0) = π→*[n] f :=
by reflexivity
definition LES_of_homotopy_groups_fun_1 :
cc_to_fn LES_of_homotopy_groups (n, 1) = π→*[n] (ppoint f) :=
by reflexivity
definition LES_of_homotopy_groups_fun_2 : cc_to_fn LES_of_homotopy_groups (n, 2) =
π→*[n] boundary_map ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y n)) :=
by reflexivity
open group
definition group_LES_of_homotopy_groups (n : ℕ) : Π(x : fin (succ 2)),
group (LES_of_homotopy_groups (n + 1, x))
| (fin.mk 0 H) := begin rexact group_homotopy_group n Y end
| (fin.mk 1 H) := begin rexact group_homotopy_group n X end
| (fin.mk 2 H) := begin rexact group_homotopy_group n (pfiber f) end
| (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition comm_group_LES_of_homotopy_groups (n : ℕ) : Π(x : fin (succ 2)),
comm_group (LES_of_homotopy_groups (n + 2, x))
| (fin.mk 0 H) := proof comm_group_homotopy_group n Y qed
| (fin.mk 1 H) := proof comm_group_homotopy_group n X qed
| (fin.mk 2 H) := proof comm_group_homotopy_group n (pfiber f) qed
| (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition Group_LES_of_homotopy_groups (x : +3ℕ) : Group.{u} :=
Group.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x))
(group_LES_of_homotopy_groups (pr1 x) (pr2 x))
definition CommGroup_LES_of_homotopy_groups (n : +3ℕ) : CommGroup.{u} :=
CommGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n))
(comm_group_LES_of_homotopy_groups (pr1 n) (pr2 n))
definition homomorphism_LES_of_homotopy_groups_fun : Π(k : +3ℕ),
Group_LES_of_homotopy_groups (S k) →g Group_LES_of_homotopy_groups k
| (k, fin.mk 0 H) :=
proof homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 0))
(phomotopy_group_functor_mul _ _) qed
| (k, fin.mk 1 H) :=
proof homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 1))
(phomotopy_group_functor_mul _ _) qed
| (k, fin.mk 2 H) :=
begin
apply homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 2)),
exact abstract begin rewrite [LES_of_homotopy_groups_fun_2],
refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[k + 1] boundary_map) _ _ _,
{ apply group_homotopy_group k},
{ apply phomotopy_group_functor_mul},
{ rewrite [▸*, -ap_compose', ▸*],
apply is_homomorphism_cast_loop_space_succ_eq_in} end end
end
| (k, fin.mk (l+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
end
end chain_complex

6
homotopy/LES_of_homotopy_groups_old.hlean
View file

@ -7,12 +7,12 @@ The old formalization of the LES of homotopy groups, where all the odd levels ha
with negation
-/
import .LES_of_homotopy_groups
import homotopy.LES_of_homotopy_groups
open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc algebra function
/--------------
PART 1
PART 1 is the same as the new formalization
--------------/
namespace chain_complex
@ -721,7 +721,7 @@ namespace chain_complex namespace old
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) _ _ _,
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', ▸*],

561
homotopy/chain_complex.hlean
View file

@ -1,561 +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
-/
import types.int types.pointed types.trunc algebra.hott ..group_theory.basic .fin
open eq pointed int unit is_equiv equiv is_trunc trunc 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⁻¹ :=
by induction q; reflexivity
definition whisker_left_idp_con_eq_assoc
{A : Type} {a₁ a₂ a₃ : A} (p : a₁ = a₂) (q : a₂ = a₃)
: whisker_left p (idp_con q)⁻¹ = con.assoc p idp q :=
by induction q; reflexivity
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 : ℕ} (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
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
namespace chain_complex
-- are chain complexes with the "set"-requirement removed interesting?
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)
section
variables {N : succ_str} (X : type_chain_complex N) (n : N)
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 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 :=
Π(n : N), is_exact_at_t X n
-- 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 : 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_type_chain_complex [constructor] /- X -/
{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 (tcc_is_chain_complex X n _) ⬝ _,
apply respect_pt
end end
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 *,
have H2 : tcc_to_fn X n (e⁻¹ᵉ* y) = pt,
begin
refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
refine ap _ q ⬝ _,
exact respect_pt e⁻¹ᵉ*
end,
cases (H _ H2) with x r,
refine fiber.mk (e x) _,
refine (p x)⁻¹ ⬝ _,
refine ap e r ⬝ _,
apply right_inv
end
-- cancel automorphisms inside a long exact sequence
definition type_chain_complex_cancel_aut [constructor] /- X -/
(g : Π{n : N}, X (S n) →* X n) (e : Π{n}, X n ≃* X n)
(r : Π{n}, X n →* X n)
(p : Π{n : N} (x : X (S n)), g (e x) = tcc_to_fn X n x)
(pr : Π{n : N} (x : X (S n)), g x = r (g (e x))) : type_chain_complex N :=
type_chain_complex.mk X @g
abstract begin
have p' : Π{n : N} (x : X (S n)), g x = tcc_to_fn X n (e⁻¹ x),
from λn, homotopy_inv_of_homotopy_pre e _ _ p,
intro n x,
refine ap g !p' ⬝ !pr ⬝ _,
refine ap r !p ⬝ _,
refine ap r (tcc_is_chain_complex X n _) ⬝ _,
apply respect_pt
end end
theorem is_exact_at_t_cancel_aut {X : type_chain_complex N}
{g : Π{n : N}, X (S n) →* X n} {e : Π{n}, X n ≃* X n}
{r : Π{n}, X n →* X n} (l : Π{n}, X n →* X n)
(p : Π{n : N} (x : X (S n)), g (e x) = tcc_to_fn X n x)
(pr : Π{n : N} (x : X (S n)), g x = r (g (e x)))
(pl : Π{n : N} (x : X (S n)), g (l x) = e (g x))
(H : is_exact_at_t X n) : is_exact_at_t (type_chain_complex_cancel_aut X @g @e @r @p @pr) n :=
begin
intro y q, esimp at *,
have H2 : tcc_to_fn X n (e⁻¹ y) = pt,
from (homotopy_inv_of_homotopy_pre e _ _ p _)⁻¹ ⬝ q,
cases (H _ H2) with x s,
refine fiber.mk (l (e x)) _,
refine !pl ⬝ _,
refine ap e (!p ⬝ s) ⬝ _,
apply right_inv
end
-- 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
-- move
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 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 (tcc_is_chain_complex X (f m) _) ⬝ _,
apply respect_pt
end
definition is_exact_at_t_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 *,
have H2 : tcc_to_fn X (f m) ((equiv_of_eq (ap (λx, X x) (c m)))⁻¹ᵉ (e⁻¹ y)) = pt,
begin
refine _ ⬝ ap e⁻¹ᵉ* q ⬝ (respect_pt (e⁻¹ᵉ*)), apply eq_inv_of_eq, clear q, revert y,
apply inv_homotopy_of_homotopy_pre e,
apply inv_homotopy_of_homotopy_pre, apply p
end,
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 *,
have H2 : cc_to_fn X n (e⁻¹ᵉ* y) = pt,
begin
refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
refine ap _ q ⬝ _,
exact respect_pt e⁻¹ᵉ*
end,
induction (H _ H2) with x,
induction x with x r,
refine image.mk (e x) _,
refine (p x)⁻¹ ⬝ _,
refine ap e r ⬝ _,
apply right_inv
end
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 (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 (tcc_is_chain_complex X n x)
end
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 *,
note q := !tr_eq_tr_equiv p,
induction q with q,
induction H x q with y r,
refine image.mk (tr y) _,
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,
have H : Π (x : Y (f (S (S n)))), g (c n ▸ g (c (S n) ▸ x)) = pt,
begin
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
end,
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 *,
have H2 : cc_to_fn X n (e⁻¹ᵉ* ((c n)⁻¹ ▸ y)) = pt,
begin
refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
rewrite [tr_inv_tr, q],
exact respect_pt e⁻¹ᵉ*
end,
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 *,
-- have H2 : lgcc_to_fn X n (e⁻¹ᵉ* y) = pt,
-- begin
-- refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
-- refine ap _ q ⬝ _,
-- exact respect_pt e⁻¹ᵉ*
-- end,
-- 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 type corresponds with 1 in the group.
We need this structure because a chain complex is a sequence of pointed types, and we need
to assume for some of the theorems below that some of these pointed types are groups, where the
unit for multiplication is the point.
-/
structure pgroup [class] (X : Type*) extends semigroup X, has_inv X :=
(pt_mul : Πa, mul pt a = a)
(mul_pt : Πa, mul a pt = a)
(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
/-
The following theorems state that in a chain complex, if certain types are contractible, and
the chain complex is exact at the right spots, a map in the chain complex is an
embedding/surjection/equivalence. For the first and third we also need to assume that
the map is a group homomorphism (and hence that the two types around it are groups).
-/
definition is_embedding_of_trivial (X : chain_complex N) {n : N}
(H : is_exact_at X n) [HX : is_contr (X (S (S n)))]
[pgroup (X n)] [pgroup (X (S n))] [is_homomorphism (cc_to_fn X n)]
: 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,
have r : pt = x, from !is_prop.elim,
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_contr (X n)] : is_surjective (cc_to_fn X (S n)) :=
begin
intro g,
refine trunc.elim _ (H g !is_prop.elim),
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_contr (X n)] [HX2 : is_contr (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
View file

@ -1,59 +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
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
View file

@ -1,97 +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
-/
-- 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 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

425
homotopy/sec86.hlean
View file

@ -1,425 +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
-/
import homotopy.wedge homotopy.homotopy_group homotopy.circle .LES_applications
open eq is_conn is_trunc pointed susp nat pi equiv is_equiv trunc fiber trunc_index
-- definition iterated_loop_ptrunc_pequiv_con' (n : ℕ₋₂) (k : ℕ) (A : Type*)
-- (p q : Ω[k](ptrunc (n+k) (Ω A))) :
-- iterated_loop_ptrunc_pequiv n k (Ω A) (loop_mul trunc_concat p q) =
-- trunc_functor2 (loop_mul concat) (iterated_loop_ptrunc_pequiv n k (Ω A) p)
-- (iterated_loop_ptrunc_pequiv n k (Ω A) q) :=
-- begin
-- revert n p q, induction k with k IH: intro n p q,
-- { reflexivity},
-- { exact sorry}
-- end
theorem elim_type_merid_inv {A : Type} (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
(a : A) : transport (susp.elim_type PN PS Pm) (merid a)⁻¹ = to_inv (Pm a) :=
by rewrite [tr_eq_cast_ap_fn,↑susp.elim_type,ap_inv,elim_merid]; apply cast_ua_inv_fn
definition is_conn_trunc (A : Type) (n k : ℕ₋₂) [H : is_conn n A]
: is_conn n (trunc k A) :=
begin
apply is_trunc_equiv_closed, apply trunc_trunc_equiv_trunc_trunc
end
section open sphere sphere.ops
definition psphere_succ [unfold_full] (n : ℕ) : S. (n + 1) = psusp (S. n) := idp
end
namespace freudenthal section
/- The Freudenthal Suspension Theorem -/
parameters {A : Type*} {n : ℕ} [is_conn n A]
/-
This proof is ported from Agda
This is the 95% version of the Freudenthal Suspension Theorem, which means that we don't
prove that loop_susp_unit : A →* Ω(psusp A) is 2n-connected (if A is n-connected),
but instead we only prove that it induces an equivalence on the first 2n homotopy groups.
-/
definition up (a : A) : north = north :> susp A :=
loop_susp_unit A a
definition code_merid : A → ptrunc (n + n) A → ptrunc (n + n) A :=
begin
have is_conn n (ptrunc (n + n) A), from !is_conn_trunc,
refine wedge_extension.ext n n (λ x y, ttrunc (n + n) A) _ _ _,
{ exact tr},
{ exact id},
{ reflexivity}
end
definition code_merid_β_left (a : A) : code_merid a pt = tr a :=
by apply wedge_extension.β_left
definition code_merid_β_right (b : ptrunc (n + n) A) : code_merid pt b = b :=
by apply wedge_extension.β_right
definition code_merid_coh : code_merid_β_left pt = code_merid_β_right pt :=
begin
symmetry, apply eq_of_inv_con_eq_idp, apply wedge_extension.coh
end
definition is_equiv_code_merid (a : A) : is_equiv (code_merid a) :=
begin
have Πa, is_trunc n.-2.+1 (is_equiv (code_merid a)),
from λa, is_trunc_of_le _ !minus_one_le_succ,
refine is_conn.elim (n.-1) _ _ a,
{ esimp, exact homotopy_closed id (homotopy.symm (code_merid_β_right))}
end
definition code_merid_equiv [constructor] (a : A) : trunc (n + n) A ≃ trunc (n + n) A :=
equiv.mk _ (is_equiv_code_merid a)
definition code_merid_inv_pt (x : trunc (n + n) A) : (code_merid_equiv pt)⁻¹ x = x :=
begin
refine ap010 @(is_equiv.inv _) _ x ⬝ _,
{ exact homotopy_closed id (homotopy.symm code_merid_β_right)},
{ apply is_conn.elim_β},
{ reflexivity}
end
definition code [unfold 4] : susp A → Type :=
susp.elim_type (trunc (n + n) A) (trunc (n + n) A) code_merid_equiv
definition is_trunc_code (x : susp A) : is_trunc (n + n) (code x) :=
begin
induction x with a: esimp,
{ exact _},
{ exact _},
{ apply is_prop.elimo}
end
local attribute is_trunc_code [instance]
definition decode_north [unfold 4] : code north → trunc (n + n) (north = north :> susp A) :=
trunc_functor (n + n) up
definition decode_north_pt : decode_north (tr pt) = tr idp :=
ap tr !con.right_inv
definition decode_south [unfold 4] : code south → trunc (n + n) (north = south :> susp A) :=
trunc_functor (n + n) merid
definition encode' {x : susp A} (p : north = x) : code x :=
transport code p (tr pt)
definition encode [unfold 5] {x : susp A} (p : trunc (n + n) (north = x)) : code x :=
begin
induction p with p,
exact transport code p (tr pt)
end
theorem encode_decode_north (c : code north) : encode (decode_north c) = c :=
begin
have H : Πc, is_trunc (n + n) (encode (decode_north c) = c), from _,
esimp at *,
induction c with a,
rewrite [↑[encode, decode_north, up, code], con_tr, elim_type_merid, ▸*,
code_merid_β_left, elim_type_merid_inv, ▸*, code_merid_inv_pt]
end
definition decode_coh_f (a : A) : tr (up pt) =[merid a] decode_south (code_merid a (tr pt)) :=
begin
refine _ ⬝op ap decode_south (code_merid_β_left a)⁻¹,
apply trunc_pathover,
apply eq_pathover_constant_left_id_right,
apply square_of_eq,
exact whisker_right !con.right_inv (merid a)
end
definition decode_coh_g (a' : A) : tr (up a') =[merid pt] decode_south (code_merid pt (tr a')) :=
begin
refine _ ⬝op ap decode_south (code_merid_β_right (tr a'))⁻¹,
apply trunc_pathover,
apply eq_pathover_constant_left_id_right,
apply square_of_eq, refine !inv_con_cancel_right ⬝ !idp_con⁻¹
end
definition decode_coh_lem {A : Type} {a a' : A} (p : a = a')
: whisker_right (con.right_inv p) p = inv_con_cancel_right p p ⬝ (idp_con p)⁻¹ :=
by induction p; reflexivity
theorem decode_coh (a : A) : decode_north =[merid a] decode_south :=
begin
apply arrow_pathover_left, intro c, esimp at *,
induction c with a',
rewrite [↑code, elim_type_merid, ▸*],
refine wedge_extension.ext n n _ _ _ _ a a',
{ exact decode_coh_f},
{ exact decode_coh_g},
{ clear a a', unfold [decode_coh_f, decode_coh_g], refine ap011 concato_eq _ _,
{ refine ap (λp, trunc_pathover (eq_pathover_constant_left_id_right (square_of_eq p))) _,
apply decode_coh_lem},
{ apply ap (λp, ap decode_south p⁻¹), apply code_merid_coh}}
end
definition decode [unfold 4] {x : susp A} (c : code x) : trunc (n + n) (north = x) :=
begin
induction x with a,
{ exact decode_north c},
{ exact decode_south c},
{ exact decode_coh a}
end
theorem decode_encode {x : susp A} (p : trunc (n + n) (north = x)) : decode (encode p) = p :=
begin
induction p with p, induction p, esimp, apply decode_north_pt
end
parameters (A n)
definition equiv' : trunc (n + n) A ≃ trunc (n + n) (Ω (psusp A)) :=
equiv.MK decode_north encode decode_encode encode_decode_north
definition pequiv' : ptrunc (n + n) A ≃* ptrunc (n + n) (Ω (psusp A)) :=
pequiv_of_equiv equiv' decode_north_pt
-- We don't prove this:
-- theorem freudenthal_suspension : is_conn_fun (n+n) (loop_susp_unit A) :=
end end freudenthal
open algebra
definition freudenthal_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
: ptrunc k A ≃* ptrunc k (Ω (psusp A)) :=
have H' : k ≤[ℕ₋₂] n + n,
by rewrite [mul.comm at H, -algebra.zero_add n at {1}]; exact of_nat_le_of_nat H,
ptrunc_pequiv_ptrunc_of_le H' (freudenthal.pequiv' A n)
definition freudenthal_equiv {A : Type*} {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
: trunc k A ≃ trunc k (Ω (psusp A)) :=
freudenthal_pequiv A H
namespace sphere
open ops algebra pointed function
-- replace with definition in algebra.homotopy_group
definition phomotopy_group_succ_in2 (A : Type*) (n : ℕ) : π*[n + 1] A = π*[n] Ω A :> Type* :=
ap (ptrunc 0) (loop_space_succ_eq_in A n)
definition stability_pequiv_helper (k n : ℕ) (H : k + 2 ≤ 2 * n)
: ptrunc k (Ω(psusp (S. n))) ≃* ptrunc k (S. n) :=
begin
have H' : k ≤ 2 * pred n,
begin
rewrite [mul_pred_right], change pred (pred (k + 2)) ≤ pred (pred (2 * n)),
apply pred_le_pred, apply pred_le_pred, exact H
end,
have is_conn (of_nat (pred n)) (S. n),
begin
cases n with n,
{ exfalso, exact not_succ_le_zero _ H},
{ esimp, apply is_conn_psphere}
end,
symmetry, exact freudenthal_pequiv (S. n) H'
end
definition stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) : π*[k + 1] (S. (n+1)) ≃* π*[k] (S. n) :=
begin
refine pequiv_of_eq (phomotopy_group_succ_in2 (S. (n+1)) k) ⬝e* _,
rewrite psphere_succ,
refine !phomotopy_group_pequiv_loop_ptrunc ⬝e* _,
refine loopn_pequiv_loopn k (stability_pequiv_helper k n H) ⬝e* _,
exact !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*,
end
-- change some "+1"'s intro succ's to avoid this definition (or vice versa)
definition group_homotopy_group2 [instance] (k : ℕ) (A : Type*) :
group (carrier (ptrunctype.to_pType (π*[k + 1] A))) :=
group_homotopy_group k A
definition loop_pequiv_loop_con {A B : Type*} (f : A ≃* B) (p q : Ω A)
: loop_pequiv_loop f (p ⬝ q) = loop_pequiv_loop f p ⬝ loop_pequiv_loop f q :=
loopn_pequiv_loopn_con 0 f p q
definition iterated_loop_ptrunc_pequiv_con {n : ℕ₋₂} {k : ℕ} {A : Type*}
(p q : Ω[succ k] (ptrunc (n+succ k) A)) :
iterated_loop_ptrunc_pequiv n (succ k) A (p ⬝ q) =
trunc_concat (iterated_loop_ptrunc_pequiv n (succ k) A p)
(iterated_loop_ptrunc_pequiv n (succ k) A q) :=
begin
refine _ ⬝ loop_ptrunc_pequiv_con _ _,
exact ap !loop_ptrunc_pequiv !loop_pequiv_loop_con
end
theorem inv_respect_binary_operation {A B : Type} (f : A ≃ B) (mA : A → A → A) (mB : B → B → B)
(p : Πa₁ a₂, f (mA a₁ a₂) = mB (f a₁) (f a₂)) (b₁ b₂ : B) :
f⁻¹ (mB b₁ b₂) = mA (f⁻¹ b₁) (f⁻¹ b₂) :=
begin
refine is_equiv_rect' f⁻¹ _ _ b₁, refine is_equiv_rect' f⁻¹ _ _ b₂,
intros a₂ a₁, apply inv_eq_of_eq, symmetry, exact p a₁ a₂
end
definition iterated_loop_ptrunc_pequiv_inv_con {n : ℕ₋₂} {k : ℕ} {A : Type*}
(p q : ptrunc n (Ω[succ k] A)) :
(iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* (trunc_concat p q) =
(iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* p ⬝
(iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* q :=
inv_respect_binary_operation (iterated_loop_ptrunc_pequiv n (succ k) A) concat trunc_concat
(@iterated_loop_ptrunc_pequiv_con n k A) p q
definition phomotopy_group_pequiv_loop_ptrunc_con {k : ℕ} {A : Type*} (p q : πg[k +1] A) :
phomotopy_group_pequiv_loop_ptrunc (succ k) A (p * q) =
phomotopy_group_pequiv_loop_ptrunc (succ k) A p ⬝
phomotopy_group_pequiv_loop_ptrunc (succ k) A q :=
begin
refine _ ⬝ !loopn_pequiv_loopn_con,
exact ap (loopn_pequiv_loopn _ _) !iterated_loop_ptrunc_pequiv_inv_con
end
definition phomotopy_group_pequiv_loop_ptrunc_inv_con {k : ℕ} {A : Type*}
(p q : Ω[succ k] (ptrunc (succ k) A)) :
(phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* (p ⬝ q) =
(phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* p *
(phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* q :=
inv_respect_binary_operation (phomotopy_group_pequiv_loop_ptrunc (succ k) A) mul concat
(@phomotopy_group_pequiv_loop_ptrunc_con k A) p q
definition tcast [constructor] {n : ℕ₋₂} {A B : n-Type*} (p : A = B) : A →* B :=
pcast (ap ptrunctype.to_pType p)
definition tr_mul_tr {n : ℕ} {A : Type*} (p q : Ω[succ n] A)
: tr p *[π[n + 1] A] tr q = tr (p ⬝ q) :=
idp
-- use this in proof for ghomotopy_group_succ_in
definition phomotopy_group_succ_in2_con {A : Type*} {n : ℕ} (g h : πg[succ n +1] A) :
pcast (phomotopy_group_succ_in2 A (succ n)) (g * h) =
pcast (phomotopy_group_succ_in2 A (succ n)) g * pcast (phomotopy_group_succ_in2 A (succ n)) h :=
begin
induction g with p, induction h with q, esimp,
rewrite [-+ tr_eq_cast_ap, ↑phomotopy_group_succ_in2, -+ tr_compose],
refine ap (transport _ _) !tr_mul_tr ⬝ _,
rewrite [+ trunc_transport],
apply ap tr, apply loop_space_succ_eq_in_concat,
end
definition stability_eq (k n : ℕ) (H : k + 3 ≤ 2 * n) : πg[k+1 +1] (S. (n+1)) = πg[k+1] (S. n) :=
begin
fapply Group_eq,
{ exact equiv_of_pequiv (stability_pequiv (succ k) n H)},
{ intro g h,
refine _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_inv_con,
apply ap !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*,
refine ap (loopn_pequiv_loopn _ _) _ ⬝ !loopn_pequiv_loopn_con,
refine ap !phomotopy_group_pequiv_loop_ptrunc _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_con,
apply phomotopy_group_succ_in2_con
}
end
theorem mul_two {A : Type} [semiring A] (a : A) : a * 2 = a + a :=
by rewrite [-one_add_one_eq_two, left_distrib, +mul_one]
theorem two_mul {A : Type} [semiring A] (a : A) : 2 * a = a + a :=
by rewrite [-one_add_one_eq_two, right_distrib, +one_mul]
definition two_le_succ_succ (n : ℕ) : 2 ≤ succ (succ n) :=
nat.succ_le_succ (nat.succ_le_succ !zero_le)
open int circle hopf
definition πnSn (n : ℕ) : πg[n+1] (S. (succ n)) = gℤ :=
begin
cases n with n IH,
{ exact fundamental_group_of_circle},
{ induction n with n IH,
{ exact π2S2},
{ refine _ ⬝ IH, apply stability_eq,
calc
succ n + 3 = succ (succ n) + 2 : !succ_add⁻¹
... ≤ succ (succ n) + (succ (succ n)) : add_le_add_left !two_le_succ_succ
... = 2 * (succ (succ n)) : !two_mul⁻¹ }}
end
attribute group_integers [constructor]
theorem not_is_trunc_sphere (n : ℕ) : ¬is_trunc n (S. (succ n)) :=
begin
intro H,
note H2 := trivial_homotopy_group_of_is_trunc (S. (succ n)) n n !le.refl,
rewrite [πnSn at H2, ▸* at H2],
have H3 : (0 : ℤ) ≠ (1 : ℤ), from dec_star,
apply H3,
apply is_prop.elim,
end
definition transport11 {A B : Type} (P : A → B → Type) {a a' : A} {b b' : B}
(p : a = a') (q : b = b') (z : P a b) : P a' b' :=
transport (P a') q (p ▸ z)
section
open sphere_index
definition add_plus_one_minus_one (n : ℕ₋₁) : n +1+ -1 = n := idp
definition add_plus_one_succ (n m : ℕ₋₁) : n +1+ (m.+1) = (n +1+ m).+1 := idp
definition minus_one_add_plus_one (n : ℕ₋₁) : -1 +1+ n = n :=
begin induction n with n IH, reflexivity, exact ap succ IH end
definition succ_add_plus_one (n m : ℕ₋₁) : (n.+1) +1+ m = (n +1+ m).+1 :=
begin induction m with m IH, reflexivity, exact ap succ IH end
definition nat_of_sphere_index : ℕ₋₁ → ℕ :=
sphere_index.rec 0 (λx, succ)
definition trunc_index_of_nat_of_sphere_index (n : ℕ₋₁)
: trunc_index.of_nat (nat_of_sphere_index n) = (of_sphere_index n).+1 :=
begin
induction n with n IH,
{ reflexivity},
{ exact ap succ IH}
end
definition sphere_index_of_nat_of_sphere_index (n : ℕ₋₁)
: sphere_index.of_nat (nat_of_sphere_index n) = n.+1 :=
begin
induction n with n IH,
{ reflexivity},
{ exact ap succ IH}
end
definition of_sphere_index_succ (n : ℕ₋₁)
: of_sphere_index (n.+1) = (of_sphere_index n).+1 :=
begin
induction n with n IH,
{ reflexivity},
{ exact ap succ IH}
end
definition sphere_index.of_nat_succ (n : ℕ)
: sphere_index.of_nat (succ n) = (sphere_index.of_nat n).+1 :=
begin
induction n with n IH,
{ reflexivity},
{ exact ap succ IH}
end
definition nat_of_sphere_index_succ (n : ℕ₋₁)
: nat_of_sphere_index (n.+1) = succ (nat_of_sphere_index n) :=
begin
induction n with n IH,
{ reflexivity},
{ exact ap succ IH}
end
definition not_is_trunc_sphere' (n : ℕ₋₁) : ¬is_trunc n (S (n.+1)) :=
begin
cases n with n,
{ esimp [sphere.ops.S, sphere], intro H,
have H2 : is_prop bool, from @(is_trunc_equiv_closed -1 sphere_equiv_bool) H,
have H3 : bool.tt ≠ bool.ff, from dec_star, apply H3, apply is_prop.elim},
{ intro H, apply not_is_trunc_sphere (nat_of_sphere_index n),
rewrite [▸*, trunc_index_of_nat_of_sphere_index, -nat_of_sphere_index_succ,
sphere_index_of_nat_of_sphere_index],
exact H}
end
end
definition π3S2 : πg[2+1] (S. 2) = gℤ :=
(πnS3_eq_πnS2 0)⁻¹ ⬝ πnSn 2
end sphere

12
homotopy/spectrum.hlean
View file

@ -5,7 +5,7 @@ Authors: Michael Shulman
-/
import types.int types.pointed types.trunc homotopy.susp algebra.homotopy_group .chain_complex cubical
import types.int types.pointed types.trunc homotopy.susp algebra.homotopy_group homotopy.chain_complex cubical
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi
/-----------------------------------------
@ -109,7 +109,7 @@ namespace pointed
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))
(calc pfiber (Ω→ f) ≃ Σ(p : Point A = Point A), ap1 f p = rfl : (fiber.sigma_char (ap1 f) (Point (Ω B)))
... ≃ Σ(p : Point A = Point A), (respect_pt f) = ap f p ⬝ (respect_pt f) : (sigma_equiv_sigma_right (λp,
calc (ap1 f p = rfl) ≃ !respect_pt⁻¹ ⬝ (ap f p ⬝ !respect_pt) = rfl : equiv_eq_closed_left _ (con.assoc _ _ _)
... ≃ ap f p ⬝ (respect_pt f) = (respect_pt f) : eq_equiv_inv_con_eq_idp
@ -137,15 +137,15 @@ namespace pointed
definition pequiv_postcompose {A B B' : Type*} (f : A →* B) (g : B ≃* B') : pfiber (g ∘* f) ≃* pfiber f :=
begin
fapply pequiv_of_equiv, esimp,
refine ((transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹) ⬝e (@fiber.equiv_postcompose A B f (Point B) B' g _)),
esimp, apply (ap (fiber.mk (Point A))), rewrite con.assoc, apply inv_con_eq_of_eq_con,
refine transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹ ⬝e fiber.equiv_postcompose f g (Point B),
esimp, apply (ap (fiber.mk (Point A))), refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con,
rewrite [con.assoc, con.right_inv, con_idp, -ap_compose'], apply ap_con_eq_con
end
definition pequiv_precompose {A A' B : Type*} (f : A →* B) (g : A' ≃* A) : pfiber (f ∘* g) ≃* pfiber f :=
begin
fapply pequiv_of_equiv, esimp,
refine (@fiber.equiv_precompose A B f (Point B) A' g _),
refine fiber.equiv_precompose f g (Point B),
esimp, apply (eq_of_fn_eq_fn (fiber.sigma_char _ _)), fapply sigma_eq: esimp,
{ apply respect_pt g },
{ apply pathover_eq_Fl' }
@ -291,7 +291,7 @@ namespace spectrum
definition sid {N : succ_str} (E : gen_spectrum N) : E →ₛ E :=
smap.mk (λn, pid (E n))
(λn, calc glue E n ∘* pid (E n) ~* glue E n : comp_pid
... ~* pid Ω(E (S n)) ∘* glue E n : pid_comp
... ~* pid (Ω(E (S n))) ∘* glue E n : pid_comp
... ~* Ω→(pid (E (S n))) ∘* glue E n : pwhisker_right (glue E n) ap1_id⁻¹*)
definition scompose {N : succ_str} {X Y Z : gen_prespectrum N} (g : Y →ₛ Z) (f : X →ₛ Y) : X →ₛ Z :=