Commit 2024-11-28 19:04 6262f69d

View on Github →

feat(Algebra/Category): Under.pushout f is left-exact if f is flat. (#19213)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/Ring/Under/Limits.lean

added def CommRingCat.Under.equalizerFork'

added def CommRingCat.Under.equalizerFork'IsLimit

added theorem CommRingCat.Under.equalizerFork'_ι

added def CommRingCat.Under.equalizerFork

added def CommRingCat.Under.equalizerForkIsLimit

added def CommRingCat.Under.equalizerForkTensorProdIso

added theorem CommRingCat.Under.equalizerFork_ι

added theorem CommRingCat.Under.equalizer_comp

added def CommRingCat.Under.piFan

added def CommRingCat.Under.piFanIsLimit

added def CommRingCat.Under.piFanTensorProductIsLimit

added theorem CommRingCat.Under.preservesFiniteLimits_of_flat

added def CommRingCat.Under.tensorProdEqualizer

added theorem CommRingCat.Under.tensorProdEqualizer_ι

added def CommRingCat.Under.tensorProdMapEqualizerForkIsLimit

added def CommRingCat.Under.tensorProductFan'

added def CommRingCat.Under.tensorProductFan

added def CommRingCat.Under.tensorProductFanIsLimit

added def CommRingCat.Under.tensorProductFanIso

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

added theorem CategoryTheory.Limits.preservesColimitsOfShape_of_discrete

added theorem CategoryTheory.Limits.preservesLimitsOfShape_of_discrete

Created Mathlib/RingTheory/TensorProduct/Pi.lean

added theorem Algebra.TensorProduct.piRight_tmul

added theorem piRightHom_mul

added theorem piRightHom_one