Merge branch 'master' of github.com:fpvandoorn/Spectral
This commit is contained in:
Yuri Sulyma
commit
ec852ca73f
12 changed files with 228 additions and 82 deletions
|
|
@ -12,32 +12,27 @@ open eq algebra is_trunc set_quotient relation sigma prod sum list trunc functio
|
|||
|
||||
namespace group
|
||||
|
||||
variables {G G' : AddGroup} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
|
||||
{A B : AddAbGroup}
|
||||
|
||||
variables (X : Set) {l l' : list (X ⊎ X)}
|
||||
|
||||
section
|
||||
|
||||
parameters {I : Set} (Y : I → AddAbGroup)
|
||||
variables {A' : AddAbGroup} {Y' : I → AddAbGroup}
|
||||
parameters {I : Type} [is_set I] (Y : I → AbGroup)
|
||||
variables {A' : AbGroup} {Y' : I → AbGroup}
|
||||
|
||||
definition dirsum_carrier : AddAbGroup := free_ab_group (trunctype.mk (Σi, Y i) _)
|
||||
definition dirsum_carrier : AbGroup := free_ab_group (Σi, Y i)
|
||||
local abbreviation ι [constructor] := @free_ab_group_inclusion
|
||||
inductive dirsum_rel : dirsum_carrier → Type :=
|
||||
| rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ + ι ⟨i, y₂⟩ + -(ι ⟨i, y₁ + y₂⟩))
|
||||
| rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹)
|
||||
|
||||
definition dirsum : AddAbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
|
||||
definition dirsum : AbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
|
||||
|
||||
-- definition dirsum_carrier_incl [constructor] (i : I) : Y i →a dirsum_carrier :=
|
||||
-- definition dirsum_carrier_incl [constructor] (i : I) : Y i →g dirsum_carrier :=
|
||||
|
||||
definition dirsum_incl [constructor] (i : I) : Y i →a dirsum :=
|
||||
add_homomorphism.mk (λy, class_of (ι ⟨i, y⟩))
|
||||
definition dirsum_incl [constructor] (i : I) : Y i →g dirsum :=
|
||||
homomorphism.mk (λy, class_of (ι ⟨i, y⟩))
|
||||
begin intro g h, symmetry, apply gqg_eq_of_rel, apply tr, apply dirsum_rel.rmk end
|
||||
|
||||
parameter {Y}
|
||||
definition dirsum.rec {P : dirsum → Type} [H : Πg, is_prop (P g)]
|
||||
(h₁ : Πi (y : Y i), P (dirsum_incl i y)) (h₂ : P 0) (h₃ : Πg h, P g → P h → P (g + h)) :
|
||||
(h₁ : Πi (y : Y i), P (dirsum_incl i y)) (h₂ : P 1) (h₃ : Πg h, P g → P h → P (g * h)) :
|
||||
Πg, P g :=
|
||||
begin
|
||||
refine @set_quotient.rec_prop _ _ _ H _,
|
||||
|
|
@ -49,42 +44,42 @@ namespace group
|
|||
exact h₃ _ _ (h₁ i y) ih,
|
||||
induction v with i y,
|
||||
refine h₃ (gqg_map _ _ (class_of [inr ⟨i, y⟩])) _ _ ih,
|
||||
refine transport P _ (h₁ i (-y)),
|
||||
refine transport P _ (h₁ i y⁻¹),
|
||||
refine _ ⬝ !one_mul,
|
||||
refine _ ⬝ ap (λx, mul x _) (to_respect_zero (dirsum_incl i)),
|
||||
apply gqg_eq_of_rel',
|
||||
apply tr, esimp,
|
||||
refine transport dirsum_rel _ (dirsum_rel.rmk i (-y) y),
|
||||
rewrite [add.left_inv, add.assoc],
|
||||
refine transport dirsum_rel _ (dirsum_rel.rmk i y⁻¹ y),
|
||||
rewrite [mul.left_inv, mul.assoc],
|
||||
end
|
||||
|
||||
definition dirsum_homotopy {φ ψ : dirsum →a A'}
|
||||
definition dirsum_homotopy {φ ψ : dirsum →g A'}
|
||||
(h : Πi (y : Y i), φ (dirsum_incl i y) = ψ (dirsum_incl i y)) : φ ~ ψ :=
|
||||
begin
|
||||
refine dirsum.rec _ _ _,
|
||||
exact h,
|
||||
refine !to_respect_zero ⬝ !to_respect_zero⁻¹,
|
||||
intro g₁ g₂ h₁ h₂, rewrite [+ to_respect_add', h₁, h₂]
|
||||
intro g₁ g₂ h₁ h₂, rewrite [* to_respect_mul, h₁, h₂]
|
||||
end
|
||||
|
||||
definition dirsum_elim_resp_quotient (f : Πi, Y i →a A') (g : dirsum_carrier)
|
||||
definition dirsum_elim_resp_quotient (f : Πi, Y i →g A') (g : dirsum_carrier)
|
||||
(r : ∥dirsum_rel g∥) : free_ab_group_elim (λv, f v.1 v.2) g = 1 :=
|
||||
begin
|
||||
induction r with r, induction r,
|
||||
rewrite [to_respect_add, to_respect_neg, to_respect_add, ▸*, ↑foldl, +one_mul,
|
||||
to_respect_add'], apply mul.right_inv
|
||||
rewrite [to_respect_mul, to_respect_inv, to_respect_mul, ▸*, ↑foldl, *one_mul,
|
||||
to_respect_mul], apply mul.right_inv
|
||||
end
|
||||
|
||||
definition dirsum_elim [constructor] (f : Πi, Y i →a A') : dirsum →a A' :=
|
||||
definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' :=
|
||||
gqg_elim _ (free_ab_group_elim (λv, f v.1 v.2)) (dirsum_elim_resp_quotient f)
|
||||
|
||||
definition dirsum_elim_compute (f : Πi, Y i →a A') (i : I) :
|
||||
definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) :
|
||||
dirsum_elim f ∘g dirsum_incl i ~ f i :=
|
||||
begin
|
||||
intro g, apply zero_add
|
||||
intro g, apply one_mul
|
||||
end
|
||||
|
||||
definition dirsum_elim_unique (f : Πi, Y i →a A') (k : dirsum →a A')
|
||||
definition dirsum_elim_unique (f : Πi, Y i →g A') (k : dirsum →g A')
|
||||
(H : Πi, k ∘g dirsum_incl i ~ f i) : k ~ dirsum_elim f :=
|
||||
begin
|
||||
apply gqg_elim_unique,
|
||||
|
|
@ -94,12 +89,12 @@ namespace group
|
|||
|
||||
end
|
||||
|
||||
variables {I J : Set} {Y Y' Y'' : I → AddAbGroup}
|
||||
variables {I J : Set} {Y Y' Y'' : I → AbGroup}
|
||||
|
||||
definition dirsum_functor [constructor] (f : Πi, Y i →a Y' i) : dirsum Y →a dirsum Y' :=
|
||||
definition dirsum_functor [constructor] (f : Πi, Y i →g Y' i) : dirsum Y →g dirsum Y' :=
|
||||
dirsum_elim (λi, dirsum_incl Y' i ∘g f i)
|
||||
|
||||
theorem dirsum_functor_compose (f' : Πi, Y' i →a Y'' i) (f : Πi, Y i →a Y' i) :
|
||||
theorem dirsum_functor_compose (f' : Πi, Y' i →g Y'' i) (f : Πi, Y i →g Y' i) :
|
||||
dirsum_functor f' ∘a dirsum_functor f ~ dirsum_functor (λi, f' i ∘a f i) :=
|
||||
begin
|
||||
apply dirsum_homotopy,
|
||||
|
|
@ -107,29 +102,29 @@ namespace group
|
|||
end
|
||||
|
||||
variable (Y)
|
||||
definition dirsum_functor_gid : dirsum_functor (λi, aid (Y i)) ~ aid (dirsum Y) :=
|
||||
definition dirsum_functor_gid : dirsum_functor (λi, gid (Y i)) ~ gid (dirsum Y) :=
|
||||
begin
|
||||
apply dirsum_homotopy,
|
||||
intro i y, reflexivity,
|
||||
end
|
||||
variable {Y}
|
||||
|
||||
definition dirsum_functor_add (f f' : Πi, Y i →a Y' i) :
|
||||
homomorphism_add (dirsum_functor f) (dirsum_functor f') ~
|
||||
dirsum_functor (λi, homomorphism_add (f i) (f' i)) :=
|
||||
definition dirsum_functor_mul (f f' : Πi, Y i →g Y' i) :
|
||||
homomorphism_mul (dirsum_functor f) (dirsum_functor f') ~
|
||||
dirsum_functor (λi, homomorphism_mul (f i) (f' i)) :=
|
||||
begin
|
||||
apply dirsum_homotopy,
|
||||
intro i y, esimp, exact sorry
|
||||
end
|
||||
|
||||
definition dirsum_functor_homotopy {f f' : Πi, Y i →a Y' i} (p : f ~2 f') :
|
||||
definition dirsum_functor_homotopy {f f' : Πi, Y i →g Y' i} (p : f ~2 f') :
|
||||
dirsum_functor f ~ dirsum_functor f' :=
|
||||
begin
|
||||
apply dirsum_homotopy,
|
||||
intro i y, exact sorry
|
||||
end
|
||||
|
||||
definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →a dirsum Y :=
|
||||
definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →g dirsum Y :=
|
||||
dirsum_elim (λj, dirsum_incl Y (f j))
|
||||
|
||||
end group
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ namespace group
|
|||
|
||||
variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
|
||||
|
||||
variables (X : Set) {Y : Set} {l l' : list (X ⊎ X)}
|
||||
variables (X : Type) {Y : Type} [is_set X] [is_set Y] {l l' : list (X ⊎ X)}
|
||||
|
||||
/- Free Abelian Group of a set -/
|
||||
namespace free_ab_group
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ namespace group
|
|||
variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
|
||||
|
||||
/- Free Group of a set -/
|
||||
variables (X : Set) {l l' : list (X ⊎ X)}
|
||||
variables (X : Type) [is_set X] {l l' : list (X ⊎ X)}
|
||||
namespace free_group
|
||||
|
||||
inductive free_group_rel : list (X ⊎ X) → list (X ⊎ X) → Type :=
|
||||
|
|
@ -123,7 +123,7 @@ namespace group
|
|||
definition free_group_inclusion [constructor] (x : X) : free_group X :=
|
||||
class_of [inl x]
|
||||
|
||||
definition fgh_helper [unfold 5] (f : X → G) (g : G) (x : X + X) : G :=
|
||||
definition fgh_helper [unfold 6] (f : X → G) (g : G) (x : X + X) : G :=
|
||||
g * sum.rec (λx, f x) (λx, (f x)⁻¹) x
|
||||
|
||||
theorem fgh_helper_respect_rel (f : X → G) (r : free_group_rel X l l')
|
||||
|
|
|
|||
|
|
@ -391,7 +391,7 @@ dirsum_functor (λi, smul_homomorphism (N i) r)
|
|||
definition dirsum_smul_right_distrib (r s : R) (n : dirsum' N) :
|
||||
dirsum_smul (r + s) n = dirsum_smul r n + dirsum_smul s n :=
|
||||
begin
|
||||
refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_add⁻¹,
|
||||
refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_mul⁻¹,
|
||||
intro i ni, exact to_smul_right_distrib r s ni
|
||||
end
|
||||
|
||||
|
|
|
|||
33
algebra/seq_colim.hlean
Normal file
33
algebra/seq_colim.hlean
Normal file
|
|
@ -0,0 +1,33 @@
|
|||
import .direct_sum .quotient_group
|
||||
|
||||
open eq algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops nat
|
||||
|
||||
namespace group
|
||||
|
||||
section
|
||||
|
||||
parameters (A : @trunctype.mk 0 ℕ _ → AbGroup) (f : Πi , A i → A (i + 1))
|
||||
variables {A' : AbGroup}
|
||||
|
||||
definition seq_colim_carrier : AbGroup := dirsum A
|
||||
inductive seq_colim_rel : seq_colim_carrier → Type :=
|
||||
| rmk : Πi a, seq_colim_rel ((dirsum_incl A i a) * (dirsum_incl A (i + 1) (f i a))⁻¹)
|
||||
|
||||
definition seq_colim : AbGroup := quotient_ab_group_gen seq_colim_carrier (λa, ∥seq_colim_rel a∥)
|
||||
|
||||
definition seq_colim_incl [constructor] (i : ℕ) : A i →g seq_colim :=
|
||||
qg_map _ ∘g dirsum_incl A i
|
||||
|
||||
definition seq_colim_quotient (h : Πi, A i →g A') (k : Πi a, h i a = h (i + 1) (f i a))
|
||||
(v : seq_colim_carrier) (r : ∥seq_colim_rel v∥) : dirsum_elim h v = 1 :=
|
||||
begin
|
||||
induction r with r, induction r, exact sorry
|
||||
end
|
||||
|
||||
definition seq_colim_elim [constructor] (h : Πi, A i →g A')
|
||||
(k : Πi a, h i a = h (i + 1) (f i a)) : seq_colim →g A' :=
|
||||
gqg_elim _ (dirsum_elim h) (seq_colim_quotient h k)
|
||||
|
||||
end
|
||||
|
||||
end group
|
||||
66
colim.hlean
66
colim.hlean
|
|
@ -1,6 +1,6 @@
|
|||
-- authors: Floris van Doorn, Egbert Rijke
|
||||
|
||||
import hit.colimit types.fin homotopy.chain_complex .move_to_lib
|
||||
import hit.colimit types.fin homotopy.chain_complex types.pointed2
|
||||
open seq_colim pointed algebra eq is_trunc nat is_equiv equiv sigma sigma.ops chain_complex
|
||||
|
||||
namespace seq_colim
|
||||
|
|
@ -8,12 +8,12 @@ namespace seq_colim
|
|||
definition pseq_colim [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) : Type* :=
|
||||
pointed.MK (seq_colim f) (@sι _ _ 0 pt)
|
||||
|
||||
definition inclusion_pt [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
|
||||
definition inclusion_pt {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
|
||||
: inclusion f (Point (X n)) = Point (pseq_colim f) :=
|
||||
begin
|
||||
induction n with n p,
|
||||
reflexivity,
|
||||
exact (ap (sι f) (respect_pt _))⁻¹ᵖ ⬝ !glue ⬝ p
|
||||
exact (ap (sι f) (respect_pt _))⁻¹ᵖ ⬝ (!glue ⬝ p)
|
||||
end
|
||||
|
||||
definition pinclusion [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
|
||||
|
|
@ -249,6 +249,24 @@ namespace seq_colim
|
|||
{ exact ap (ι _) !respect_pt }
|
||||
end
|
||||
|
||||
definition pshift_equiv_pinclusion {A : ℕ → Type*} (f : Πn, A n →* A (succ n)) (n : ℕ) :
|
||||
psquare (pinclusion f n) (pinclusion (λn, f (n+1)) n) (f n) (pshift_equiv f) :=
|
||||
phomotopy.mk homotopy.rfl begin
|
||||
refine !idp_con ⬝ _, esimp,
|
||||
induction n with n IH,
|
||||
{ esimp[inclusion_pt], esimp[shift_diag], exact !idp_con⁻¹ },
|
||||
{ esimp[inclusion_pt], refine !con_inv_cancel_left ⬝ _,
|
||||
rewrite ap_con, rewrite ap_con,
|
||||
refine _ ⬝ whisker_right _ !con.assoc,
|
||||
refine _ ⬝ (con.assoc (_ ⬝ _) _ _)⁻¹,
|
||||
xrewrite [-IH],
|
||||
esimp[shift_up], rewrite [elim_glue, ap_inv, -ap_compose'], esimp,
|
||||
rewrite [-+con.assoc], apply whisker_right,
|
||||
rewrite con.assoc, apply !eq_inv_con_of_con_eq,
|
||||
symmetry, exact eq_of_square !natural_square
|
||||
}
|
||||
end
|
||||
|
||||
section functor
|
||||
variable {f}
|
||||
variables {A' : ℕ → Type} {f' : seq_diagram A'}
|
||||
|
|
@ -305,6 +323,30 @@ namespace seq_colim
|
|||
: Π(x : seq_colim f), P x :=
|
||||
by induction v with Pincl Pglue; exact seq_colim.rec f Pincl Pglue
|
||||
|
||||
definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Π{n}, A n →* A (n+1)}
|
||||
{f' : Π{n}, A' n →* A' (n+1)} (g : Π{n}, A n ≃* A' n)
|
||||
(p : Π⦃n⦄, g ∘* f ~ f' ∘* g) : pseq_colim @f ≃* pseq_colim @f' :=
|
||||
pequiv_of_equiv (seq_colim_equiv @g p) (ap (ι _) (respect_pt g))
|
||||
|
||||
definition seq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π⦃n⦄, A n → A (n+1)}
|
||||
(p : Π⦃n⦄ (a : A n), f a = f' a) : seq_colim f ≃ seq_colim f' :=
|
||||
seq_colim_equiv (λn, erfl) p
|
||||
|
||||
definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π{n}, A n →* A (n+1)}
|
||||
(p : Π⦃n⦄, f ~ f') : pseq_colim @f ≃* pseq_colim @f' :=
|
||||
pseq_colim_pequiv (λn, pequiv.rfl) p
|
||||
|
||||
definition pseq_colim_pequiv_pinclusion {A A' : ℕ → Type*} {f : Π(n), A n →* A (n+1)}
|
||||
{f' : Π(n), A' n →* A' (n+1)} (g : Π(n), A n ≃* A' n)
|
||||
(p : Π⦃n⦄, g (n+1) ∘* f n ~ f' n ∘* g n) (n : ℕ) :
|
||||
psquare (pinclusion f n) (pinclusion f' n) (g n) (pseq_colim_pequiv g p) :=
|
||||
sorry
|
||||
|
||||
definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : Π⦃n⦄, A n →* A (n+1)}
|
||||
(p : Π⦃n⦄ (a : A n), f a = f' a) (n : ℕ) :
|
||||
pseq_colim_equiv_constant p ∘* pinclusion f n ~* pinclusion f' n :=
|
||||
sorry
|
||||
|
||||
definition is_equiv_seq_colim_rec (P : seq_colim f → Type) :
|
||||
is_equiv (seq_colim_rec_unc :
|
||||
(Σ(Pincl : Π ⦃n : ℕ⦄ (a : A n), P (ι f a)),
|
||||
|
|
@ -327,19 +369,6 @@ namespace seq_colim
|
|||
equiv.mk _ !is_equiv_seq_colim_rec
|
||||
end functor
|
||||
|
||||
definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Π{n}, A n →* A (n+1)}
|
||||
{f' : Π{n}, A' n →* A' (n+1)} (g : Π{n}, A n ≃* A' n)
|
||||
(p : Π⦃n⦄, g ∘* f ~ f' ∘* g) : pseq_colim @f ≃* pseq_colim @f' :=
|
||||
pequiv_of_equiv (seq_colim_equiv @g p) (ap (ι _) (respect_pt g))
|
||||
|
||||
definition seq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π⦃n⦄, A n → A (n+1)}
|
||||
(p : Π⦃n⦄ (a : A n), f a = f' a) : seq_colim f ≃ seq_colim f' :=
|
||||
seq_colim_equiv (λn, erfl) p
|
||||
|
||||
definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π{n}, A n →* A (n+1)}
|
||||
(p : Π⦃n⦄, f ~ f') : pseq_colim @f ≃* pseq_colim @f' :=
|
||||
pseq_colim_pequiv (λn, pequiv.rfl) p
|
||||
|
||||
definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)}
|
||||
(g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~ g n) : pseq_colim @f →* B :=
|
||||
begin
|
||||
|
|
@ -361,6 +390,7 @@ namespace seq_colim
|
|||
theorem prep0_succ_lemma {A : ℕ → Type*} (f : pseq_diagram A) (n : ℕ)
|
||||
(p : rep0 (λn x, f x) n pt = rep0 (λn x, f x) n pt)
|
||||
(q : prep0 f n (Point (A 0)) = Point (A n))
|
||||
|
||||
: loop_equiv_eq_closed (ap (@f n) q ⬝ respect_pt (@f n))
|
||||
(ap (@f n) p) = Ω→(@f n) (loop_equiv_eq_closed q p) :=
|
||||
by rewrite [▸*, con_inv, ↑ap1_gen, +ap_con, ap_inv, +con.assoc]
|
||||
|
|
@ -466,6 +496,10 @@ namespace seq_colim
|
|||
{ exact sorry }
|
||||
end
|
||||
|
||||
definition pseq_colim_loop_pinclusion {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ) :
|
||||
pseq_colim_loop f ∘* Ω→ (pinclusion f n) ~* pinclusion (λn, Ω→(f n)) n :=
|
||||
sorry
|
||||
|
||||
-- open succ_str
|
||||
-- definition pseq_colim_succ_str_change_index' {N : succ_str} {B : N → Type*} (n : N) (m : ℕ)
|
||||
-- (h : Πn, B n →* B (S n)) :
|
||||
|
|
|
|||
|
|
@ -1,23 +1,73 @@
|
|||
import ..homotopy.spectrum ..homotopy.EM ..algebra.arrow_group ..algebra.direct_sum ..homotopy.fwedge ..choice ..homotopy.pushout ..move_to_lib
|
||||
|
||||
open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc
|
||||
function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi smash
|
||||
open eq spectrum int pointed group algebra sphere nat equiv susp is_trunc
|
||||
function fwedge cofiber lift is_equiv choice algebra pi smash
|
||||
|
||||
namespace homology
|
||||
|
||||
/- homology theory -/
|
||||
/- 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)
|
||||
(Hid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x)
|
||||
(Hcompose : Π(n : ℤ) {X Y Z : Type*} (f : Y →* Z) (g : X →* Y),
|
||||
Hh n (f ∘* g) ~ Hh n f ∘ Hh n g)
|
||||
(Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
|
||||
(Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
|
||||
Hsusp n Y ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n X)
|
||||
(Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n f) (Hh n (pcod f)))
|
||||
(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)))
|
||||
|
||||
section
|
||||
parameter (theory : homology_theory)
|
||||
open homology_theory
|
||||
|
||||
theorem HH_base_indep (n : ℤ) {A : Type} (a b : A)
|
||||
: HH theory n (pType.mk A a) ≃g HH theory n (pType.mk A b) :=
|
||||
calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (psusp A) : by exact (Hsusp theory n (pType.mk A a)) ⁻¹ᵍ
|
||||
... ≃g HH theory n (pType.mk A b) : by exact Hsusp theory n (pType.mk A b)
|
||||
|
||||
theorem Hh_homotopy' (n : ℤ) {A B : Type*} (f : A → B) (p q : f pt = pt)
|
||||
: Hh theory n (pmap.mk f p) ~ Hh theory n (pmap.mk f q) := λ x,
|
||||
calc Hh theory n (pmap.mk f p) x
|
||||
= Hh theory n (pmap.mk f p) (Hsusp theory n A ((Hsusp theory n A)⁻¹ᵍ x))
|
||||
: by exact ap (Hh theory n (pmap.mk f p)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x)⁻¹
|
||||
... = Hsusp theory n B (Hh theory (succ n) (pmap.mk (susp.functor f) !refl) ((Hsusp theory n A)⁻¹ x))
|
||||
: by exact (Hsusp_natural theory n (pmap.mk f p) ((Hsusp theory n A)⁻¹ᵍ x))⁻¹
|
||||
... = Hh theory n (pmap.mk f q) (Hsusp theory n A ((Hsusp theory n A)⁻¹ x))
|
||||
: by exact Hsusp_natural theory n (pmap.mk f q) ((Hsusp theory n A)⁻¹ x)
|
||||
... = Hh theory n (pmap.mk f q) x
|
||||
: by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x)
|
||||
|
||||
theorem Hh_homotopy (n : ℤ) {A B : Type*} (f g : A →* B) (h : f ~ g) : Hh theory n f ~ Hh theory n g := λ x,
|
||||
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)))
|
||||
|
||||
definition HH_isomorphism (n : ℤ) {A B : Type*} (e : A ≃* B)
|
||||
: HH theory n A ≃g HH theory n B :=
|
||||
begin
|
||||
fapply isomorphism.mk,
|
||||
{ exact Hh theory n e },
|
||||
fapply adjointify,
|
||||
{ exact Hh theory n e⁻¹ᵉ* },
|
||||
{ intro x, exact calc
|
||||
Hh theory n e (Hh theory n e⁻¹ᵉ* x)
|
||||
= Hh theory n (e ∘* e⁻¹ᵉ*) x : by exact (Hcompose theory n e e⁻¹ᵉ* x)⁻¹
|
||||
... = Hh theory n !pid x : by exact Hh_homotopy n (e ∘* e⁻¹ᵉ*) !pid (to_right_inv e) x
|
||||
... = x : by exact Hid theory n x
|
||||
},
|
||||
{ intro x, exact calc
|
||||
Hh theory n e⁻¹ᵉ* (Hh theory n e x)
|
||||
= Hh theory n (e⁻¹ᵉ* ∘* e) x : by exact (Hcompose theory n e⁻¹ᵉ* e x)⁻¹
|
||||
... = Hh theory n !pid x : by exact Hh_homotopy n (e⁻¹ᵉ* ∘* e) !pid (to_left_inv e) x
|
||||
... = x : by exact Hid theory n x
|
||||
}
|
||||
end
|
||||
|
||||
end
|
||||
|
||||
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)
|
||||
(Hid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x)
|
||||
(Hcompose : Π(n : ℤ) {X Y Z : Type*} (g : Y →* Z) (f : X →* Y) (x : HH n X),
|
||||
Hh n (g ∘* f) x = Hh n g (Hh n f x))
|
||||
(Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
|
||||
(Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
|
||||
Hsusp n Y ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n X)
|
||||
(Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n f) (Hh n (pcod f)))
|
||||
(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))
|
||||
)
|
||||
end homology
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
-- Author: Kuen-Bang Hou (Favonia)
|
||||
|
||||
import core types.lift
|
||||
import ..homotopy.homology
|
||||
import core
|
||||
import .homology
|
||||
|
||||
open eq pointed group algebra circle sphere nat equiv susp
|
||||
function sphere homology int lift
|
||||
|
|
@ -13,9 +13,21 @@ section
|
|||
|
||||
open homology_theory
|
||||
|
||||
theorem Hsphere : Π(n : ℕ), HH theory n (plift (psphere n)) ≃g HH theory 0 (plift (psphere 0)) :=
|
||||
sorry
|
||||
|
||||
theorem Hsphere : Π(n : ℤ)(m : ℕ), HH theory n (plift (psphere m)) ≃g HH theory (n - m) (plift (psphere 0)) :=
|
||||
begin
|
||||
intros n m, revert n, induction m with m,
|
||||
{ exact λ n, isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_zero n)⁻¹ },
|
||||
{ intro n, exact calc
|
||||
HH theory n (plift (psusp (psphere m)))
|
||||
≃g HH theory n (psusp (plift (psphere m))) : by exact HH_isomorphism theory n (plift_psusp (psphere m))
|
||||
... ≃g HH theory (succ (pred n)) (psusp (plift (psphere m)))
|
||||
: by exact isomorphism_ap (λ n, HH theory n (psusp (plift (psphere m)))) (succ_pred n)⁻¹
|
||||
... ≃g HH theory (pred n) (plift (psphere m)) : by exact Hsusp theory (pred n) (plift (psphere m))
|
||||
... ≃g HH theory (pred n - m) (plift (psphere 0)) : by exact v_0 (pred n)
|
||||
... ≃g HH theory (n - succ m) (plift (psphere 0))
|
||||
: by exact isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_sub n 1 m ⬝ ap (λ m, n - m) (add.comm 1 m))
|
||||
}
|
||||
end
|
||||
end
|
||||
|
||||
end homology
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ import homotopy.smash types.pointed2 .pushout homotopy.red_susp
|
|||
open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
|
||||
function red_susp unit
|
||||
|
||||
/- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (?) (notation means suspension, wedge, smash) -/
|
||||
/- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (notation means suspension, wedge, smash) -/
|
||||
|
||||
/- To prove: Σ(X ∧ Y) ≃ X ★ Y (?) (notation means suspension, smash, join) -/
|
||||
|
||||
|
|
|
|||
|
|
@ -396,17 +396,17 @@ namespace spectrum
|
|||
definition spectrify_pequiv {N : succ_str} (X : gen_prespectrum N) (n : N) :
|
||||
spectrify_type X n ≃* Ω (spectrify_type X (S n)) :=
|
||||
begin
|
||||
refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
|
||||
refine !pshift_equiv ⬝e* _,
|
||||
transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)), rotate 1,
|
||||
refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
|
||||
transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)),
|
||||
fapply pseq_colim_pequiv,
|
||||
{ intro n, apply loopn_pequiv_loopn, apply pequiv_ap X, apply succ_str.add_succ },
|
||||
{ intro k, apply to_homotopy,
|
||||
refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (loopn_succ_in_inv_natural (succ k) _) ⬝* _,
|
||||
refine !passoc ⬝* _ ⬝* !passoc⁻¹*, apply pwhisker_left,
|
||||
refine !apn_pcompose⁻¹* ⬝* _ ⬝* !apn_pcompose, apply apn_phomotopy,
|
||||
exact !glue_ptransport⁻¹* }
|
||||
exact !glue_ptransport⁻¹* },
|
||||
refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
|
||||
refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
|
||||
end
|
||||
|
||||
definition spectrify [constructor] {N : succ_str} (X : gen_prespectrum N) : gen_spectrum N :=
|
||||
|
|
@ -426,7 +426,14 @@ namespace spectrum
|
|||
begin
|
||||
fapply smap.mk,
|
||||
{ intro n, exact pinclusion _ 0 },
|
||||
{ intro n, exact sorry }
|
||||
{ intro n, apply phomotopy_of_psquare, refine !pid_pcompose⁻¹* ⬝ph* _,
|
||||
refine !pid_pcompose⁻¹* ⬝ph* _,
|
||||
--pshift_equiv_pinclusion (spectrify_type_fun X n) 0
|
||||
refine _ ⬝v* _,
|
||||
rotate 1, exact pshift_equiv_pinclusion (spectrify_type_fun X n) 0,
|
||||
-- refine !passoc⁻¹* ⬝* pwhisker_left _ _ ⬝* _,
|
||||
exact sorry
|
||||
}
|
||||
end
|
||||
|
||||
definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}
|
||||
|
|
|
|||
|
|
@ -95,6 +95,13 @@ namespace eq
|
|||
|
||||
end eq open eq
|
||||
|
||||
namespace pmap
|
||||
|
||||
definition eta {A B : Type*} (f : A →* B) : pmap.mk f (respect_pt f) = f :=
|
||||
begin induction f, reflexivity end
|
||||
|
||||
end pmap
|
||||
|
||||
namespace trunc
|
||||
|
||||
-- TODO: redefine loopn_ptrunc_pequiv
|
||||
|
|
@ -170,6 +177,9 @@ namespace group
|
|||
-- : @is_mul_hom G G' (@ab_group.to_group _ (AbGroup.struct G)) _ φ :=
|
||||
-- homomorphism.struct φ
|
||||
|
||||
definition isomorphism_ap {A : Type} (F : A → Group) {a b : A} (p : a = b) : F a ≃g F b :=
|
||||
isomorphism_of_eq (ap F p)
|
||||
|
||||
end group open group
|
||||
|
||||
namespace function
|
||||
|
|
|
|||
5
susp_product.hlean
Normal file
5
susp_product.hlean
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
import core
|
||||
open susp smash pointed wedge prod
|
||||
|
||||
definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ (X ∧ Y)) :=
|
||||
sorry
|
||||
Loading…
Reference in a new issue