182 lines
8.2 KiB
Text
182 lines
8.2 KiB
Text
import types.pointed types.int types.fiber
|
||
|
||
open algebra nat int pointed unit sigma fiber sigma.ops eq equiv prod is_trunc equiv.ops
|
||
|
||
namespace chain_complex
|
||
|
||
structure chain_complex : Type :=
|
||
(car : ℤ → Type*)
|
||
(fn : Π{n : ℤ}, car (n + 1) →* car n)
|
||
(is_chain_complex : Π{n : ℤ} (x : car ((n + 1) + 1)), fn (fn x) = pt)
|
||
|
||
structure left_chain_complex : Type := -- chain complex on the naturals with maps going down
|
||
(car : ℕ → Type*)
|
||
(fn : Π{n : ℕ}, car (n + 1) →* car n)
|
||
(is_chain_complex : Π{n : ℕ} (x : car ((n + 1) + 1)), fn (fn x) = pt)
|
||
|
||
structure right_chain_complex : Type := -- chain complex on the naturals with maps going up
|
||
(car : ℕ → Type*)
|
||
(fn : Π{n : ℕ}, car n →* car (n + 1))
|
||
(is_chain_complex : Π{n : ℕ} (x : car n), fn (fn x) = pt)
|
||
|
||
definition cc_to_car [coercion] := @chain_complex.car
|
||
definition cc_to_fn := @chain_complex.fn
|
||
definition cc_is_chain_complex := @chain_complex.is_chain_complex
|
||
definition lcc_to_car [coercion] := @left_chain_complex.car
|
||
definition lcc_to_fn := @left_chain_complex.fn
|
||
definition lcc_is_chain_complex := @left_chain_complex.is_chain_complex
|
||
definition rcc_to_car [coercion] := @right_chain_complex.car
|
||
definition rcc_to_fn := @right_chain_complex.fn
|
||
definition rcc_is_chain_complex := @right_chain_complex.is_chain_complex
|
||
|
||
-- note: these notions are shifted by one!
|
||
definition is_exact_at [reducible] (X : chain_complex) (n : ℤ) : Type :=
|
||
Π(x : X (n + 1)), cc_to_fn X x = pt → Σ(y : X ((n + 1) + 1)), cc_to_fn X y = x
|
||
definition is_exact_at_l [reducible] (X : left_chain_complex) (n : ℕ) : Type :=
|
||
Π(x : X (n + 1)), lcc_to_fn X x = pt → Σ(y : X ((n + 1) + 1)), lcc_to_fn X y = x
|
||
definition is_exact_at_r [reducible] (X : right_chain_complex) (n : ℕ) : Type :=
|
||
Π(x : X (n + 1)), rcc_to_fn X x = pt → Σ(y : X n), rcc_to_fn X y = x
|
||
|
||
definition is_exact [reducible] (X : chain_complex) : Type := Π(n : ℤ), is_exact_at X n
|
||
definition is_exact_l [reducible] (X : left_chain_complex) : Type := Π(n : ℕ), is_exact_at_l X n
|
||
definition is_exact_r [reducible] (X : right_chain_complex) : Type := Π(n : ℕ), is_exact_at_r X n
|
||
|
||
definition chain_complex_from_left (X : left_chain_complex) : chain_complex :=
|
||
chain_complex.mk (int.rec X (λn, Unit))
|
||
begin
|
||
intro n, fconstructor,
|
||
{ induction n with n n,
|
||
{ exact @lcc_to_fn X n},
|
||
{ esimp, intro x, exact star}},
|
||
{ induction n with n n,
|
||
{ apply respect_pt},
|
||
{ reflexivity}}
|
||
end
|
||
begin
|
||
intro n, induction n with n n,
|
||
{ exact lcc_is_chain_complex X},
|
||
{ esimp, intro x, reflexivity}
|
||
end
|
||
|
||
definition is_exact_from_left {X : left_chain_complex} {n : ℕ} (H : is_exact_at_l X n)
|
||
: is_exact_at (chain_complex_from_left X) n :=
|
||
H
|
||
|
||
-- move to pointed
|
||
definition pfiber [constructor] {X Y : Type*} (f : X →* Y) : Type* :=
|
||
pointed.MK (fiber f pt) (fiber.mk pt !respect_pt)
|
||
|
||
definition pequiv_of_equiv [constructor] {A B : Type*} (f : A ≃ B) (H : f pt = pt) : A ≃* B :=
|
||
pequiv.mk' (pmap.mk f H)
|
||
|
||
definition fiber_sequence_helper [constructor] (v : Σ(X Y : Type*), X →* Y)
|
||
: Σ(Z X : Type*), Z →* X :=
|
||
⟨pfiber v.2.2, v.1, pmap.mk point rfl⟩
|
||
|
||
definition fiber_sequence_carrier {X Y : Type*} (f : X →* Y) (n : ℕ) : Type* :=
|
||
nat.cases_on n Y (λk, (iterate fiber_sequence_helper k ⟨X, Y, f⟩).1)
|
||
|
||
definition fiber_sequence_fun {X Y : Type*} (f : X →* Y) (n : ℕ)
|
||
: fiber_sequence_carrier f (n + 1) →* fiber_sequence_carrier f n :=
|
||
nat.cases_on n f proof (λk, pmap.mk point rfl) qed
|
||
|
||
/- Definition 8.4.3 -/
|
||
definition fiber_sequence.{u} {X Y : Pointed.{u}} (f : X →* Y) : left_chain_complex.{u} :=
|
||
begin
|
||
fconstructor,
|
||
{ exact fiber_sequence_carrier f},
|
||
{ exact fiber_sequence_fun f},
|
||
{ intro n x, cases n with n,
|
||
{ exact point_eq x},
|
||
{ exact point_eq x}}
|
||
end
|
||
|
||
definition is_exact_fiber_sequence {X Y : Type*} (f : X →* Y) : is_exact_l (fiber_sequence f) :=
|
||
begin
|
||
intro n x p, cases n with n,
|
||
{ exact ⟨fiber.mk x p, rfl⟩},
|
||
{ exact ⟨fiber.mk x p, rfl⟩}
|
||
end
|
||
|
||
-- move to types.sigma
|
||
definition sigma_assoc_comm_equiv [constructor] {A : Type} (B C : A → Type)
|
||
: (Σ(v : Σa, B a), C v.1) ≃ (Σ(u : Σa, C a), B u.1) :=
|
||
calc (Σ(v : Σa, B a), C v.1)
|
||
≃ (Σa (b : B a), C a) : !sigma_assoc_equiv⁻¹
|
||
... ≃ (Σa, B a × C a) : sigma_equiv_sigma_id (λa, !equiv_prod)
|
||
... ≃ (Σa, C a × B a) : sigma_equiv_sigma_id (λa, !prod_comm_equiv)
|
||
... ≃ (Σa (c : C a), B a) : sigma_equiv_sigma_id (λa, !equiv_prod)
|
||
... ≃ (Σ(u : Σa, C a), B u.1) : sigma_assoc_equiv
|
||
|
||
attribute is_equiv_sigma_functor is_equiv.is_equiv_id pequiv.mk' [constructor]
|
||
attribute sigma.eta [unfold 3]
|
||
|
||
-- set_option pp.notation false
|
||
/- Lemma 8.4.4(i) -/
|
||
definition fiber_sequence_carrier_equiv0.{u} {X Y : Pointed.{u}} (f : X →* Y)
|
||
: fiber_sequence_carrier f 3 ≃* Ω Y :=
|
||
pequiv_of_equiv
|
||
(calc
|
||
fiber_sequence_carrier f 3 ≃ fiber (fiber_sequence_fun f 1) pt : erfl
|
||
... ≃ Σ(x : fiber_sequence_carrier f 2), fiber_sequence_fun f 1 x = pt : fiber.sigma_char
|
||
... ≃ Σ(v : fiber f pt), fiber_sequence_fun f 1 v = pt : erfl
|
||
... ≃ Σ(v : Σ(x : X), f x = pt), fiber_sequence_fun f 1 (fiber.mk v.1 v.2) = pt
|
||
: sigma_equiv_sigma_left !fiber.sigma_char
|
||
... ≃ Σ(v : Σ(x : X), f x = pt), v.1 = pt : erfl
|
||
... ≃ Σ(v : Σ(x : X), x = pt), f v.1 = pt : sigma_assoc_comm_equiv
|
||
... ≃ f !center.1 = pt : sigma_equiv_of_is_contr_left _
|
||
... ≃ f pt = pt : erfl
|
||
... ≃ pt = pt : by exact !equiv_eq_closed_left !respect_pt
|
||
... ≃ Ω Y : erfl)
|
||
begin
|
||
change (respect_pt f)⁻¹ ⬝
|
||
((center_eq ⟨Pointed.Point X, refl (Pointed.Point X)⟩)⁻¹ ▸ respect_pt f) = idp,
|
||
rewrite tr_constant,
|
||
apply con.left_inv
|
||
end
|
||
|
||
/- (generalization of) Lemma 8.4.4(ii) -/
|
||
definition fiber_sequence_carrier_equiv1.{u} {X Y : Pointed.{u}} (f : X →* Y) (n : ℕ)
|
||
: fiber_sequence_carrier f (n+4) ≃* Ω(fiber_sequence_carrier f (n+1)) :=
|
||
pequiv_of_equiv
|
||
(calc
|
||
fiber_sequence_carrier f (n+4) ≃ fiber (fiber_sequence_fun f (n+2)) pt : erfl
|
||
... ≃ Σ(x : fiber_sequence_carrier f _), fiber_sequence_fun f (n+2) x = pt
|
||
: fiber.sigma_char
|
||
... ≃ Σ(x : fiber (fiber_sequence_fun f (n+1)) pt), fiber_sequence_fun f _ x = pt
|
||
: erfl
|
||
... ≃ Σ(v : Σ(x : fiber_sequence_carrier f _), fiber_sequence_fun f _ x = pt),
|
||
fiber_sequence_fun f _ (fiber.mk v.1 v.2) = pt
|
||
: by exact sigma_equiv_sigma !fiber.sigma_char (λa, erfl)
|
||
... ≃ Σ(v : Σ(x : fiber_sequence_carrier f _), fiber_sequence_fun f _ x = pt),
|
||
v.1 = pt
|
||
: erfl
|
||
... ≃ Σ(v : Σ(x : fiber_sequence_carrier f _), x = pt),
|
||
fiber_sequence_fun f _ v.1 = pt
|
||
: sigma_assoc_comm_equiv
|
||
... ≃ fiber_sequence_fun f _ !center.1 = pt
|
||
: @(sigma_equiv_of_is_contr_left _) !is_contr_sigma_eq'
|
||
... ≃ fiber_sequence_fun f _ pt = pt
|
||
: erfl
|
||
... ≃ pt = pt
|
||
: by exact !equiv_eq_closed_left !respect_pt
|
||
... ≃ Ω(fiber_sequence_carrier f (n+1)) : erfl)
|
||
begin reflexivity end
|
||
|
||
/- Lemma 8.4.4 (i)(ii), combined -/
|
||
definition fiber_sequence_carrier_equiv {X Y : Type*} (f : X →* Y) (n : ℕ)
|
||
: fiber_sequence_carrier f (n+3) ≃* Ω(fiber_sequence_carrier f n) :=
|
||
nat.cases_on n (fiber_sequence_carrier_equiv0 f) (fiber_sequence_carrier_equiv1 f)
|
||
exit
|
||
/- Lemma 8.4.4(iii) -/
|
||
definition fiber_sequence_function0 {X Y : Type*} (f : X →* Y)
|
||
: Π(x : fiber_sequence_carrier f 4), ap1 f (fiber_sequence_carrier_equiv f 1 x)⁻¹ᵖ =
|
||
fiber_sequence_carrier_equiv f 0 (fiber_sequence_fun f 3 x) :=
|
||
take (x : fiber (fiber_sequence_fun f 2) pt),
|
||
obtain (v : fiber (fiber_sequence_fun f 1) pt) (q : _), from x,
|
||
begin
|
||
unfold [fiber_sequence_carrier_equiv,fiber_sequence_carrier_equiv0,fiber_sequence_carrier_equiv1,equiv.trans, equiv.symm, pequiv._trans_of_to_pmap],
|
||
esimp [sigma_assoc_equiv, equiv.symm, equiv.trans], unfold [fiber_sequence_fun, fiber_sequence_carrier]
|
||
end
|
||
|
||
end chain_complex
|