/-
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

Reduced cohomology of spectra and cohomology theories
-/

import .spectrum .EM ..algebra.arrow_group .fwedge ..choice .pushout ..move_to_lib ..algebra.product_group

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

-- TODO: move
structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
  ( im_in_ker : Π(a:A), g (f a) = pt)
  ( ker_in_im : Π(b:B), (g b = pt) → image f b)

definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) :=
is_exact f g

definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
  (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g :=
is_exact.mk H₁ H₂

definition is_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C}
  (H : is_exact_t f g) : @is_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) :=
begin
  constructor,
  { intro a, esimp, induction a with a,
    exact ap tr (is_exact_t.im_in_ker H a) },
  { intro b p, induction b with b, note q := !tr_eq_tr_equiv p, induction q with q,
    induction is_exact_t.ker_in_im H b q with a r,
    exact image.mk (tr a) (ap tr r) }
end

definition is_exact_homotopy {A B C : Type*} {f f' : A → B} {g g' : B → C}
  (p : f ~ f') (q : g ~ g') (H : is_exact f g) : is_exact f' g' :=
begin
  induction p using homotopy.rec_on_idp,
  induction q using homotopy.rec_on_idp,
  assumption
end

-- move to arrow group

definition ap1_pmap_mul {X Y : Type*} (f g : X →* Ω Y) :
  Ω→ (pmap_mul f g) ~* pmap_mul (Ω→ f) (Ω→ g) :=
begin
  fconstructor,
  { intro p, esimp,
    refine ap1_gen_con_left (respect_pt f) (respect_pt f)
             (respect_pt g) (respect_pt g) p ⬝ _,
    refine !whisker_right_idp ◾ !whisker_left_idp2, },
  { refine !con.assoc ⬝ _,
    refine _ ◾ idp ⬝ _, rotate 1,
    rexact ap1_gen_con_left_idp (respect_pt f) (respect_pt g), esimp,
    refine !con.assoc ⬝ _,
    apply whisker_left, apply inv_con_eq_idp,
    refine !con2_con_con2 ⬝ ap011 concat2 _ _:
      refine eq_of_square (!natural_square ⬝hp !ap_id) ⬝ !con_idp }
end

definition pmap_mul_pcompose {A B C : Type*} (g h : B →* Ω C) (f : A →* B) :
  pmap_mul g h ∘* f ~* pmap_mul (g ∘* f) (h ∘* f) :=
begin
  fconstructor,
  { intro p, reflexivity },
  { esimp, refine !idp_con ⬝ _, refine !con2_con_con2⁻¹ ⬝ whisker_right _ _,
    refine !ap_eq_ap011⁻¹ }
end

definition pcompose_pmap_mul {A B C : Type*} (h : B →* C) (f g : A →* Ω B) :
  Ω→ h ∘* pmap_mul f g ~* pmap_mul (Ω→ h ∘* f) (Ω→ h ∘* g) :=
begin
  fconstructor,
  { intro p, exact ap1_con h (f p) (g p) },
  { refine whisker_left _ !con2_con_con2⁻¹ ⬝ _, refine !con.assoc⁻¹ ⬝ _,
    refine whisker_right _ (eq_of_square !ap1_gen_con_natural) ⬝ _,
    refine !con.assoc ⬝ whisker_left _ _, apply ap1_gen_con_idp }
end

definition loop_psusp_intro_pmap_mul {X Y : Type*} (f g : psusp X →* Ω Y) :
  loop_psusp_intro (pmap_mul f g) ~* pmap_mul (loop_psusp_intro f) (loop_psusp_intro g) :=
pwhisker_right _ !ap1_pmap_mul ⬝* !pmap_mul_pcompose

definition equiv_glue2 (Y : spectrum) (n : ℤ) : Ω (Ω (Y (n+2))) ≃* Y n :=
begin
  refine (!equiv_glue ⬝e* loop_pequiv_loop (!equiv_glue ⬝e* loop_pequiv_loop _))⁻¹ᵉ*,
  refine pequiv_of_eq (ap Y _),
  exact add.assoc n 1 1
end

namespace cohomology

definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum :=
spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*)

definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : AbGroup :=
AbGroup_trunc_pmap X (Y (n+2))

definition ordinary_cohomology [reducible] (X : Type*) (G : AbGroup) (n : ℤ) : AbGroup :=
cohomology X (EM_spectrum G) n

definition ordinary_cohomology_Z [reducible] (X : Type*) (n : ℤ) : AbGroup :=
ordinary_cohomology X agℤ n

notation `H^` n `[`:0 X:0 `, ` Y:0 `]`:0 := cohomology X Y n
notation `H^` n `[`:0 X:0 `]`:0 := ordinary_cohomology_Z X n

-- check H^3[S¹*,EM_spectrum agℤ]
-- check H^3[S¹*]

definition unpointed_cohomology (X : Type) (Y : spectrum) (n : ℤ) : AbGroup :=
cohomology X₊ Y n

/- functoriality -/

definition cohomology_functor [constructor] {X X' : Type*} (f : X' →* X) (Y : spectrum)
  (n : ℤ) : cohomology X Y n →g cohomology X' Y n :=
Group_trunc_pmap_homomorphism f

definition cohomology_functor_pid (X : Type*) (Y : spectrum) (n : ℤ) (f : H^n[X, Y]) :
  cohomology_functor (pid X) Y n f = f :=
!Group_trunc_pmap_pid

definition cohomology_functor_pcompose {X X' X'' : Type*} (f : X' →* X) (g : X'' →* X')
  (Y : spectrum) (n : ℤ) (h : H^n[X, Y]) : cohomology_functor (f ∘* g) Y n h =
  cohomology_functor g Y n (cohomology_functor f Y n h) :=
!Group_trunc_pmap_pcompose

definition cohomology_functor_phomotopy {X X' : Type*} {f g : X' →* X} (p : f ~* g)
  (Y : spectrum) (n : ℤ) : cohomology_functor f Y n ~ cohomology_functor g Y n :=
Group_trunc_pmap_phomotopy p

definition cohomology_functor_phomotopy_refl {X X' : Type*} (f : X' →* X) (Y : spectrum) (n : ℤ)
  (x : H^n[X, Y]) : cohomology_functor_phomotopy (phomotopy.refl f) Y n x = idp :=
Group_trunc_pmap_phomotopy_refl f x

definition cohomology_functor_pconst {X X' : Type*} (Y : spectrum) (n : ℤ) (f : H^n[X, Y]) :
  cohomology_functor (pconst X' X) Y n f = 1 :=
!Group_trunc_pmap_pconst

definition cohomology_isomorphism {X X' : Type*} (f : X' ≃* X) (Y : spectrum) (n : ℤ) :
  H^n[X, Y] ≃g H^n[X', Y] :=
Group_trunc_pmap_isomorphism f

definition cohomology_isomorphism_refl (X : Type*) (Y : spectrum) (n : ℤ) (x : H^n[X,Y]) :
  cohomology_isomorphism (pequiv.refl X) Y n x = x :=
!Group_trunc_pmap_isomorphism_refl

/- suspension axiom -/

definition cohomology_psusp_2 (Y : spectrum) (n : ℤ) :
  Ω (Ω[2] (Y ((n+1)+2))) ≃* Ω[2] (Y (n+2)) :=
begin
  apply loopn_pequiv_loopn 2,
  exact loop_pequiv_loop (pequiv_of_eq (ap Y (add_comm_right n 1 2))) ⬝e* !equiv_glue⁻¹ᵉ*
end

definition cohomology_psusp_1 (X : Type*) (Y : spectrum) (n : ℤ) :
  psusp X →* Ω (Ω (Y (n + 1 + 2))) ≃ X →* Ω (Ω (Y (n+2))) :=
calc
  psusp X →* Ω[2] (Y (n + 1 + 2)) ≃ X →* Ω (Ω[2] (Y (n + 1 + 2))) : psusp_adjoint_loop_unpointed
    ... ≃ X →* Ω[2] (Y (n+2)) : equiv_of_pequiv (pequiv_ppcompose_left
                                                  (cohomology_psusp_2 Y n))

definition cohomology_psusp_1_pmap_mul {X : Type*} {Y : spectrum} {n : ℤ}
  (f g : psusp X →* Ω (Ω (Y (n + 1 + 2)))) : cohomology_psusp_1 X Y n (pmap_mul f g) ~*
  pmap_mul (cohomology_psusp_1 X Y n f) (cohomology_psusp_1 X Y n g) :=
begin
  unfold [cohomology_psusp_1],
  refine pwhisker_left _ !loop_psusp_intro_pmap_mul ⬝* _,
  apply pcompose_pmap_mul
end

definition cohomology_psusp_equiv (X : Type*) (Y : spectrum) (n : ℤ) :
  H^n+1[psusp X, Y] ≃ H^n[X, Y] :=
trunc_equiv_trunc _ (cohomology_psusp_1 X Y n)

definition cohomology_psusp (X : Type*) (Y : spectrum) (n : ℤ) :
  H^n+1[psusp X, Y] ≃g H^n[X, Y] :=
isomorphism_of_equiv (cohomology_psusp_equiv X Y n)
  begin
    intro f₁ f₂, induction f₁ with f₁, induction f₂ with f₂,
    apply ap tr, apply eq_of_phomotopy, exact cohomology_psusp_1_pmap_mul f₁ f₂
  end

definition cohomology_psusp_natural {X X' : Type*} (f : X →* X') (Y : spectrum) (n : ℤ) :
  cohomology_psusp X Y n ∘ cohomology_functor (psusp_functor f) Y (n+1) ~
  cohomology_functor f Y n ∘ cohomology_psusp X' Y n :=
begin
  refine (trunc_functor_compose _ _ _)⁻¹ʰᵗʸ ⬝hty _ ⬝hty trunc_functor_compose _ _ _,
  apply trunc_functor_homotopy, intro g,
  apply eq_of_phomotopy, refine _ ⬝* !passoc⁻¹*, apply pwhisker_left,
  apply loop_psusp_intro_natural
end

/- exactness -/

definition cohomology_exact {X X' : Type*} (f : X →* X') (Y : spectrum) (n : ℤ) :
  is_exact_g (cohomology_functor (pcod f) Y n) (cohomology_functor f Y n) :=
is_exact_trunc_functor (cofiber_exact f)

/- additivity -/

definition additive_hom [constructor] {I : Type} (X : I → Type*) (Y : spectrum) (n : ℤ) :
  H^n[⋁X, Y] →g Πᵍ i, H^n[X i, Y] :=
Group_pi_intro (λi, cohomology_functor (pinl i) Y n)

definition additive_equiv.{u} {I : Type.{u}} (H : has_choice 0 I) (X : I → Type*) (Y : spectrum)
  (n : ℤ) : H^n[⋁X, Y] ≃ Πᵍ i, H^n[X i, Y] :=
trunc_fwedge_pmap_equiv H X (Ω[2] (Y (n+2)))

definition spectrum_additive {I : Type} (H : has_choice 0 I) (X : I → Type*) (Y : spectrum)
  (n : ℤ) : is_equiv (additive_hom X Y n) :=
is_equiv_of_equiv_of_homotopy (additive_equiv H X Y n) begin intro f, induction f, reflexivity end

/- dimension axiom for ordinary cohomology -/
open is_conn trunc_index
theorem EM_dimension' (G : AbGroup) (n : ℤ) (H : n ≠ 0) :
  is_contr (ordinary_cohomology pbool G n) :=
begin
  apply is_conn_equiv_closed 0 !pmap_pbool_equiv⁻¹ᵉ,
  apply is_conn_equiv_closed 0 !equiv_glue2⁻¹ᵉ,
  cases n with n n,
  { cases n with n,
    { exfalso, apply H, reflexivity },
    { apply is_conn_of_le, apply zero_le_of_nat n, exact is_conn_EMadd1 G n, }},
  { apply is_trunc_trunc_of_is_trunc, apply @is_contr_loop_of_is_trunc (n+1) (K G 0),
    apply is_trunc_of_le _ (zero_le_of_nat n) }
end

theorem EM_dimension (G : AbGroup) (n : ℤ) (H : n ≠ 0) :
  is_contr (ordinary_cohomology (plift pbool) G n) :=
@(is_trunc_equiv_closed_rev -2
  (equiv_of_isomorphism (cohomology_isomorphism (pequiv_plift pbool) _ _)))
  (EM_dimension' G n H)

/- cohomology theory -/

structure cohomology_theory.{u} : Type.{u+1} :=
  (HH : ℤ → pType.{u} → AbGroup.{u})
  (Hiso : Π(n : ℤ) {X Y : Type*} (f : X ≃* Y), HH n Y ≃g HH n X)
  (Hiso_refl : Π(n : ℤ) (X : Type*) (x : HH n X), Hiso n pequiv.rfl x = x)
  (Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), HH n Y →g HH n X)
  (Hhomotopy : Π(n : ℤ) {X Y : Type*} {f g : X →* Y} (p : f ~* g), Hh n f ~ Hh n g)
  (Hhomotopy_refl : Π(n : ℤ) {X Y : Type*} (f : X →* Y) (x : HH n Y),
    Hhomotopy n (phomotopy.refl f) x = idp)
  (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) (z : HH n Z),
    Hh n (g ∘* f) z = Hh n f (Hh n g z))
  (Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
  (Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
    Hsusp n X ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n Y)
  (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n (pcod f)) (Hh n f))
  (Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice 0 I →
    is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i)))

structure ordinary_theory.{u} extends cohomology_theory.{u} : Type.{u+1} :=
 (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift pbool)))

attribute cohomology_theory.HH [coercion]
postfix `^→`:90 := cohomology_theory.Hh
open cohomology_theory

definition Hequiv (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X ≃* Y) : H n Y ≃ H n X :=
equiv_of_isomorphism (Hiso H n f)

definition Hsusp_neg (H : cohomology_theory) (n : ℤ) (X : Type*) : H n (psusp X) ≃g H (pred n) X :=
isomorphism_of_eq (ap (λn, H n _) proof (sub_add_cancel n 1)⁻¹ qed) ⬝g cohomology_theory.Hsusp H (pred n) X

definition Hsusp_neg_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X →* Y) :
  Hsusp_neg H n X ∘ H ^→ n (psusp_functor f) ~ H ^→ (pred n) f ∘ Hsusp_neg H n Y :=
sorry

definition Hsusp_inv_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X →* Y) :
  H ^→ (succ n) (psusp_functor f) ∘g (Hsusp H n Y)⁻¹ᵍ ~ (Hsusp H n X)⁻¹ᵍ ∘ H ^→ n f :=
sorry

definition Hsusp_neg_inv_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X →* Y) :
  H ^→ n (psusp_functor f) ∘g (Hsusp_neg H n Y)⁻¹ᵍ ~ (Hsusp_neg H n X)⁻¹ᵍ ∘ H ^→ (pred n) f :=
sorry

definition Hadditive_equiv (H : cohomology_theory) (n : ℤ) {I : Type} (X : I → Type*) (H2 : has_choice 0 I)
  : H n (⋁ X) ≃g Πᵍ i, H n (X i) :=
isomorphism.mk _ (Hadditive H n X H2)

definition Hlift_empty.{u} (H : cohomology_theory.{u}) (n : ℤ) :
  is_contr (H n (plift punit)) :=
let P : lift empty → Type* := lift.rec empty.elim in
let x := Hadditive H n P _ in
begin
  note z := equiv.mk _ x,
  refine @(is_trunc_equiv_closed_rev -2 (_ ⬝e z ⬝e _)) !is_contr_unit,
    refine Hequiv H n (pequiv_punit_of_is_contr _ _ ⬝e* !pequiv_plift),
    apply is_contr_fwedge_of_neg, intro y, induction y with y, exact y,
  apply equiv_unit_of_is_contr, apply is_contr_pi_of_neg, intro y, induction y with y, exact y
end

definition Hempty (H : cohomology_theory.{0}) (n : ℤ) :
  is_contr (H n punit) :=
@(is_trunc_equiv_closed _ (Hequiv H n !pequiv_plift)) (Hlift_empty H n)

definition Hconst (H : cohomology_theory) (n : ℤ) {X Y : Type*} (y : H n Y) : H ^→ n (pconst X Y) y = 1 :=
begin
  refine Hhomotopy H n (pconst_pcompose (pconst X (plift punit)))⁻¹* y ⬝ _,
  refine Hcompose H n _ _ y ⬝ _,
  refine ap (H ^→ n _) (@eq_of_is_contr _ (Hlift_empty H n) _ 1) ⬝ _,
  apply respect_one
end

-- definition Hwedge (H : cohomology_theory) (n : ℤ) (A B : Type*) : H n (A ∨ B) ≃g H n A ×ag H n B :=
-- begin
--   refine Hiso H n (pwedge_pequiv_fwedge A B)⁻¹ᵉ* ⬝g _,
--   refine Hadditive_equiv H n _ _ ⬝g _
-- end

definition cohomology_theory_spectrum.{u} [constructor] (Y : spectrum.{u}) : cohomology_theory.{u} :=
cohomology_theory.mk
  (λn A, H^n[A, Y])
  (λn A B f, cohomology_isomorphism f Y n)
  (λn A, cohomology_isomorphism_refl A Y n)
  (λn A B f, cohomology_functor f Y n)
  (λn A B f g p, cohomology_functor_phomotopy p Y n)
  (λn A B f x, cohomology_functor_phomotopy_refl f Y n x)
  (λn A x, cohomology_functor_pid A Y n x)
  (λn A B C g f x, cohomology_functor_pcompose g f Y n x)
  (λn A, cohomology_psusp A Y n)
  (λn A B f, cohomology_psusp_natural f Y n)
  (λn A B f, cohomology_exact f Y n)
  (λn I A H, spectrum_additive H A Y n)

-- set_option pp.universes true
-- set_option pp.abbreviations false
-- print cohomology_theory_spectrum
-- print EM_spectrum
-- print has_choice_lift
-- print equiv_lift
-- print has_choice_equiv_closed
definition ordinary_theory_EM [constructor] (G : AbGroup) : ordinary_theory :=
⦃ordinary_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄

end cohomology