Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-07-26 12:57
c4d273c2
View on Github →
feat(category_theory/limits): preserves biproducts if comparison is iso (
#14419
)
Estimated changes
Modified
src/category_theory/limits/preserves/shapes/biproducts.lean
added
def
category_theory.functor.biprod_comparison'
added
theorem
category_theory.functor.biprod_comparison'_comp_biprod_comparison
added
def
category_theory.functor.biprod_comparison
added
theorem
category_theory.functor.biprod_comparison_fst
added
theorem
category_theory.functor.biprod_comparison_snd
added
def
category_theory.functor.biproduct_comparison'
added
theorem
category_theory.functor.biproduct_comparison'_comp_biproduct_comparison
added
def
category_theory.functor.biproduct_comparison
added
theorem
category_theory.functor.biproduct_comparison_π
added
theorem
category_theory.functor.inl_biprod_comparison'
added
theorem
category_theory.functor.inr_biprod_comparison'
added
theorem
category_theory.functor.retraction_biprod_comparison'
added
theorem
category_theory.functor.retraction_biproduct_comparison'
added
theorem
category_theory.functor.section_biprod_comparison
added
theorem
category_theory.functor.section_biproduct_comparison
added
theorem
category_theory.functor.ι_biproduct_comparison'
added
def
category_theory.limits.preserves_binary_biproduct_of_epi_biprod_comparison'
added
def
category_theory.limits.preserves_binary_biproduct_of_mono_biprod_comparison
added
def
category_theory.limits.preserves_biproduct_of_epi_biproduct_comparison'
added
def
category_theory.limits.preserves_biproduct_of_mono_biproduct_comparison
Modified
src/category_theory/limits/shapes/biproducts.lean
modified
theorem
category_theory.limits.bicone.to_cocone_ι_app
added
theorem
category_theory.limits.bicone.to_cocone_ι_app_mk
modified
theorem
category_theory.limits.bicone.to_cone_π_app
added
theorem
category_theory.limits.bicone.to_cone_π_app_mk
added
def
category_theory.limits.biprod.iso_coprod
added
theorem
category_theory.limits.biprod.iso_coprod_inv
added
def
category_theory.limits.biprod.iso_prod
added
theorem
category_theory.limits.biprod.iso_prod_hom
added
theorem
category_theory.limits.biprod.iso_prod_inv
added
theorem
category_theory.limits.biprod_iso_coprod_hom
added
def
category_theory.limits.biproduct.iso_coproduct
added
theorem
category_theory.limits.biproduct.iso_coproduct_hom
added
theorem
category_theory.limits.biproduct.iso_coproduct_inv
added
def
category_theory.limits.biproduct.iso_product
added
theorem
category_theory.limits.biproduct.iso_product_hom
added
theorem
category_theory.limits.biproduct.iso_product_inv
Modified
src/category_theory/preadditive/additive_functor.lean