pushout of biprod.fst and biprod.snd is zero

Stream: maths

[Scott Morrison]

This is a maths question, where I'm hoping I'm missing an easier proof.

Say I have a biproduct of two objects X and Y, with projection maps biprod.fst : X ⊞ Y ⟶ X and biprod.snd : X ⊞ Y ⟶ Y, and inclusion maps biprod.inl and biprod.inr, satisfying the usual identities.

I want to say that the square formed by biprod.fst, biprod.snd, and the zero maps 0 : X ⟶ 0 and 0 : Y ⟶ 0 is a pushout square.

I was sure it was going to be easy, but ... the best I can come up with is:

The biproduct is also a coproduct, so we can compute pushout biprod.fst biprod.snd as coequalizer (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr), and then by assuming our category is preadditive, this is cokernel (biprod.fst ≫ biprod.inl - biprod.snd ≫ biprod.inr), but then that map is an involution (calculate!), so an isomorphism, so that cokernel is zero.

Any suggestions? Even just a compilation of this argument to one that avoids talking about coequalizers and cokernels would probably help. (Is it true without assuming preadditivity?)

[Adam Topaz]

If you have a square diagram with say Z instead of 0, then I think it suffices to show that the maps from A and B to Z are both zero. But by the commutativity of the diagram and properties of the biproduct, the map from A to Z should factor via the inclusion of A to the biproduct, followed by the projection to B then the map from B to Z, and this should be zero from the properties of the biproduct. I haven't written anything down, but I think(???) this works?

[Scott Morrison]

I don't see the "should factor" step in that argument.

[Adam Topaz]

That's because the incl of A into the biprod followed by the projection toA is the identity

[Adam Topaz]

So write the map from A to Z as the incl of A to the biprod, followed by proj to A followed by the map to Z, then use the commutativity of the square

[Adam Topaz]

(sorry for the bad typesetting... I'm on mobile)

[Scott Morrison]

Perfect, thank you. :-)

[Reid Barton]

$$\begin{CD} 0 @>>> A \\ @VVV @VVV\\ B @>>> A \oplus B @>>> B \\ @VVV @VVV @VVV\\ 0 @>>> A @>>> 0 \end{CD}$$

The top left square is a pushout by definition, and the two big rectangles are trivially pushouts, so by using pushout cancellation twice, so is the bottom right square.

[Scott Morrison]

Oh, now I want to formalise this one, precisely because our API for this style of argument is still missing.

[Scott Morrison]

Was some of this done in LTE?

[Johan Commelin]

I think Andrew set up this kind of API when doing pullbacks of schemes.

[Johan Commelin]

But I don't know if it was dualised to include pushouts.

[Scott Morrison]

docs#category_theory.limits.right_square_is_pushout

[Reid Barton]

I made some arguments like this one in lean-homotopy-theory, though it wasn't for the mathlib notion of pushout (which didn't yet exist). e.g. using https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/category_theory/pasting_pushouts.lean and https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/category_theory/colimit_lemmas.lean

[Scott Morrison]

How would everyone feel about migrating Reid's Is_pushout to mathlib?

[Scott Morrison]

(i.e. a prop-valued thing parameterised by four morphisms)

[Scott Morrison]

Maybe call it pushout_square instead? (To avoid another is_*)

[Scott Morrison]

It becomes yet-another-way to talk about limits, and therefor some additional API cost for glue

[Scott Morrison]

But it would still let us state Andrew's docs#category_theory.limits.right_square_is_pushout much more succinctly.

[Scott Morrison]

I noticed that LTE/for_mathlib has a is_biprod structure.

[Scott Morrison]

#14220

[Bhavik Mehta]

Yeah I think this is an excellent idea - I either made a poor version of it in the topos project or thought about doing it! I think it would definitely make this sort of argument easier to formalise

[Scott Morrison]

Should we call it cartesian rather than pullback_square? I think I prefer pullback_square, although then I don't know what to call bicartesian.

[Johan Commelin]

cartesian is shorter, and doesn't contain a _. So I would vote for that.

[Bhavik Mehta]

And then cocartesian for pushout_square? I slightly prefer pullback_square: cartesian is overloaded plenty, but I'd be happy either way

[Johan Commelin]

How about commsq.pullback?

[Johan Commelin]

In LTE I defined commsq. I think it's a useful shorthand, and it provides an anchor for dot-notation.

[Johan Commelin]

For h : commsq a b c d you get h.w and h.w_assoc, and of course h.symm.

[Bhavik Mehta]

That sounds sensible to me, although it kind of opens the door to commtri? (and its dual commcotri)! Also I suppose comm_sq would be better?

[Markus Himmel]

There is also the option of stating being a pullback square for morphisms in the arrow category, though I'm not sure how ergonomic that would be

[Reid Barton]

I assume commsq is a bundled commutative square; then how do you state the pushout pasting lemma?

[Johan Commelin]

No, it isn't bundled. a b c d are 4 morphisms.

[Reid Barton]

oh it's a Prop?

[Johan Commelin]

For technical reasons, no. But a Prop-version seems quite useful to me.

[Reid Barton]

Where is the definition?

[Johan Commelin]

In the salamander lemma, you need to consider the direct sum of the two objects on the antidiagonal. So I bundled that into the defn.

[Johan Commelin]

That way you can get commsq.op and commsq.symm with nice defeqs.

[Reid Barton]

OK, well normally two objects don't have a direct sum :upside_down:

[Johan Commelin]

It also assumed an ab cat :see_no_evil:

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/commsq.lean

[Johan Commelin]

But I think simply a Prop version could already be useful, and have a nice API.

[Johan Commelin]

My crazy contraption can have a different name (-;

[Reid Barton]

So the Prop version is just (w : g₁₁ ≫ f₂₁ = f₁₁ ≫ g₁₂)?

[Johan Commelin]

Yes

[Johan Commelin]

Se the of_eq constructor.

[Reid Barton]

I think this could be useful, then is_pushout and is_pullback can extend it

[Johan Commelin]

Maybe assume it, instead of extending?

[Johan Commelin]

Then you can write h.is_pushout

[Johan Commelin]

And sq1.hcomp sq2 (idem for .vcomp). That way the pasting lemmas would become quite nice, I think.

[Johan Commelin]

h.op.is_pullback \iff h.is_pushout etc...

[Reid Barton]

What do you mean "assume"?

[Johan Commelin]

As an explicit parameter

[Johan Commelin]

def commsq.is_pullback (h : commsq a b c d) : Prop := blabla

[Reid Barton]

Oh I see, but somehow it feels a bit more awkward because it suggests you would have to prove the square commutes, before talking about whether it is a pushout

[Reid Barton]

but I guess you have a style in mind where you don't actually do that

[Reid Barton]

i.e. in l-h-t you can just write Is_pushout f g h k, rather than \<show f >> g = h >> k, by assumption\>.is_pushout or whatever

[Reid Barton]

(ok if the proof is by assumption it's a bad example, but maybe it will be by simp etc)

[Johan Commelin]

Yeah, I see. I think both use cases are nice.

[Johan Commelin]

I have in mind statements like:

lemma pasting (h : sq1.is_pushout) :
  (sq1.hcomp sq2).is_pushout \iff sq2.is_pushout

[Johan Commelin]

Maybe the base for the dot-notation should be a law-less (but type correct) square?

[Johan Commelin]

And then you have sq.is_comm and sq.is_pullback can extend that?

[Reid Barton]

Johan Commelin said:

Maybe the base for the dot-notation should be a law-less (but type correct) square?

So this is just the proposition true?

[Reid Barton]

I think this might also be awkward in the goal view

[Reid Barton]

Also I'm not sure how well this works with rewriting along equalities of morphisms

[Johan Commelin]

What do you mean?

[Johan Commelin]

.w gives you back the actual equality condition

[Reid Barton]

e.g. if my goal is Is_pushout f g h k and I have H : f = f' I know how to rw H

[Reid Barton]

if my goal is (sq : anysq f g h k).is_pushout then I don't think I can rw H

[Johan Commelin]

Hmm, I see.

[Reid Barton]

(and that's quite a common thing to do, e.g., you need to do it several times in the proof that started this discussion)

[Scott Morrison]

I've added comm_sq, renamed pullback_square to is_pullback, and have it extend comm_sq. I added comm_sq.of_arrow, but no further API relating comm_sq to the arrow category as yet. I think this PR (#14220) is ready for review for now.

[Johan Commelin]

Why do you call the constructors mk' if you don't provide a mk? Or am I blind?

[Scott Morrison]

Not sure what happened there. Removed.

[Johan Commelin]

I just realized that I would really like to have functor.map_comm_sq :grinning:

[Scott Morrison]

#14351

[Scott Morrison]

(Also for functor.map_is_pullback etc)

[Scott Morrison]

The rest of Reid's argument is in #14375.

[Bhavik Mehta]

It would be nice to use this to refactor docs#category_theory.is_kernel_pair

[Bhavik Mehta]

in fact looking at that again, most of what I did in that file are (useful) special cases of comm_sq

[Scott Morrison]

One difference is that in is_pullback I wrapped is_limit in nonempty, so we have is_pullback : Prop. Do you think it would be okay to change kernel_pair like that?

[Bhavik Mehta]

Probably - it's subsingleton (not just up to iso) so I expect it should be fine