Commit 2023-03-07 17:18 b66eff51

View on Github →

feat: port CategoryTheory.Limits.Constructions.BinaryProducts (#2699)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.lean

added theorem hasBinaryCoproducts_of_hasInitial_and_pushouts

added theorem hasBinaryProducts_of_hasTerminal_and_pullbacks

added def isBinaryCoproductOfIsInitialIsPushout

added def isBinaryProductOfIsTerminalIsPullback

added def isCoproductOfIsInitialIsPushout

added def isProductOfIsTerminalIsPullback

added def isPullbackOfIsTerminalIsProduct

added def isPushoutOfIsInitialIsCoproduct

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean

modified def CategoryTheory.Limits.preservesPullbackSymmetry

modified def CategoryTheory.Limits.preservesPushoutSymmetry

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean