Mathlib Changelog
v4
Changelog
About
Github
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