map_indices_dtt_hell.lean

import algebra.category.Module.abelian
import algebra.category.Module.images
import algebra.homology.homology
import algebra.homology.Module
import algebra.homology.homotopy
import .category_theory .linear_algebra

section

open category_theory category_theory.limits homological_complex opposite

local attribute [instance] category_theory.limits.has_zero_object.has_zero
local attribute [instance]
  category_theory.concrete_category.has_coe_to_sort
  category_theory.concrete_category.has_coe_to_fun

universes u u' v v' idx idx'

local attribute [instance] classical.prop_decidable

noncomputable
def homological_complex.map_grading_obj [has_zero_morphisms V] [has_zero_object V]
  {ι' : Type idx'} {c' : complex_shape ι'} (f : ι → ι')
  (h1 : function.injective f) (h2 : ∀ i j, c.rel i j → c'.rel (f i) (f j)) 
  (C : homological_complex V c) : homological_complex V c' := {
    X := λ i, (function.partial_inv f i).cases_on' 0 C.X,
    d := λ i j, match function.partial_inv f i with
                | some i' := match function.partial_inv f j with
                              | some j' := C.d i' j'
                              | none    := 0
                              end
                | none    := 0
                end,
    shape' := by { intros i j h,
                    destruct function.partial_inv f i, { intro h', rw h', refl },
                    intros i' h', rw h', delta homological_complex.map_grading_obj._match_1,
                    destruct function.partial_inv f j, { intro h'', rw h'', refl },
                    intros j' h'', rw h'', delta homological_complex.map_grading_obj._match_2,
                    dsimp, rw C.shape' i' j' (mt (h2 i' j') _),
                    rw function.partial_inv_of_injective h1 i' i at h',
                    rw function.partial_inv_of_injective h1 j' j at h'',
                    rw [h', h''], exact h },
    d_comp_d' := by { intros i j k hij hjk,
                      destruct function.partial_inv f i, { intro h, rw h, exact zero_comp },
                      intros i' h, rw h, delta homological_complex.map_grading_obj._match_1,
                      destruct function.partial_inv f j, { intro h', rw h', exact comp_zero },
                      intros j' h', rw h', delta homological_complex.map_grading_obj._match_2,
                      destruct function.partial_inv f k, { intro h'', rw h'', exact comp_zero },
                      intros k' h'', rw h'', exact C.d_comp_d i' j' k' }
  }

lemma option.dtt_hell {α : Type*} {P : option α → Sort*}
  (case_none : P none) (case_some : Π (a : α), P (some a))
  (o : option α) (h : o.is_some)
  : @option.rec_on α P o case_none case_some == case_some (option.get h) :=
  by { cases o, { exfalso, simp at h, exact h }, { refl } }

lemma homological_complex.map_grading_obj_X_spec
  [has_zero_morphisms V] [has_zero_object V]
  {ι' : Type idx'} {c' : complex_shape ι'} (f : ι → ι')
  (h1 : function.injective f) (h2 : ∀ i j, c.rel i j → c'.rel (f i) (f j)) 
  (C : homological_complex V c)
  (i' : ι') (i : ι) (hi : f i = i')
  : (homological_complex.map_grading_obj f h1 h2 C).X i' = C.X i :=
begin
  delta homological_complex.map_grading_obj,
  dsimp,
  transitivity (some i).cases_on' 0 C.X,
  congr, 
  { rw function.partial_inv_of_injective h1 i i', assumption },
  { refl }
end

noncomputable
def homological_complex.map_grading_obj_id_or_zero_L
  [has_zero_morphisms V] [has_zero_object V]
  {ι' : Type idx'} {c' : complex_shape ι'} (f : ι → ι')
  (h1 : function.injective f) (h2 : ∀ i j, c.rel i j → c'.rel (f i) (f j)) 
  (C : homological_complex V c) (i' : ι') (i : ι)
  : (C.map_grading_obj f h1 h2).X i' ⟶ C.X i :=
  if h : f i = i'
  then eq_to_hom (by { dsimp [homological_complex.map_grading_obj],
                       rw (function.partial_inv_of_injective h1 i i').mpr h,
                       refl })
  else 0

noncomputable
def homological_complex.map_grading_obj_id_or_zero_R
  [has_zero_morphisms V] [has_zero_object V]
  {ι' : Type idx'} {c' : complex_shape ι'} (f : ι → ι')
  (h1 : function.injective f) (h2 : ∀ i j, c.rel i j → c'.rel (f i) (f j)) 
  (C : homological_complex V c) (i' : ι') (i : ι)
  : C.X i ⟶ (C.map_grading_obj f h1 h2).X i' :=
  if h : f i = i'
  then eq_to_hom (by { dsimp [homological_complex.map_grading_obj],
                       rw (function.partial_inv_of_injective h1 i i').mpr h,
                       refl })
  else 0

noncomputable
def homological_complex.map_grading_map
  [has_zero_morphisms V] [has_zero_object V]
  {ι' : Type idx'} {c' : complex_shape ι'} (f : ι → ι')
  (h1 : function.injective f) (h2 : ∀ i j, c.rel i j → c'.rel (f i) (f j)) 
  {C C' : homological_complex V c} (ϕ : C ⟶ C') (i' : ι')
  : (homological_complex.map_grading_obj f h1 h2 C).X i'
  ⟶ (homological_complex.map_grading_obj f h1 h2 C').X i' := 
  @option.rec_on ι (λ o, o.cases_on' 0 C.X ⟶ o.cases_on' 0 C'.X) (function.partial_inv f i') 0 ϕ.f

lemma homological_complex.map_grading_map_spec
  [has_zero_morphisms V] [has_zero_object V]
  {ι' : Type idx'} {c' : complex_shape ι'} (f : ι → ι')
  (h1 : function.injective f) (h2 : ∀ i j, c.rel i j → c'.rel (f i) (f j)) 
  {C C' : homological_complex V c} (ϕ : C ⟶ C')
  (i' : ι') (i : ι) (h : f i = i')
  : homological_complex.map_grading_map f h1 h2 ϕ i' 
  = C.map_grading_obj_id_or_zero_L f h1 h2 i' i
    ≫ ϕ.f i
    ≫ C'.map_grading_obj_id_or_zero_R f h1 h2 i' i :=
begin
  have := (function.partial_inv_of_injective h1 i i').mpr h,
  rw option.eq_some_iff_get_eq at this, cases this with h' h'',
  delta homological_complex.map_grading_map,
  apply eq_of_heq,
  transitivity, apply option.dtt_hell _ _ _ h', rw h'',
  delta homological_complex.map_grading_obj_id_or_zero_L,
  delta homological_complex.map_grading_obj_id_or_zero_R,
  split_ifs,
  rw (category_theory.functor.conj_eq_to_hom_iff_heq (ϕ.f i) (ϕ.f i) rfl rfl).mpr heq.rfl,
  congr,
  all_goals { try { symmetry, apply homological_complex.map_grading_obj_X_spec } },
  all_goals { try { assumption } },
  { symmetry, apply cast_heq },
  { simp },
  { symmetry, apply cast_heq,
    ext, simp, apply homological_complex.map_grading_obj_X_spec; assumption },
end

noncomputable
def homological_complex.map_grading
  [has_zero_morphisms V] [has_zero_object V]
  {ι' : Type idx'} {c' : complex_shape ι'} (f : ι → ι')
  (h1 : function.injective f) (h2 : ∀ i j, c.rel i j → c'.rel (f i) (f j)) 
  : homological_complex V c ⥤ homological_complex V c' := {
    obj := homological_complex.map_grading_obj f h1 h2,
    map := λ C C' ϕ, {
      f := homological_complex.map_grading_map f h1 h2 ϕ,
      comm' := by { intros i' j' hij,
                    by_cases h : ∃ i, f i = i',
                    { cases h with i hi,
                      by_cases h' : ∃ j, f j = j',
                      { cases h' with j hj,
                        rw homological_complex.map_grading_map_spec f h1 h2 ϕ i' i hi,
                        rw homological_complex.map_grading_map_spec f h1 h2 ϕ j' j hj,
                        delta homological_complex.map_grading_obj_id_or_zero_L,
                        delta homological_complex.map_grading_obj_id_or_zero_R,
                        dsimp [homological_complex.map_grading_obj],
                        split_ifs,
                        -- suffices : ∀ (h₁ : (homological_complex.map_grading_obj f h1 h2 C).X i' = C.X i)
                        --              (h₂ : C'.X i = (homological_complex.map_grading_obj f h1 h2 C').X i')
                        --              (h₃ : (homological_complex.map_grading_obj f h1 h2 C).X j' = C.X j)
                        --              (h₄ : C'.X j = (homological_complex.map_grading_obj f h1 h2 C').X j'),
                        --              (eq_to_hom h₁ ≫ ϕ.f i ≫ eq_to_hom h₂)
                        --              ≫ (homological_complex.map_grading_obj f h1 h2 C').d i' j' =
                        --             (homological_complex.map_grading_obj f h1 h2 C).d i' j'
                        --             ≫ eq_to_hom h₁ ≫ ϕ.f j ≫ eq_to_hom h₂
                         } }  }
    }
  }

end