-
Notifications
You must be signed in to change notification settings - Fork 6
/
pi_n.lean
136 lines (109 loc) · 5.03 KB
/
pi_n.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
import category_theory.isomorphism
import category_theory.types
import homotopy_theory.formal.i_category.homotopy_classes
import homotopy_theory.formal.i_category.drag
import .disk_sphere
import .i_category
import .pointed
noncomputable theory
open category_theory (hiding is_iso)
local notation f ` ∘ `:80 g:80 := g ≫ f
namespace homotopy_theory.topological_spaces
open homotopy_theory.cofibrations
open homotopy_theory.cylinder
open homotopy_theory.weak_equivalences
open Top
local notation `Top` := Top.{0}
local notation `Set` := Type.{0}
local notation `[` A `, ` X `]` := homotopy_classes A X
-- We define π₀(X) as the set of homotopy classes of maps from a point
-- to X. π₀ is a functor from Top to Set, namely the functor
-- corepresented on the homotopy category by *.
def π₀ : Top ↝ Set :=
{ obj := λ X, [*, X], map := λ X Y f x, ⟦f⟧ ∘ x,
-- We have to write this proof by hand
-- because `continuous_map` isn't handled by `auto_cases`
map_id' := by { intros X, ext ⟨x⟩, cases x, refl } }
-- The "based n-sphere" is the quotient of D[n] by its boundary S[n-1].
def based_sphere (n : ℕ) : Top :=
quotient_space (sphere_disk_incl n)
def based_sphere_basepoint (n : ℕ) : Top.point ⟶ based_sphere n :=
Top.const (quotient_space.pt _)
lemma based_sphere_well_pointed (n : ℕ) : is_cof (based_sphere_basepoint n) :=
precofibration_category.pushout_is_cof (quotient_space.is_pushout _)
(sphere_disk_cofibration n)
-- We define πₙ(X, x) as the set of homotopy classes of maps D[n]/S[n-1] → X
-- which send the basepoint to x, rel the basepoint.
def π_ (n : ℕ) (X : Top) (x : X) : Set :=
homotopy_classes_extending_rel (based_sphere_basepoint n)
(based_sphere_well_pointed n) (Top.const x)
def π_induced (n : ℕ) {X Y : Top} (x : X) (f : X ⟶ Y) : π_ n X x ⟶ π_ n Y (f x) :=
hcer_induced f
-- Non-Top_ptd-aware versions of functoriality.
--
-- This should really be an application of a lemma `hcer_induced_id`,
-- but writing down the type of that lemma is more annoying than just
-- writing the one-line proof here.
lemma π_induced_id (n : ℕ) {X : Top} (x : X) : π_induced n x (𝟙 X) = id :=
by funext a; induction a using quot.ind; change ⟦_⟧ = _; simp; refl
-- Similarly.
lemma π_induced_comp (n : ℕ) {X Y Z : Top} (x : X) (f : X ⟶ Y) (g : Y ⟶ Z) :
π_induced n x (g ∘ f) = π_induced n (f x) g ∘ π_induced n x f :=
by funext a; induction a using quot.ind; change ⟦_⟧ = ⟦_⟧; simp; refl
def π (n : ℕ) : Top_ptd ↝ Set :=
{ obj := λ Xx, π_ n Xx.space Xx.pt,
map := λ Xx Yy f,
by convert π_induced n Xx.pt f.val; rw f.property,
map_id' := assume Xx, π_induced_id n Xx.pt,
map_comp' := assume Xx Yy Zz f g, begin
-- This is tricky because the action of π on a morphism f involves
-- recursion on the equality `f.property` : f x = y. We need to
-- arrange for z and then y to be "free", i.e., not mentioned
-- earlier in the context, so that we can match on the equality
-- proofs using `subst`.
rcases Xx with ⟨X, x⟩,
rcases Yy with ⟨Y, y⟩,
rcases Zz with ⟨Z, z⟩,
rcases g with ⟨g, hg⟩, change Y ⟶ Z at g, change g y = z at hg,
rcases f with ⟨f, hf⟩, change X ⟶ Y at f, change f x = y at hf,
subst z, subst y,
-- Now we can apply the simple version
exact π_induced_comp n x f g
end }
-- Change-of-basepoint maps.
def path {X : Top} (x x' : X) : Type := homotopy (Top.const x : * ⟶ X) (Top.const x' : * ⟶ X)
def path.induced {X Y : Top} (f : X ⟶ Y) {x x' : X} (γ : path x x') : path (f x) (f x') :=
γ.congr_left f
def path_of_homotopy {X Y : Top} (x : X) {f f' : X ⟶ Y} (H : homotopy f f') :
path (f x) (f' x) :=
H.congr_right (Top.const x)
-- TODO: Move this
def iso_of_equiv {X Y : Set} (e : equiv X Y) : X ≅ Y :=
{ hom := e.to_fun,
inv := e.inv_fun,
hom_inv_id' := funext e.left_inv,
inv_hom_id' := funext e.right_inv }
def change_of_basepoint (n : ℕ) {X : Top} {x x' : X} (γ : path x x') : π_ n X x ≅ π_ n X x' :=
iso_of_equiv $ drag_equiv γ
lemma change_of_basepoint_induced (n : ℕ) {X Y : Top} {x x' : X} (γ : path x x') (f : X ⟶ Y) :
π_induced n x' f ∘ (change_of_basepoint n γ).hom =
(change_of_basepoint n (γ.induced f)).hom ∘ π_induced n x f :=
funext $ drag_equiv_induced _ _
lemma π₀_induced_homotopic {X Y : Top} {f f' : X ⟶ Y} (h : f ≃ f') :
π₀ &> f = π₀ &> f' :=
have ⟦f⟧ = ⟦f'⟧, from quotient.sound h,
funext $ λ x, show ⟦f⟧ ∘ x = ⟦f'⟧ ∘ x, by rw this
-- Homotopic maps induce the same map on πₙ, up to change-of-basepoint
-- identifications.
lemma π_induced_homotopic (n : ℕ) {X Y : Top} (x : X) {f f' : X ⟶ Y} (H : homotopy f f') :
(change_of_basepoint n (path_of_homotopy x H)).hom ∘ π_induced n x f =
π_induced n x f' :=
funext $ hcer_induced_homotopic _
lemma π_induced_homotopic_id (n : ℕ) {X : Top} (x : X) {f : X ⟶ X} (h : 𝟙 X ≃ f) :
is_iso (π_induced n x f) :=
let ⟨H⟩ := h in
begin
rw [←π_induced_homotopic n x H, π_induced_id],
apply iso_iso
end
end homotopy_theory.topological_spaces