Commit 2026-10-10 13:11 26660f2b

View on Github →

feat(CategoryTheory): the external product of two Guitart exact squares is Guitart exact (#43895)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Adjunction/Mates.lean

Modified Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean

Modified Mathlib/CategoryTheory/Functor/TwoSquare.lean

deleted def CategoryTheory.TwoSquare.op

added def CategoryTheory.TwoSquare.prod

deleted def CategoryTheory.TwoSquare

Modified Mathlib/CategoryTheory/GuitartExact/Basic.lean

Modified Mathlib/CategoryTheory/GuitartExact/HorizontalComposition.lean

Modified Mathlib/CategoryTheory/GuitartExact/KanExtension.lean

Modified Mathlib/CategoryTheory/GuitartExact/Opposite.lean

Modified Mathlib/CategoryTheory/GuitartExact/Over.lean

Created Mathlib/CategoryTheory/GuitartExact/Prod.lean

added def CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.functor

added def CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.functorObj

added def CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.inverse

added def CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.inverseObj

added def CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence

Modified Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean

Modified Mathlib/CategoryTheory/Monoidal/Closed/Functor.lean