Commit 2026-09-30 10:34 0e51f706

View on Github →

feat(Algebra/Homology/ShortComplex): pullbacks and pushouts of short exact sequences (#44229) Given a short complex S and a morphism f : Y ⟶ S.X₃, this PR constructs the short complex S.pull f, namely S.X₁ ⟶ pullback f S.g ⟶ Y, and shows that it is short exact whenever S is, in an abelian category. Dually, for f : S.X₁ ⟶ Y it constructs S.push f, namely Y ⟶ pushout f S.f ⟶ S.X₃, and shows that it is short exact whenever S is. In Algebra/Homology/ShortComplex/Pullback.lean:

  • ShortComplex.pull, with instances Epi (S.pull f).g (abelian, S.g epi) and Mono (S.pull f).f (S.f mono);
  • ShortComplex.ShortExact.pull. In Algebra/Homology/ShortComplex/Pushout.lean:
  • ShortComplex.push, with instances Mono (S.push f).f (abelian, S.f mono) and Epi (S.push f).g (S.g epi);
  • ShortComplex.ShortExact.push. This replaces an earlier version phrased in terms of the Subobject API, following a suggestion of @joelriou, who wrote the pull construction. This PR was split from #36744.

Estimated changes