homology.lean

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

open category_theory category_theory.limits

section

local attribute [instance] category_theory.limits.has_zero_object.has_zero

parameters {C : Type*} [category C] {R : Type*} [comm_ring R] 

instance zero_obj_subsingleton : subsingleton (0 : Module R) := 
  let f := is_zero.iso_zero (Module.is_zero_of_subsingleton (Module.of R punit))
  in ⟨λ a b, have h : f.hom (f.inv a) = f.hom (f.inv b),
             from congr_arg f.hom (subsingleton.elim (f.inv a) (f.inv b)),
             by { change (f.inv ≫ f.hom) a = (f.inv ≫ f.hom) b at h,
                  rw iso.inv_hom_id at h, exact h }⟩ 

def exists_preim_cycle_of_homology_zero {ι : Type*} {c : complex_shape ι}
                                 (C : homological_complex (Module R) c) (i j : ι)
                                 (hij : c.rel i j)
                                 (H : is_isomorphic (C.homology j) 0)
                                 (x : C.X j) (is_cycle : C.d_from j x = 0)
  : ∃ x_1 : C.X i, (C.d i j) x_1 = x :=
begin
  have : function.surjective (C.boundaries_to_cycles j),
  { have H' := H, 
    delta homological_complex.homology at H',
    delta homology at H',
    cases H',
    have := (Module.cokernel_iso_range_quotient _).symm.trans H',
    intro c,
    delta homological_complex.cycles at c,
    have is_zero : this.inv (this.hom (submodule.quotient.mk c_1))
                  = submodule.quotient.mk c_1,
    { transitivity (this.hom ≫ this.inv) (submodule.quotient.mk c_1), refl,
      have hom_iv_eq_id := this.hom_inv_id',
      dsimp at hom_iv_eq_id, rw hom_iv_eq_id, refl },
    rw (_ : this.hom (submodule.quotient.mk c_1) = 0) at is_zero,
    { simp at is_zero,
      symmetry' at is_zero,
      rw submodule.quotient.mk_eq_zero at is_zero,
      exact is_zero },
    { apply subsingleton.elim } },
  let x' := Module.to_cycles ⟨x, is_cycle⟩,
  cases (this x') with y' h,
  delta homological_complex.boundaries at y',
  delta image_subobject at y',
  destruct (Module.image_iso_range (C.d_to j)).hom
              ((image_subobject_iso (C.d_to j)).hom y'),
  intros y hy hy',
  let y'' : linear_map.ker (C.d_from j) := set.inclusion _ ⟨y, hy⟩,
  swap,
  { intros z hz, cases hz with z' hz, rw ← hz,
    change (C.d_to j ≫ C.d_from j) z' = 0, simp },
  cases hy with w hw,
  existsi (C.X_prev_iso hij).hom w,
  rw C.d_to_eq hij at hw,
  transitivity y, assumption,
  suffices : Module.to_cycles ⟨x, is_cycle⟩ = Module.to_cycles y'',
  { symmetry,
    replace this := congr_arg ⇑(kernel_subobject (C.d_from j)).arrow this,
    rw [Module.to_kernel_subobject_arrow, Module.to_kernel_subobject_arrow] at this,
    exact this },
  change (x' = Module.to_cycles y''),
  rw ← h,
  apply Module.cycles_ext,
  simp,
  have := congr_arg subtype.val hy',
  simp at this, 
  rw ← this,
  transitivity ((image_subobject_iso (C.d_to j)).hom
                ≫ (Module.image_iso_range (C.d_to j)).hom
                ≫ (submodule.subtype (linear_map.range (C.d_to j)))) y',
  { congr,
    rw (_ : (linear_map.range (C.d_to j)).subtype
          = Module.of_hom ((linear_map.range (C.d_to j)).subtype)),
    rw ← Module.image_iso_range_inv_image_ι (C.d_to j),
    rw ← category.assoc (iso.hom _) (iso.inv _) _,
    rw iso.hom_inv_id, simp, refl },
  refl
end

noncomputable
def preim_cycle_of_homology_zero {ι : Type*} {c : complex_shape ι}
                                 (C : homological_complex (Module R) c) (i j : ι)
                                 (hij : c.rel i j)
                                 (H : is_isomorphic (C.homology j) 0)
                                 (x : C.X j) (is_cycle : C.d_from j x = 0) : C.X i :=
@classical.some (C.X i) (λ y, C.d i j y = x)
                (exists_preim_cycle_of_homology_zero C i j hij H x is_cycle)

lemma preim_cycle_of_homology_zero_spec {ι : Type*} {c : complex_shape ι}
                                 (C : homological_complex (Module R) c) (i j : ι)
                                 (hij : c.rel i j)
                                 (H : is_isomorphic (C.homology j) 0)
                                 (x : C.X j) (is_cycle : C.d_from j x = 0)
  : C.d i j (preim_cycle_of_homology_zero C i j hij H x is_cycle) = x :=
@classical.some_spec (C.X i) (λ y, C.d i j y = x)
                     (exists_preim_cycle_of_homology_zero C i j hij H x is_cycle)
end