Translating Module.exact_iff to Ab

Stream: general

[Fabian Glöckle]

Hi, I am trying to prove the equivalent statement to docs#Module.exact_iff for AddCommGroup instead of Module, i.e.

theorem exact_iff {M N O : AddCommGroup.{v}} (f : M ⟶ N) (g : N ⟶ O): exact f g ↔ f.range = g.ker := sorry

If you can explain me why this isn't needed or how to do it with the forgetful functor from Module \Z, I'd be very grateful.
For now, I thought I'll have to translate the proof, which involves first getting the respective statements for docs#Module.kernel_cone, docs#Module.kernel_is_limit etc.
@Markus Himmel It seems you have written this for Module. What yould you recommend?

[Riccardo Brasca]

I would prove that an equivalences of categories preserves exactness (that it's relevant in its own). Then I suppose we know that the forgetful functor is an equivalence. But it's very possible there is a shorter way.

[Fabian Glöckle]

yes, we do know that

[Markus Himmel]

If you know that the forgetful functor preserves and reflects exact sequences then it should be easy

[Riccardo Brasca]

So this is a good reason to finish my review of #12071

[Fabian Glöckle]

uhh, nice!

[Riccardo Brasca]

So I really suggest to prove the general about equivalences of categories, and use it.

[Johan Commelin]

@Fabian Glöckle AddCommGroup.exact_iff is already in LTE.

[Fabian Glöckle]

ohh

[Fabian Glöckle]

wait, doesn't VSCode Ctrl-T search your own src/ as well?

[Johan Commelin]

Je ne sais pas. But I think you want

src/for_mathlib/AddCommGroup/exact.lean
12:theorem exact_iff : exact f g ↔ f.range = g.ker :=

[Fabian Glöckle]

yes yes I've found it

[Fabian Glöckle]

but I thought I had checked in advance what's there

[Fabian Glöckle]

so do you grep your repo to find lemmas others have written or do you all just have a very good overview over what's there?

[Fabian Glöckle]

and so you did rewrite the def kernel_is_limit : is_limit (kernel_cone f) :D

[Fabian Glöckle]

thank you a lot
that saved me a bunch of time!

[Johan Commelin]

Fabian Glöckle said:

so do you grep your repo to find lemmas others have written or do you all just have a very good overview over what's there?

both (-;

[Riccardo Brasca]

@Markus Himmel If you're happy with #12071 don't forget to merge it!