Commit 2025-04-28 17:33 3640ff59

View on Github →

chore(CategoryTheory): fix some Fintype/Finite assumptions (#24423) Found by the linter in #10235 Assume [Finite J] instead of [Fintype J] here and there. IMHO, the right way to fix this is to use Fin n in the typeclass definition, then use {J : Type*} [Finite J] in the instance, cf. CategoryTheory.Limits.PreservesFiniteCoproducts I didn't take that path, because I never used this part of the library, so

I failed to quickly prove equivalence between PreservesFiniteCoproducts given Equiv between domains;
my opinion about design choices has higher chances of being wrong.

Estimated changes

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

Modified Mathlib/CategoryTheory/Monoidal/Preadditive.lean

modified theorem CategoryTheory.biproduct_ι_comp_leftDistributor_hom

modified theorem CategoryTheory.biproduct_ι_comp_leftDistributor_inv

modified theorem CategoryTheory.biproduct_ι_comp_rightDistributor_hom

modified theorem CategoryTheory.biproduct_ι_comp_rightDistributor_inv

modified def CategoryTheory.leftDistributor

modified theorem CategoryTheory.leftDistributor_assoc

modified theorem CategoryTheory.leftDistributor_ext_left

modified theorem CategoryTheory.leftDistributor_ext_right

modified theorem CategoryTheory.leftDistributor_ext₂_left

modified theorem CategoryTheory.leftDistributor_ext₂_right

modified theorem CategoryTheory.leftDistributor_hom_comp_biproduct_π

modified theorem CategoryTheory.leftDistributor_inv_comp_biproduct_π

modified theorem CategoryTheory.leftDistributor_rightDistributor_assoc

modified def CategoryTheory.rightDistributor

modified theorem CategoryTheory.rightDistributor_assoc

modified theorem CategoryTheory.rightDistributor_ext_left

modified theorem CategoryTheory.rightDistributor_ext_right

modified theorem CategoryTheory.rightDistributor_ext₂_left

modified theorem CategoryTheory.rightDistributor_ext₂_right

modified theorem CategoryTheory.rightDistributor_hom_comp_biproduct_π

modified theorem CategoryTheory.rightDistributor_inv_comp_biproduct_π

Modified Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

Modified Mathlib/CategoryTheory/Preadditive/Biproducts.lean