Commit 2025-02-25 07:12 86a0f010

View on Github →

chore: split long file CategoryTheory.Limits.Shapes.Biproducts (#22258)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Biproducts.lean

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

Created Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean

added def CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor

added def CategoryTheory.Limits.Bicone.toBinaryBiconeIsBilimit

added def CategoryTheory.Limits.Bicone.toBinaryBiconeIsColimit

added def CategoryTheory.Limits.Bicone.toBinaryBiconeIsLimit

added structure CategoryTheory.Limits.BinaryBicone.IsBilimit

added theorem CategoryTheory.Limits.BinaryBicone.binary_cofan_inl_toCocone

added theorem CategoryTheory.Limits.BinaryBicone.binary_cofan_inr_toCocone

added theorem CategoryTheory.Limits.BinaryBicone.binary_fan_fst_toCone

added theorem CategoryTheory.Limits.BinaryBicone.binary_fan_snd_toCone

added def CategoryTheory.Limits.BinaryBicone.fstKernelFork

added theorem CategoryTheory.Limits.BinaryBicone.fstKernelFork_ι

added def CategoryTheory.Limits.BinaryBicone.inlCokernelCofork

added theorem CategoryTheory.Limits.BinaryBicone.inlCokernelCofork_π

added def CategoryTheory.Limits.BinaryBicone.inrCokernelCofork

added theorem CategoryTheory.Limits.BinaryBicone.inrCokernelCofork_π

added def CategoryTheory.Limits.BinaryBicone.isColimitInlCokernelCofork

added def CategoryTheory.Limits.BinaryBicone.isColimitInrCokernelCofork

added def CategoryTheory.Limits.BinaryBicone.isLimitFstKernelFork

added def CategoryTheory.Limits.BinaryBicone.isLimitSndKernelFork

added def CategoryTheory.Limits.BinaryBicone.sndKernelFork

added theorem CategoryTheory.Limits.BinaryBicone.sndKernelFork_ι

added def CategoryTheory.Limits.BinaryBicone.toBiconeFunctor

added def CategoryTheory.Limits.BinaryBicone.toBiconeIsBilimit

added def CategoryTheory.Limits.BinaryBicone.toBiconeIsColimit

added def CategoryTheory.Limits.BinaryBicone.toBiconeIsLimit

added def CategoryTheory.Limits.BinaryBicone.toCocone

added theorem CategoryTheory.Limits.BinaryBicone.toCocone_pt

added theorem CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_left

added theorem CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_right

added def CategoryTheory.Limits.BinaryBicone.toCone

added theorem CategoryTheory.Limits.BinaryBicone.toCone_pt

added theorem CategoryTheory.Limits.BinaryBicone.toCone_π_app_left

added theorem CategoryTheory.Limits.BinaryBicone.toCone_π_app_right

added structure CategoryTheory.Limits.BinaryBicone

added theorem CategoryTheory.Limits.BinaryBiconeMorphism.ext

added structure CategoryTheory.Limits.BinaryBiconeMorphism

added def CategoryTheory.Limits.BinaryBicones.ext

added def CategoryTheory.Limits.BinaryBicones.functoriality

added def CategoryTheory.Limits.BinaryBiproduct.bicone

added theorem CategoryTheory.Limits.BinaryBiproduct.bicone_fst

added theorem CategoryTheory.Limits.BinaryBiproduct.bicone_inl

added theorem CategoryTheory.Limits.BinaryBiproduct.bicone_inr

added theorem CategoryTheory.Limits.BinaryBiproduct.bicone_snd

added def CategoryTheory.Limits.BinaryBiproduct.isBilimit

added def CategoryTheory.Limits.BinaryBiproduct.isColimit

added def CategoryTheory.Limits.BinaryBiproduct.isLimit

added structure CategoryTheory.Limits.BinaryBiproductData

added theorem CategoryTheory.Limits.HasBinaryBiproduct.mk

added def CategoryTheory.Limits.Indecomposable

added def CategoryTheory.Limits.biprod.associator

added theorem CategoryTheory.Limits.biprod.associator_inv_natural

added theorem CategoryTheory.Limits.biprod.associator_natural

added theorem CategoryTheory.Limits.biprod.braid_natural

added def CategoryTheory.Limits.biprod.braiding'

added theorem CategoryTheory.Limits.biprod.braiding'_eq_braiding

added def CategoryTheory.Limits.biprod.braiding

added theorem CategoryTheory.Limits.biprod.braiding_map_braiding

added theorem CategoryTheory.Limits.biprod.conePointUniqueUpToIso_hom

added theorem CategoryTheory.Limits.biprod.conePointUniqueUpToIso_inv

added def CategoryTheory.Limits.biprod.fstKernelFork

added theorem CategoryTheory.Limits.biprod.fstKernelFork_ι

added theorem CategoryTheory.Limits.biprod.hom_ext'

added theorem CategoryTheory.Limits.biprod.hom_ext

added def CategoryTheory.Limits.biprod.inlCokernelCofork

added theorem CategoryTheory.Limits.biprod.inlCokernelCofork_π

added theorem CategoryTheory.Limits.biprod.inl_desc

added theorem CategoryTheory.Limits.biprod.inl_fst

added theorem CategoryTheory.Limits.biprod.inl_map

added theorem CategoryTheory.Limits.biprod.inl_snd

added def CategoryTheory.Limits.biprod.inrCokernelCofork

added theorem CategoryTheory.Limits.biprod.inrCokernelCofork_π

added theorem CategoryTheory.Limits.biprod.inr_desc

added theorem CategoryTheory.Limits.biprod.inr_fst

added theorem CategoryTheory.Limits.biprod.inr_map

added theorem CategoryTheory.Limits.biprod.inr_snd

added def CategoryTheory.Limits.biprod.isCokernelInlCokernelFork

added def CategoryTheory.Limits.biprod.isCokernelInrCokernelFork

added theorem CategoryTheory.Limits.biprod.isIso_inl_iff_id_eq_fst_comp_inl

added def CategoryTheory.Limits.biprod.isKernelFstKernelFork

added def CategoryTheory.Limits.biprod.isKernelSndKernelFork

added def CategoryTheory.Limits.biprod.isoCoprod

added theorem CategoryTheory.Limits.biprod.isoCoprod_inv

added def CategoryTheory.Limits.biprod.isoProd

added theorem CategoryTheory.Limits.biprod.isoProd_hom

added theorem CategoryTheory.Limits.biprod.isoProd_inv

added theorem CategoryTheory.Limits.biprod.lift_fst

added theorem CategoryTheory.Limits.biprod.lift_snd

added def CategoryTheory.Limits.biprod.mapIso

added theorem CategoryTheory.Limits.biprod.map_eq_map'

added theorem CategoryTheory.Limits.biprod.map_fst

added theorem CategoryTheory.Limits.biprod.map_snd

added def CategoryTheory.Limits.biprod.sndKernelFork

added theorem CategoryTheory.Limits.biprod.sndKernelFork_ι

added theorem CategoryTheory.Limits.biprod.symmetry'

added theorem CategoryTheory.Limits.biprod.symmetry

added def CategoryTheory.Limits.biprod.uniqueUpToIso

added def CategoryTheory.Limits.biprodIso

added theorem CategoryTheory.Limits.biprod_isZero_iff

added theorem CategoryTheory.Limits.biprod_isoCoprod_hom

added def CategoryTheory.Limits.cokernelBiprodInlIso

added def CategoryTheory.Limits.cokernelBiprodInrIso

added def CategoryTheory.Limits.getBinaryBiproductData

added theorem CategoryTheory.Limits.hasBinaryBiproducts_of_finite_biproducts

added theorem CategoryTheory.Limits.isIso_left_of_isIso_biprod_map

added theorem CategoryTheory.Limits.isIso_right_of_isIso_biprod_map

added def CategoryTheory.Limits.isoBiprodZero

added def CategoryTheory.Limits.isoZeroBiprod

added def CategoryTheory.Limits.kernelBiprodFstIso

added def CategoryTheory.Limits.kernelBiprodSndIso

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

deleted def CategoryTheory.Indecomposable

deleted def CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor

deleted def CategoryTheory.Limits.Bicone.toBinaryBiconeIsBilimit

deleted def CategoryTheory.Limits.Bicone.toBinaryBiconeIsColimit

deleted def CategoryTheory.Limits.Bicone.toBinaryBiconeIsLimit

modified theorem CategoryTheory.Limits.Bicone.toCocone_inj

modified theorem CategoryTheory.Limits.Bicone.toCocone_pt

modified theorem CategoryTheory.Limits.Bicone.toCone_proj

modified theorem CategoryTheory.Limits.Bicone.toCone_pt

modified theorem CategoryTheory.Limits.Bicone.toCone_π_app

deleted structure CategoryTheory.Limits.BinaryBicone.IsBilimit

deleted theorem CategoryTheory.Limits.BinaryBicone.binary_cofan_inl_toCocone

deleted theorem CategoryTheory.Limits.BinaryBicone.binary_cofan_inr_toCocone

deleted theorem CategoryTheory.Limits.BinaryBicone.binary_fan_fst_toCone

deleted theorem CategoryTheory.Limits.BinaryBicone.binary_fan_snd_toCone

deleted def CategoryTheory.Limits.BinaryBicone.fstKernelFork

deleted theorem CategoryTheory.Limits.BinaryBicone.fstKernelFork_ι

deleted def CategoryTheory.Limits.BinaryBicone.inlCokernelCofork

deleted theorem CategoryTheory.Limits.BinaryBicone.inlCokernelCofork_π

deleted def CategoryTheory.Limits.BinaryBicone.inrCokernelCofork

deleted theorem CategoryTheory.Limits.BinaryBicone.inrCokernelCofork_π

deleted def CategoryTheory.Limits.BinaryBicone.isColimitInlCokernelCofork

deleted def CategoryTheory.Limits.BinaryBicone.isColimitInrCokernelCofork

deleted def CategoryTheory.Limits.BinaryBicone.isLimitFstKernelFork

deleted def CategoryTheory.Limits.BinaryBicone.isLimitSndKernelFork

deleted def CategoryTheory.Limits.BinaryBicone.sndKernelFork

deleted theorem CategoryTheory.Limits.BinaryBicone.sndKernelFork_ι

deleted def CategoryTheory.Limits.BinaryBicone.toBiconeFunctor

deleted def CategoryTheory.Limits.BinaryBicone.toBiconeIsBilimit

deleted def CategoryTheory.Limits.BinaryBicone.toBiconeIsColimit

deleted def CategoryTheory.Limits.BinaryBicone.toBiconeIsLimit

deleted def CategoryTheory.Limits.BinaryBicone.toCocone

deleted theorem CategoryTheory.Limits.BinaryBicone.toCocone_pt

deleted theorem CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_left

deleted theorem CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_right

deleted def CategoryTheory.Limits.BinaryBicone.toCone

deleted theorem CategoryTheory.Limits.BinaryBicone.toCone_pt

deleted theorem CategoryTheory.Limits.BinaryBicone.toCone_π_app_left

deleted theorem CategoryTheory.Limits.BinaryBicone.toCone_π_app_right

deleted structure CategoryTheory.Limits.BinaryBicone

deleted theorem CategoryTheory.Limits.BinaryBiconeMorphism.ext

deleted structure CategoryTheory.Limits.BinaryBiconeMorphism

deleted def CategoryTheory.Limits.BinaryBicones.ext

deleted def CategoryTheory.Limits.BinaryBicones.functoriality

deleted def CategoryTheory.Limits.BinaryBiproduct.bicone

deleted theorem CategoryTheory.Limits.BinaryBiproduct.bicone_fst

deleted theorem CategoryTheory.Limits.BinaryBiproduct.bicone_inl

deleted theorem CategoryTheory.Limits.BinaryBiproduct.bicone_inr

deleted theorem CategoryTheory.Limits.BinaryBiproduct.bicone_snd

deleted def CategoryTheory.Limits.BinaryBiproduct.isBilimit

deleted def CategoryTheory.Limits.BinaryBiproduct.isColimit

deleted def CategoryTheory.Limits.BinaryBiproduct.isLimit

deleted structure CategoryTheory.Limits.BinaryBiproductData

deleted theorem CategoryTheory.Limits.HasBinaryBiproduct.mk

deleted def CategoryTheory.Limits.biprod.associator

deleted theorem CategoryTheory.Limits.biprod.associator_inv_natural

deleted theorem CategoryTheory.Limits.biprod.associator_natural

deleted theorem CategoryTheory.Limits.biprod.braid_natural

deleted def CategoryTheory.Limits.biprod.braiding'

deleted theorem CategoryTheory.Limits.biprod.braiding'_eq_braiding

deleted def CategoryTheory.Limits.biprod.braiding

deleted theorem CategoryTheory.Limits.biprod.braiding_map_braiding

deleted theorem CategoryTheory.Limits.biprod.conePointUniqueUpToIso_hom

deleted theorem CategoryTheory.Limits.biprod.conePointUniqueUpToIso_inv

deleted def CategoryTheory.Limits.biprod.fstKernelFork

deleted theorem CategoryTheory.Limits.biprod.fstKernelFork_ι

deleted theorem CategoryTheory.Limits.biprod.hom_ext'

deleted theorem CategoryTheory.Limits.biprod.hom_ext

deleted def CategoryTheory.Limits.biprod.inlCokernelCofork

deleted theorem CategoryTheory.Limits.biprod.inlCokernelCofork_π

deleted theorem CategoryTheory.Limits.biprod.inl_desc

deleted theorem CategoryTheory.Limits.biprod.inl_fst

deleted theorem CategoryTheory.Limits.biprod.inl_map

deleted theorem CategoryTheory.Limits.biprod.inl_snd

deleted def CategoryTheory.Limits.biprod.inrCokernelCofork

deleted theorem CategoryTheory.Limits.biprod.inrCokernelCofork_π

deleted theorem CategoryTheory.Limits.biprod.inr_desc

deleted theorem CategoryTheory.Limits.biprod.inr_fst

deleted theorem CategoryTheory.Limits.biprod.inr_map

deleted theorem CategoryTheory.Limits.biprod.inr_snd

deleted def CategoryTheory.Limits.biprod.isCokernelInlCokernelFork

deleted def CategoryTheory.Limits.biprod.isCokernelInrCokernelFork

deleted theorem CategoryTheory.Limits.biprod.isIso_inl_iff_id_eq_fst_comp_inl

deleted def CategoryTheory.Limits.biprod.isKernelFstKernelFork

deleted def CategoryTheory.Limits.biprod.isKernelSndKernelFork

deleted def CategoryTheory.Limits.biprod.isoCoprod

deleted theorem CategoryTheory.Limits.biprod.isoCoprod_inv

deleted def CategoryTheory.Limits.biprod.isoProd

deleted theorem CategoryTheory.Limits.biprod.isoProd_hom

deleted theorem CategoryTheory.Limits.biprod.isoProd_inv

deleted theorem CategoryTheory.Limits.biprod.lift_fst

deleted theorem CategoryTheory.Limits.biprod.lift_snd

deleted def CategoryTheory.Limits.biprod.mapIso

deleted theorem CategoryTheory.Limits.biprod.map_eq_map'

deleted theorem CategoryTheory.Limits.biprod.map_fst

deleted theorem CategoryTheory.Limits.biprod.map_snd

deleted def CategoryTheory.Limits.biprod.sndKernelFork

deleted theorem CategoryTheory.Limits.biprod.sndKernelFork_ι

deleted theorem CategoryTheory.Limits.biprod.symmetry'

deleted theorem CategoryTheory.Limits.biprod.symmetry

deleted def CategoryTheory.Limits.biprod.uniqueUpToIso

deleted def CategoryTheory.Limits.biprodIso

deleted theorem CategoryTheory.Limits.biprod_isZero_iff

deleted theorem CategoryTheory.Limits.biprod_isoCoprod_hom

deleted def CategoryTheory.Limits.cokernelBiprodInlIso

deleted def CategoryTheory.Limits.cokernelBiprodInrIso

deleted def CategoryTheory.Limits.getBinaryBiproductData

deleted theorem CategoryTheory.Limits.hasBinaryBiproducts_of_finite_biproducts

deleted def CategoryTheory.Limits.isoBiprodZero

deleted def CategoryTheory.Limits.isoZeroBiprod

deleted def CategoryTheory.Limits.kernelBiprodFstIso

deleted def CategoryTheory.Limits.kernelBiprodSndIso

deleted theorem CategoryTheory.isIso_left_of_isIso_biprod_map

deleted theorem CategoryTheory.isIso_right_of_isIso_biprod_map

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean

Modified Mathlib/CategoryTheory/Preadditive/Biproducts.lean

Modified Mathlib/CategoryTheory/Preadditive/Mat.lean

Modified Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean

Modified Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean

Modified Mathlib/CategoryTheory/Triangulated/Basic.lean