Jonas van de Schaaf - Projectivity of the sequence space

Stream: Lean Together 2026

[Jireh Loreaux]

Discussion thread for the talk.

[Kevin Buzzard]

@Jonas van der Schaaf do you understand why, of the two proofs you gave, the first one was so much longer? Are these really "different proofs" or is it the "same proof" but somehow the difference in lengths is the justification that the two proofs are the same?

[Jonas van der Schaaf]

Sorry for my late response, definitely the key "insight" (quotation marks because it is quite trivial) is definitely the same.

In one proof, I use fully faithfulness to prove that a certain map from the coproduct is the lift out of it and an isomorphism and hence that the target is also a coproduct. In the other, fully faithfulness is used to directly reflect a colimit cocone. The lemmas used after the fully faithful reduction use the exact same lemma under the hood, so they are (at least morally) pretty similar.

There are multiple reasons for the proofs having such different lengths. One of the proofs is _much_ more explicit, involves a commutative square that is actually made up of many maps between types which don't even live in the same universe, and uses an explicit description of categorical products of types for reasons I don't even remember.

While the same amount of data is involved in both proofs, the proof with cocones captures all the data in one structure which can be easily manipulated using the full force of all theorems in mathlib as well.