Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-13 15:02 234ddfea

View on Github →

chore(category_theory): put biproduct results on preadditive categories into the correct file (#16924)

Estimated changes

Modified src/algebra/category/Group/biproducts.lean

Modified src/category_theory/abelian/basic.lean

Modified src/category_theory/limits/preserves/shapes/biproducts.lean

deleted def category_theory.limits.preserves_binary_biproduct_of_epi_biprod_comparison'

deleted def category_theory.limits.preserves_binary_biproduct_of_mono_biprod_comparison

deleted def category_theory.limits.preserves_binary_biproduct_of_preserves_binary_coproduct

deleted def category_theory.limits.preserves_binary_biproduct_of_preserves_binary_product

deleted def category_theory.limits.preserves_binary_biproducts_of_preserves_binary_coproducts

deleted def category_theory.limits.preserves_binary_biproducts_of_preserves_binary_products

deleted def category_theory.limits.preserves_binary_coproduct_of_preserves_binary_biproduct

deleted def category_theory.limits.preserves_binary_coproducts_of_preserves_binary_biproducts

deleted def category_theory.limits.preserves_binary_product_of_preserves_binary_biproduct

deleted def category_theory.limits.preserves_binary_products_of_preserves_binary_biproducts

deleted def category_theory.limits.preserves_biproduct_of_epi_biproduct_comparison'

deleted def category_theory.limits.preserves_biproduct_of_mono_biproduct_comparison

deleted def category_theory.limits.preserves_biproduct_of_preserves_coproduct

deleted def category_theory.limits.preserves_biproduct_of_preserves_product

deleted def category_theory.limits.preserves_biproducts_of_shape_of_preserves_coproducts_of_shape

deleted def category_theory.limits.preserves_biproducts_of_shape_of_preserves_products_of_shape

deleted def category_theory.limits.preserves_coproduct_of_preserves_biproduct

deleted def category_theory.limits.preserves_coproducts_of_shape_of_preserves_biproducts_of_shape

deleted def category_theory.limits.preserves_product_of_preserves_biproduct

deleted def category_theory.limits.preserves_products_of_shape_of_preserves_biproducts_of_shape

Modified src/category_theory/limits/shapes/biproducts.lean

added theorem category_theory.is_iso_left_of_is_iso_biprod_map

added theorem category_theory.is_iso_right_of_is_iso_biprod_map

deleted def category_theory.limits.bicone_is_bilimit_of_colimit_cocone_of_is_colimit

deleted def category_theory.limits.bicone_is_bilimit_of_limit_cone_of_is_limit

deleted def category_theory.limits.binary_bicone.is_bilimit_of_cokernel_fst

deleted def category_theory.limits.binary_bicone.is_bilimit_of_cokernel_snd

deleted def category_theory.limits.binary_bicone.is_bilimit_of_kernel_inl

deleted def category_theory.limits.binary_bicone.is_bilimit_of_kernel_inr

deleted def category_theory.limits.binary_bicone.of_colimit_cocone

deleted def category_theory.limits.binary_bicone.of_limit_cone

deleted def category_theory.limits.binary_bicone_is_bilimit_of_colimit_cocone_of_is_colimit

deleted def category_theory.limits.binary_bicone_is_bilimit_of_limit_cone_of_is_limit

deleted def category_theory.limits.binary_bicone_of_is_split_epi_of_kernel

deleted def category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel

deleted theorem category_theory.limits.biprod.add_eq_lift_desc_id

deleted theorem category_theory.limits.biprod.add_eq_lift_id_desc

deleted theorem category_theory.limits.biprod.desc_eq

modified theorem category_theory.limits.biprod.is_iso_inl_iff_id_eq_fst_comp_inl

deleted theorem category_theory.limits.biprod.lift_desc

deleted theorem category_theory.limits.biprod.lift_eq

deleted theorem category_theory.limits.biprod.map_eq

deleted theorem category_theory.limits.biprod.total

deleted theorem category_theory.limits.biproduct.desc_eq

deleted theorem category_theory.limits.biproduct.lift_desc

deleted theorem category_theory.limits.biproduct.lift_eq

deleted theorem category_theory.limits.biproduct.lift_matrix

deleted theorem category_theory.limits.biproduct.map_eq

deleted theorem category_theory.limits.biproduct.map_matrix

deleted theorem category_theory.limits.biproduct.matrix_desc

deleted theorem category_theory.limits.biproduct.matrix_map

deleted def category_theory.limits.biproduct.reindex

deleted theorem category_theory.limits.biproduct.total

deleted theorem category_theory.limits.fst_of_is_colimit

deleted theorem category_theory.limits.has_binary_biproduct.of_has_binary_coproduct

deleted theorem category_theory.limits.has_binary_biproduct.of_has_binary_product

deleted theorem category_theory.limits.has_binary_biproduct_of_total

deleted theorem category_theory.limits.has_binary_biproducts.of_has_binary_coproducts

deleted theorem category_theory.limits.has_binary_biproducts.of_has_binary_products

deleted theorem category_theory.limits.has_biproduct.of_has_coproduct

deleted theorem category_theory.limits.has_biproduct.of_has_product

deleted theorem category_theory.limits.has_biproduct_of_total

deleted theorem category_theory.limits.has_finite_biproducts.of_has_finite_coproducts

deleted theorem category_theory.limits.has_finite_biproducts.of_has_finite_products

deleted theorem category_theory.limits.inl_of_is_limit

deleted theorem category_theory.limits.inr_of_is_limit

deleted theorem category_theory.limits.is_bilimit.binary_total

deleted theorem category_theory.limits.is_bilimit.total

deleted def category_theory.limits.is_bilimit_binary_bicone_of_is_split_epi_of_kernel

deleted def category_theory.limits.is_bilimit_binary_bicone_of_is_split_mono_of_cokernel

deleted def category_theory.limits.is_bilimit_of_is_colimit

deleted def category_theory.limits.is_bilimit_of_is_limit

deleted def category_theory.limits.is_bilimit_of_total

deleted def category_theory.limits.is_binary_bilimit_of_is_colimit

deleted def category_theory.limits.is_binary_bilimit_of_is_limit

deleted def category_theory.limits.is_binary_bilimit_of_total

deleted theorem category_theory.limits.snd_of_is_colimit

Modified src/category_theory/preadditive/additive_functor.lean

Modified src/category_theory/preadditive/biproducts.lean

deleted theorem category_theory.is_iso_left_of_is_iso_biprod_map

deleted theorem category_theory.is_iso_right_of_is_iso_biprod_map

added def category_theory.limits.bicone_is_bilimit_of_colimit_cocone_of_is_colimit

added def category_theory.limits.bicone_is_bilimit_of_limit_cone_of_is_limit

added def category_theory.limits.binary_bicone.is_bilimit_of_cokernel_fst

added def category_theory.limits.binary_bicone.is_bilimit_of_cokernel_snd

added def category_theory.limits.binary_bicone.is_bilimit_of_kernel_inl

added def category_theory.limits.binary_bicone.is_bilimit_of_kernel_inr

added def category_theory.limits.binary_bicone.of_colimit_cocone

added def category_theory.limits.binary_bicone.of_limit_cone

added def category_theory.limits.binary_bicone_is_bilimit_of_colimit_cocone_of_is_colimit

added def category_theory.limits.binary_bicone_is_bilimit_of_limit_cone_of_is_limit

added def category_theory.limits.binary_bicone_of_is_split_epi_of_kernel

added def category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel

added theorem category_theory.limits.biprod.add_eq_lift_desc_id

added theorem category_theory.limits.biprod.add_eq_lift_id_desc

added theorem category_theory.limits.biprod.desc_eq

added theorem category_theory.limits.biprod.lift_desc

added theorem category_theory.limits.biprod.lift_eq

added theorem category_theory.limits.biprod.map_eq

added theorem category_theory.limits.biprod.total

added theorem category_theory.limits.biproduct.desc_eq

added theorem category_theory.limits.biproduct.lift_desc

added theorem category_theory.limits.biproduct.lift_eq

added theorem category_theory.limits.biproduct.lift_matrix

added theorem category_theory.limits.biproduct.map_eq

added theorem category_theory.limits.biproduct.map_matrix

added theorem category_theory.limits.biproduct.matrix_desc

added theorem category_theory.limits.biproduct.matrix_map

added def category_theory.limits.biproduct.reindex

added theorem category_theory.limits.biproduct.total

added theorem category_theory.limits.fst_of_is_colimit

added theorem category_theory.limits.has_binary_biproduct.of_has_binary_coproduct

added theorem category_theory.limits.has_binary_biproduct.of_has_binary_product

added theorem category_theory.limits.has_binary_biproduct_of_total

added theorem category_theory.limits.has_binary_biproducts.of_has_binary_coproducts

added theorem category_theory.limits.has_binary_biproducts.of_has_binary_products

added theorem category_theory.limits.has_biproduct.of_has_coproduct

added theorem category_theory.limits.has_biproduct.of_has_product

added theorem category_theory.limits.has_biproduct_of_total

added theorem category_theory.limits.has_finite_biproducts.of_has_finite_coproducts

added theorem category_theory.limits.has_finite_biproducts.of_has_finite_products

added theorem category_theory.limits.inl_of_is_limit

added theorem category_theory.limits.inr_of_is_limit

added theorem category_theory.limits.is_bilimit.binary_total

added theorem category_theory.limits.is_bilimit.total

added def category_theory.limits.is_bilimit_binary_bicone_of_is_split_epi_of_kernel

added def category_theory.limits.is_bilimit_binary_bicone_of_is_split_mono_of_cokernel

added def category_theory.limits.is_bilimit_of_is_colimit

added def category_theory.limits.is_bilimit_of_is_limit

added def category_theory.limits.is_bilimit_of_total

added def category_theory.limits.is_binary_bilimit_of_is_colimit

added def category_theory.limits.is_binary_bilimit_of_is_limit

added def category_theory.limits.is_binary_bilimit_of_total

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_binary_biproduct_of_preserves_binary_coproduct

added def category_theory.limits.preserves_binary_biproduct_of_preserves_binary_product

added def category_theory.limits.preserves_binary_biproducts_of_preserves_binary_coproducts

added def category_theory.limits.preserves_binary_biproducts_of_preserves_binary_products

added def category_theory.limits.preserves_binary_coproduct_of_preserves_binary_biproduct

added def category_theory.limits.preserves_binary_coproducts_of_preserves_binary_biproducts

added def category_theory.limits.preserves_binary_product_of_preserves_binary_biproduct

added def category_theory.limits.preserves_binary_products_of_preserves_binary_biproducts

added def category_theory.limits.preserves_biproduct_of_epi_biproduct_comparison'

added def category_theory.limits.preserves_biproduct_of_mono_biproduct_comparison

added def category_theory.limits.preserves_biproduct_of_preserves_coproduct

added def category_theory.limits.preserves_biproduct_of_preserves_product

added def category_theory.limits.preserves_biproducts_of_shape_of_preserves_coproducts_of_shape

added def category_theory.limits.preserves_biproducts_of_shape_of_preserves_products_of_shape

added def category_theory.limits.preserves_coproduct_of_preserves_biproduct

added def category_theory.limits.preserves_coproducts_of_shape_of_preserves_biproducts_of_shape

added def category_theory.limits.preserves_product_of_preserves_biproduct

added def category_theory.limits.preserves_products_of_shape_of_preserves_biproducts_of_shape

added theorem category_theory.limits.snd_of_is_colimit

Modified src/category_theory/preadditive/hom_orthogonal.lean