Commit 2023-08-24 09:53 75e30432

View on Github →

feat: some lemmas about products and coproducts in opposite categories (#6758)

Adds missing theorem hasColimit_op_of_hasLimit and its dual.
Adds instance [HasCoproduct Z] : HasProduct (fun z ↦ op (Z z)) and its dual
Defines the isomorphism op (∐ Z) ≅ ∏ (fun z => op (Z z)) and its dual and proves some naturality lemmas about them.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

added theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct_hom

added theorem CategoryTheory.Limits.hasColimit_op_of_hasLimit

added theorem CategoryTheory.Limits.hasLimit_op_of_hasColimit

added def CategoryTheory.Limits.opCoproductIsoProduct

added theorem CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι

added def CategoryTheory.Limits.opProductIsoCoproduct

added theorem CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_π_op

added theorem CategoryTheory.Limits.π_comp_opProductIsoCoproduct