bicartesian squares

Stream: condensed mathematics

[Johan Commelin]

Here's a diagram chase (https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/bicartesian3.lean#L42):

lemma commsq.bicartesian_iff_isos : sqm.bicartesian ↔ (is_iso gKh ∧ is_iso gQh) :=
begin
  delta commsq.bicartesian,
  split,
  { intro h, split,
    { rw is_iso_iff_mono_and_epi, split,
      { rw [AddCommGroup.mono_iff_ker_eq_bot, eq_bot_iff], sorry },
      { sorry } },
    { sorry } },
  { sorry }
end

We only need this in Ab. So it can be done using actual elements. Let me know if you would like to work on this.

[Kevin Buzzard]

I'm looking for something to do, I could take this on.

[Markus Himmel]

I pushed a proof of the forward direction

[Yaël Dillies]

Now pull a proof in the backward direction.

[Kevin Buzzard]

Maybe a variant of to_additive could help with this?

[Johan Commelin]

This is cool. If we can also get the other direction done, then we can defer the 6 nasty sorries in salamander.lean to a later project.

[Johan Commelin]

@Markus Himmel so you didn't do a proof with elements, I see. Are you interested in doing the other direction as well?
I was otherwise thinking of just doing a chase using elements.

[Markus Himmel]

@Johan Commelin it depends on how quickly you need it. I could have a look on Saturday or Sunday. Is the proof (using elements) straightforward on paper?

[Johan Commelin]

With elements it's quite straightforward, yes.

[Johan Commelin]

If you want to go without elements, you could try to show again that you have a pullback-and-pushout, because the isos guarantee that the fibers at 0 are isomorphic so you have a pullback by "homogeneity" (dualise for pushout).

[Johan Commelin]

But the "homogeneity" is much easier using elements, I guess.

[Markus Himmel]

Okay, I'll try to formalize it during the weekend if no one beats me to it

[Johan Commelin]

Thanks!

[Markus Himmel]

commsq.bicartesian_iff_isos is now done.