Commit 2023-11-12 13:54 63c34b16

View on Github →

refactor(CategoryTheory): change the API for opposite (co)products to accept general (co)fans (#8302)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

added def CategoryTheory.Limits.Cofan.IsColimit.op

added def CategoryTheory.Limits.Cofan.op

added def CategoryTheory.Limits.Fan.IsLimit.op

added def CategoryTheory.Limits.Fan.op

added theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom

modified theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct_hom

added def CategoryTheory.Limits.opCoproductIsoProduct'

added theorem CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj

modified def CategoryTheory.Limits.opCoproductIsoProduct

modified theorem CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι

added def CategoryTheory.Limits.opProductIsoCoproduct'

added theorem CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift

modified def CategoryTheory.Limits.opProductIsoCoproduct

added theorem CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_lift

deleted theorem CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_π_op

added theorem CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom

added theorem CategoryTheory.Limits.proj_comp_opProductIsoCoproduct_hom

deleted theorem CategoryTheory.Limits.π_comp_opProductIsoCoproduct