split_exact

Stream: condensed mathematics

[Scott Morrison]

I did some cleanup of for_mathlib/split_exact.lean, in the hope of actually, you know, putting it in mathlib. :-) Mostly it is was already in great shape. However there is a TODO that I don't understand:

-- TODO: this should be generalized to isoms of short sequences,
-- because now it forces one direction, and we want both.

Could someone explain this to me?'

[Johan Commelin]

@Scott Morrison I think the point is that instead of a map i : B \hom A \b+ C you could also have a map A \b+ C \hom B instead.

[Scott Morrison]

But how do "isoms of short sequences" come into it?

[Johan Commelin]

Not so sure what I was thinking when I wrote that comment.

[Johan Commelin]

Maybe what I really meant is that we should also have the "dual" constructor.

[Johan Commelin]

Ooh, maybe if you have a f' g' and some isomorphisms, then you get short_exact f g \iff short_exact f' g'. Maybe I was thinking of that statement.

[Scott Morrison]

I PR'd short_exact as #14009. Reviews/merges welcome. :-)

[Scott Morrison]

Maybe I'll aim at for_mathlib/exact_seq.lean when I want to do more for_mathlibbing. That one looks close to ready.