homology in Ab

Stream: condensed mathematics

[Johan Commelin]

Here's a stupid little lemma that we'll need

-- somewhere in `src/system_of_complexes/shift_sub_id.lean`
lemma _root_.category_theory.homology.π_eq_zero
  {A B C : Ab} {f : A ⟶ B} {g : B ⟶ C} (w : f ≫ g = 0) (x)
  (h : ∃ a : A, f a = (kernel_subobject g).arrow x) :
  homology.π f g w x = 0 :=
begin
  rcases h with ⟨a, ha⟩,
  sorry
end

[Johan Commelin]

It's a bit annoying, since homology is defined using category theory, and so it's not defeq to a group quotient.

[Scott Morrison]

This is probably easier in Module where there is as bit more API. I'd try it there first then port to Ab. I think I have an old branch that does similar things, I'll try to recover it.

[Johan Commelin]

Ooh, I just remembered that we have

protected noncomputable
def AddCommGroup.homology_iso {A B C : AddCommGroup.{u}} (f : A ⟶ B) (g : B ⟶ C) (w : f ≫ g = 0) :
  homology f g w ≅ AddCommGroup.of (g.ker ⧸ (f.range.comap g.ker.subtype)) :=

in derived/example.lean