2017-06-08 15:54:47 +00:00
|
|
|
|
/-
|
|
|
|
|
Copyright (c) 2017 Yuri Sulyma, Favonia
|
|
|
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
|
Authors: Yuri Sulyma, Favonia
|
|
|
|
|
|
|
|
|
|
Reduced homology theories
|
|
|
|
|
-/
|
|
|
|
|
|
2017-06-06 18:08:37 +00:00
|
|
|
|
import ..homotopy.spectrum ..homotopy.EM ..algebra.arrow_group ..algebra.direct_sum ..homotopy.fwedge ..choice ..homotopy.pushout ..move_to_lib
|
2017-06-06 16:22:11 +00:00
|
|
|
|
|
2017-06-06 22:57:34 +00:00
|
|
|
|
open eq spectrum int pointed group algebra sphere nat equiv susp is_trunc
|
|
|
|
|
function fwedge cofiber lift is_equiv choice algebra pi smash
|
2017-06-06 16:22:11 +00:00
|
|
|
|
|
|
|
|
|
namespace homology
|
|
|
|
|
|
2017-06-06 20:29:41 +00:00
|
|
|
|
/- homology theory -/
|
|
|
|
|
|
|
|
|
|
structure homology_theory.{u} : Type.{u+1} :=
|
|
|
|
|
(HH : ℤ → pType.{u} → AbGroup.{u})
|
|
|
|
|
(Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), HH n X →g HH n Y)
|
2017-06-08 16:14:07 +00:00
|
|
|
|
(Hpid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x)
|
|
|
|
|
(Hpcompose : Π(n : ℤ) {X Y Z : Type*} (f : Y →* Z) (g : X →* Y),
|
2017-06-06 22:57:55 +00:00
|
|
|
|
Hh n (f ∘* g) ~ Hh n f ∘ Hh n g)
|
2017-06-08 16:14:07 +00:00
|
|
|
|
(Hpsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
|
|
|
|
|
(Hpsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
|
|
|
|
|
Hpsusp n Y ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hpsusp n X)
|
2017-06-06 20:29:41 +00:00
|
|
|
|
(Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n f) (Hh n (pcod f)))
|
2017-06-06 22:57:55 +00:00
|
|
|
|
(Hadditive : Π(n : ℤ) {I : Set.{u}} (X : I → Type*), is_equiv
|
|
|
|
|
(dirsum_elim (λi, Hh n (pinl i)) : dirsum (λi, HH n (X i)) → HH n (⋁ X)))
|
2017-06-06 20:29:41 +00:00
|
|
|
|
|
2017-06-08 15:54:47 +00:00
|
|
|
|
structure ordinary_homology_theory.{u} extends homology_theory.{u} : Type.{u+1} :=
|
|
|
|
|
(Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift (psphere 0))))
|
|
|
|
|
|
2017-06-06 20:29:41 +00:00
|
|
|
|
section
|
|
|
|
|
parameter (theory : homology_theory)
|
|
|
|
|
open homology_theory
|
|
|
|
|
|
2017-06-07 05:10:25 +00:00
|
|
|
|
theorem HH_base_indep (n : ℤ) {A : Type} (a b : A)
|
2017-06-06 22:57:55 +00:00
|
|
|
|
: HH theory n (pType.mk A a) ≃g HH theory n (pType.mk A b) :=
|
2017-06-08 16:14:07 +00:00
|
|
|
|
calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (psusp A) : by exact (Hpsusp theory n (pType.mk A a)) ⁻¹ᵍ
|
|
|
|
|
... ≃g HH theory n (pType.mk A b) : by exact Hpsusp theory n (pType.mk A b)
|
2017-06-06 20:29:41 +00:00
|
|
|
|
|
2017-06-07 05:10:25 +00:00
|
|
|
|
theorem Hh_homotopy' (n : ℤ) {A B : Type*} (f : A → B) (p q : f pt = pt)
|
2017-06-06 22:57:55 +00:00
|
|
|
|
: Hh theory n (pmap.mk f p) ~ Hh theory n (pmap.mk f q) := λ x,
|
|
|
|
|
calc Hh theory n (pmap.mk f p) x
|
2017-06-08 16:14:07 +00:00
|
|
|
|
= Hh theory n (pmap.mk f p) (Hpsusp theory n A ((Hpsusp theory n A)⁻¹ᵍ x))
|
|
|
|
|
: by exact ap (Hh theory n (pmap.mk f p)) (equiv.to_right_inv (equiv_of_isomorphism (Hpsusp theory n A)) x)⁻¹
|
|
|
|
|
... = Hpsusp theory n B (Hh theory (succ n) (pmap.mk (susp.functor f) !refl) ((Hpsusp theory n A)⁻¹ x))
|
|
|
|
|
: by exact (Hpsusp_natural theory n (pmap.mk f p) ((Hpsusp theory n A)⁻¹ᵍ x))⁻¹
|
|
|
|
|
... = Hh theory n (pmap.mk f q) (Hpsusp theory n A ((Hpsusp theory n A)⁻¹ x))
|
|
|
|
|
: by exact Hpsusp_natural theory n (pmap.mk f q) ((Hpsusp theory n A)⁻¹ x)
|
2017-06-06 22:57:55 +00:00
|
|
|
|
... = Hh theory n (pmap.mk f q) x
|
2017-06-08 16:14:07 +00:00
|
|
|
|
: by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hpsusp theory n A)) x)
|
2017-06-06 22:57:55 +00:00
|
|
|
|
|
2017-06-07 05:10:25 +00:00
|
|
|
|
theorem Hh_homotopy (n : ℤ) {A B : Type*} (f g : A →* B) (h : f ~ g) : Hh theory n f ~ Hh theory n g := λ x,
|
2017-06-06 22:57:55 +00:00
|
|
|
|
calc Hh theory n f x
|
|
|
|
|
= Hh theory n (pmap.mk f (respect_pt f)) x : by exact ap (λ f, Hh theory n f x) (pmap.eta f)⁻¹
|
|
|
|
|
... = Hh theory n (pmap.mk f (h pt ⬝ respect_pt g)) x : by exact Hh_homotopy' n f (respect_pt f) (h pt ⬝ respect_pt g) x
|
|
|
|
|
... = Hh theory n g x : by exact ap (λ f, Hh theory n f x) (@pmap_eq _ _ (pmap.mk f (h pt ⬝ respect_pt g)) _ h (refl (h pt ⬝ respect_pt g)))
|
|
|
|
|
|
2017-06-06 23:12:50 +00:00
|
|
|
|
definition HH_isomorphism (n : ℤ) {A B : Type*} (e : A ≃* B)
|
|
|
|
|
: HH theory n A ≃g HH theory n B :=
|
2017-06-06 22:57:55 +00:00
|
|
|
|
begin
|
2017-06-06 23:12:50 +00:00
|
|
|
|
fapply isomorphism.mk,
|
|
|
|
|
{ exact Hh theory n e },
|
2017-06-06 22:57:55 +00:00
|
|
|
|
fapply adjointify,
|
|
|
|
|
{ exact Hh theory n e⁻¹ᵉ* },
|
|
|
|
|
{ intro x, exact calc
|
|
|
|
|
Hh theory n e (Hh theory n e⁻¹ᵉ* x)
|
2017-06-08 16:14:07 +00:00
|
|
|
|
= Hh theory n (e ∘* e⁻¹ᵉ*) x : by exact (Hpcompose theory n e e⁻¹ᵉ* x)⁻¹
|
2017-06-06 22:57:55 +00:00
|
|
|
|
... = Hh theory n !pid x : by exact Hh_homotopy n (e ∘* e⁻¹ᵉ*) !pid (to_right_inv e) x
|
2017-06-08 16:14:07 +00:00
|
|
|
|
... = x : by exact Hpid theory n x
|
2017-06-06 22:57:55 +00:00
|
|
|
|
},
|
|
|
|
|
{ intro x, exact calc
|
|
|
|
|
Hh theory n e⁻¹ᵉ* (Hh theory n e x)
|
2017-06-08 16:14:07 +00:00
|
|
|
|
= Hh theory n (e⁻¹ᵉ* ∘* e) x : by exact (Hpcompose theory n e⁻¹ᵉ* e x)⁻¹
|
2017-06-06 22:57:55 +00:00
|
|
|
|
... = Hh theory n !pid x : by exact Hh_homotopy n (e⁻¹ᵉ* ∘* e) !pid (to_left_inv e) x
|
2017-06-08 16:14:07 +00:00
|
|
|
|
... = x : by exact Hpid theory n x
|
2017-06-06 22:57:55 +00:00
|
|
|
|
}
|
|
|
|
|
end
|
|
|
|
|
|
2017-06-06 20:29:41 +00:00
|
|
|
|
end
|
|
|
|
|
|
2017-06-06 16:22:11 +00:00
|
|
|
|
end homology
|