Commit 2023-03-08 18:05 2b36d194

View on Github →

feat: port CategoryTheory.Limits.Shapes/Biproducts (#2710)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Indecomposable

added structure CategoryTheory.Limits.Bicone.IsBilimit

added def CategoryTheory.Limits.Bicone.ofColimitCocone

added def CategoryTheory.Limits.Bicone.ofLimitCone

added def CategoryTheory.Limits.Bicone.toBinaryBicone

added def CategoryTheory.Limits.Bicone.toBinaryBiconeIsBilimit

added def CategoryTheory.Limits.Bicone.toBinaryBiconeIsColimit

added def CategoryTheory.Limits.Bicone.toBinaryBiconeIsLimit

added def CategoryTheory.Limits.Bicone.toCocone

added theorem CategoryTheory.Limits.Bicone.toCocone_pt

added theorem CategoryTheory.Limits.Bicone.toCocone_ι_app

added theorem CategoryTheory.Limits.Bicone.toCocone_ι_app_mk

added def CategoryTheory.Limits.Bicone.toCone

added theorem CategoryTheory.Limits.Bicone.toCone_pt

added theorem CategoryTheory.Limits.Bicone.toCone_π_app

added theorem CategoryTheory.Limits.Bicone.toCone_π_app_mk

added def CategoryTheory.Limits.Bicone.whisker

added def CategoryTheory.Limits.Bicone.whiskerIsBilimitIff

added def CategoryTheory.Limits.Bicone.whiskerToCocone

added def CategoryTheory.Limits.Bicone.whiskerToCone

added theorem CategoryTheory.Limits.Bicone.ι_of_isLimit

added theorem CategoryTheory.Limits.Bicone.π_of_isColimit

added structure CategoryTheory.Limits.Bicone

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.toBicone

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 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 theorem CategoryTheory.Limits.HasBiproduct.mk

added structure CategoryTheory.Limits.LimitBicone

added theorem CategoryTheory.Limits.bicone_ι_π_ne

added theorem CategoryTheory.Limits.bicone_ι_π_self

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_isoCoprod_hom

added def CategoryTheory.Limits.biproduct.bicone

added theorem CategoryTheory.Limits.biproduct.bicone_ι

added theorem CategoryTheory.Limits.biproduct.bicone_π

added def CategoryTheory.Limits.biproduct.components

added theorem CategoryTheory.Limits.biproduct.components_matrix

added theorem CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom

added theorem CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv

added def CategoryTheory.Limits.biproduct.fromSubtype

added theorem CategoryTheory.Limits.biproduct.fromSubtype_eq_lift

added theorem CategoryTheory.Limits.biproduct.fromSubtype_toSubtype

added theorem CategoryTheory.Limits.biproduct.fromSubtype_π

added theorem CategoryTheory.Limits.biproduct.fromSubtype_π_subtype

added theorem CategoryTheory.Limits.biproduct.hom_ext'

added theorem CategoryTheory.Limits.biproduct.hom_ext

added def CategoryTheory.Limits.biproduct.isBilimit

added def CategoryTheory.Limits.biproduct.isColimit

added def CategoryTheory.Limits.biproduct.isColimitToSubtype

added def CategoryTheory.Limits.biproduct.isLimit

added def CategoryTheory.Limits.biproduct.isLimitFromSubtype

added def CategoryTheory.Limits.biproduct.isoCoproduct

added theorem CategoryTheory.Limits.biproduct.isoCoproduct_hom

added theorem CategoryTheory.Limits.biproduct.isoCoproduct_inv

added def CategoryTheory.Limits.biproduct.isoProduct

added theorem CategoryTheory.Limits.biproduct.isoProduct_hom

added theorem CategoryTheory.Limits.biproduct.isoProduct_inv

added theorem CategoryTheory.Limits.biproduct.lift_map

added theorem CategoryTheory.Limits.biproduct.lift_π

added def CategoryTheory.Limits.biproduct.mapIso

added theorem CategoryTheory.Limits.biproduct.map_desc

added theorem CategoryTheory.Limits.biproduct.map_eq_map'

added theorem CategoryTheory.Limits.biproduct.map_π

added def CategoryTheory.Limits.biproduct.matrix

added def CategoryTheory.Limits.biproduct.matrixEquiv

added theorem CategoryTheory.Limits.biproduct.matrix_components

added theorem CategoryTheory.Limits.biproduct.matrix_π

added def CategoryTheory.Limits.biproduct.toSubtype

added theorem CategoryTheory.Limits.biproduct.toSubtype_eq_desc

added theorem CategoryTheory.Limits.biproduct.toSubtype_fromSubtype

added theorem CategoryTheory.Limits.biproduct.toSubtype_π

added def CategoryTheory.Limits.biproduct.uniqueUpToIso

added theorem CategoryTheory.Limits.biproduct.ι_desc

added theorem CategoryTheory.Limits.biproduct.ι_fromSubtype

added theorem CategoryTheory.Limits.biproduct.ι_map

added theorem CategoryTheory.Limits.biproduct.ι_matrix

added theorem CategoryTheory.Limits.biproduct.ι_toSubtype

added theorem CategoryTheory.Limits.biproduct.ι_toSubtype_subtype

added theorem CategoryTheory.Limits.biproduct.ι_π

added theorem CategoryTheory.Limits.biproduct.ι_π_ne

added theorem CategoryTheory.Limits.biproduct.ι_π_self

added def CategoryTheory.Limits.biproductIso

added def CategoryTheory.Limits.biproductUniqueIso

added def CategoryTheory.Limits.cokernelBiprodInlIso

added def CategoryTheory.Limits.cokernelBiprodInrIso

added def CategoryTheory.Limits.cokernelBiproductFromSubtypeIso

added def CategoryTheory.Limits.cokernelBiproductιIso

added def CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype

added def CategoryTheory.Limits.getBinaryBiproductData

added def CategoryTheory.Limits.getBiproductData

added theorem CategoryTheory.Limits.hasBinaryBiproducts_of_finite_biproducts

added theorem CategoryTheory.Limits.hasBiproductsOfShape_of_equiv

added def CategoryTheory.Limits.isoBiprodZero

added def CategoryTheory.Limits.isoZeroBiprod

added def CategoryTheory.Limits.kernelBiprodFstIso

added def CategoryTheory.Limits.kernelBiprodSndIso

added def CategoryTheory.Limits.kernelBiproductToSubtypeIso

added def CategoryTheory.Limits.kernelBiproductπIso

added def CategoryTheory.Limits.kernelForkBiproductToSubtype

added def CategoryTheory.Limits.limitBiconeOfUnique

added theorem CategoryTheory.isIso_left_of_isIso_biprod_map

added theorem CategoryTheory.isIso_right_of_isIso_biprod_map