Commit 2023-03-10 08:05 c48abe75

View on Github →

feat: port CategoryTheory.Preadditive.Biproducts (#2760)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/Biproducts.lean

added theorem CategoryTheory.Biprod.column_nonzero_of_iso

added def CategoryTheory.Biprod.gaussian'

added def CategoryTheory.Biprod.gaussian

added theorem CategoryTheory.Biprod.inl_ofComponents

added theorem CategoryTheory.Biprod.inr_ofComponents

added def CategoryTheory.Biprod.isoElim'

added def CategoryTheory.Biprod.isoElim

added def CategoryTheory.Biprod.ofComponents

added theorem CategoryTheory.Biprod.ofComponents_comp

added theorem CategoryTheory.Biprod.ofComponents_eq

added theorem CategoryTheory.Biprod.ofComponents_fst

added theorem CategoryTheory.Biprod.ofComponents_snd

added def CategoryTheory.Biprod.unipotentLower

added def CategoryTheory.Biprod.unipotentUpper

added def CategoryTheory.Biproduct.columnNonzeroOfIso

added theorem CategoryTheory.Biproduct.column_nonzero_of_iso'

added def CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelFst

added def CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelSnd

added def CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInl

added def CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInr

added def CategoryTheory.Limits.BinaryBicone.ofColimitCocone

added def CategoryTheory.Limits.BinaryBicone.ofLimitCone

added theorem CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryCoproduct

added theorem CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryProduct

added theorem CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryCoproducts

added theorem CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts

added theorem CategoryTheory.Limits.HasBiproduct.of_hasCoproduct

added theorem CategoryTheory.Limits.HasBiproduct.of_hasProduct

added theorem CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteCoproducts

added theorem CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts

added theorem CategoryTheory.Limits.IsBilimit.binary_total

added theorem CategoryTheory.Limits.IsBilimit.total

added def CategoryTheory.Limits.biconeIsBilimitOfColimitCoconeOfIsColimit

added def CategoryTheory.Limits.biconeIsBilimitOfLimitConeOfIsLimit

added def CategoryTheory.Limits.binaryBiconeIsBilimitOfColimitCoconeOfIsColimit

added def CategoryTheory.Limits.binaryBiconeIsBilimitOfLimitConeOfIsLimit

added def CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel

added def CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel

added theorem CategoryTheory.Limits.biprod.add_eq_lift_desc_id

added theorem CategoryTheory.Limits.biprod.add_eq_lift_id_desc

added theorem CategoryTheory.Limits.biprod.desc_eq

added theorem CategoryTheory.Limits.biprod.lift_desc

added theorem CategoryTheory.Limits.biprod.lift_eq

added theorem CategoryTheory.Limits.biprod.map_eq

added theorem CategoryTheory.Limits.biprod.total

added theorem CategoryTheory.Limits.biproduct.desc_eq

added theorem CategoryTheory.Limits.biproduct.lift_desc

added theorem CategoryTheory.Limits.biproduct.lift_eq

added theorem CategoryTheory.Limits.biproduct.lift_matrix

added theorem CategoryTheory.Limits.biproduct.map_eq

added theorem CategoryTheory.Limits.biproduct.map_matrix

added theorem CategoryTheory.Limits.biproduct.matrix_desc

added theorem CategoryTheory.Limits.biproduct.matrix_map

added def CategoryTheory.Limits.biproduct.reindex

added theorem CategoryTheory.Limits.biproduct.total

added theorem CategoryTheory.Limits.fst_of_isColimit

added theorem CategoryTheory.Limits.hasBinaryBiproduct_of_total

added theorem CategoryTheory.Limits.hasBiproduct_of_total

added theorem CategoryTheory.Limits.inl_of_isLimit

added theorem CategoryTheory.Limits.inr_of_isLimit

added def CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitEpiOfKernel

added def CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitMonoOfCokernel

added def CategoryTheory.Limits.isBilimitOfIsColimit

added def CategoryTheory.Limits.isBilimitOfIsLimit

added def CategoryTheory.Limits.isBilimitOfTotal

added def CategoryTheory.Limits.isBinaryBilimitOfIsColimit

added def CategoryTheory.Limits.isBinaryBilimitOfIsLimit

added def CategoryTheory.Limits.isBinaryBilimitOfTotal

added def CategoryTheory.Limits.preservesBinaryBiproductOfEpiBiprodComparison'

added def CategoryTheory.Limits.preservesBinaryBiproductOfMonoBiprodComparison

added def CategoryTheory.Limits.preservesBinaryBiproductOfPreservesBinaryCoproduct

added def CategoryTheory.Limits.preservesBinaryBiproductOfPreservesBinaryProduct

added def CategoryTheory.Limits.preservesBinaryBiproductsOfPreservesBinaryCoproducts

added def CategoryTheory.Limits.preservesBinaryBiproductsOfPreservesBinaryProducts

added def CategoryTheory.Limits.preservesBinaryCoproductOfPreservesBinaryBiproduct

added def CategoryTheory.Limits.preservesBinaryCoproductsOfPreservesBinaryBiproducts

added def CategoryTheory.Limits.preservesBinaryProductOfPreservesBinaryBiproduct

added def CategoryTheory.Limits.preservesBinaryProductsOfPreservesBinaryBiproducts

added def CategoryTheory.Limits.preservesBiproductOfEpiBiproductComparison'

added def CategoryTheory.Limits.preservesBiproductOfMonoBiproductComparison

added def CategoryTheory.Limits.preservesBiproductOfPreservesCoproduct

added def CategoryTheory.Limits.preservesBiproductOfPreservesProduct

added def CategoryTheory.Limits.preservesBiproductsOfShapeOfPreservesCoproductsOfShape

added def CategoryTheory.Limits.preservesBiproductsOfShapeOfPreservesProductsOfShape

added def CategoryTheory.Limits.preservesCoproductOfPreservesBiproduct

added def CategoryTheory.Limits.preservesCoproductsOfShapeOfPreservesBiproductsOfShape

added def CategoryTheory.Limits.preservesProductOfPreservesBiproduct

added def CategoryTheory.Limits.preservesProductsOfShapeOfPreservesBiproductsOfShape

added theorem CategoryTheory.Limits.snd_of_isColimit