Commit 2025-04-15 09:57 69393803

View on Github →

feat: a binary fan in Over X is the same thing as a pullback cone to X (#23723) From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

added def CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor

added def CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanInverse

added def CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor

added def CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanInverse

added def CategoryTheory.Limits.Over.ConstructProducts.conesEquiv

added def CategoryTheory.Limits.Over.ConstructProducts.conesEquivCounitIso

added def CategoryTheory.Limits.Over.ConstructProducts.conesEquivFunctor

added def CategoryTheory.Limits.Over.ConstructProducts.conesEquivInverse

added def CategoryTheory.Limits.Over.ConstructProducts.conesEquivInverseObj

added def CategoryTheory.Limits.Over.ConstructProducts.conesEquivUnitIso

added theorem CategoryTheory.Limits.Over.ConstructProducts.has_over_limit_discrete_of_widePullback_limit

added theorem CategoryTheory.Limits.Over.ConstructProducts.over_binaryProduct_of_pullback

added theorem CategoryTheory.Limits.Over.ConstructProducts.over_finiteProducts_of_finiteWidePullbacks

added theorem CategoryTheory.Limits.Over.ConstructProducts.over_product_of_widePullback

added theorem CategoryTheory.Limits.Over.ConstructProducts.over_products_of_widePullbacks

added theorem CategoryTheory.Limits.Over.isPullback_of_binaryFan_isLimit

added theorem CategoryTheory.Limits.Over.over_hasTerminal

added def CategoryTheory.Limits.Over.prodLeftIsoPullback

added theorem CategoryTheory.Limits.Over.prodLeftIsoPullback_hom_fst

added theorem CategoryTheory.Limits.Over.prodLeftIsoPullback_hom_snd

added theorem CategoryTheory.Limits.Over.prodLeftIsoPullback_inv_fst

added theorem CategoryTheory.Limits.Over.prodLeftIsoPullback_inv_snd

added def CategoryTheory.Limits.pullbackConeEquivBinaryFan

added def CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan

deleted def CategoryTheory.Over.ConstructProducts.conesEquiv

deleted def CategoryTheory.Over.ConstructProducts.conesEquivCounitIso

deleted def CategoryTheory.Over.ConstructProducts.conesEquivFunctor

deleted def CategoryTheory.Over.ConstructProducts.conesEquivInverse

deleted def CategoryTheory.Over.ConstructProducts.conesEquivInverseObj

deleted def CategoryTheory.Over.ConstructProducts.conesEquivUnitIso

deleted theorem CategoryTheory.Over.ConstructProducts.has_over_limit_discrete_of_widePullback_limit

deleted theorem CategoryTheory.Over.ConstructProducts.over_binaryProduct_of_pullback

deleted theorem CategoryTheory.Over.ConstructProducts.over_finiteProducts_of_finiteWidePullbacks

deleted theorem CategoryTheory.Over.ConstructProducts.over_product_of_widePullback

deleted theorem CategoryTheory.Over.ConstructProducts.over_products_of_widePullbacks

deleted theorem CategoryTheory.Over.isPullback_of_binaryFan_isLimit

deleted theorem CategoryTheory.Over.over_hasTerminal

deleted def CategoryTheory.Over.prodLeftIsoPullback

deleted theorem CategoryTheory.Over.prodLeftIsoPullback_hom_fst

deleted theorem CategoryTheory.Over.prodLeftIsoPullback_hom_snd

deleted theorem CategoryTheory.Over.prodLeftIsoPullback_inv_fst

deleted theorem CategoryTheory.Over.prodLeftIsoPullback_inv_snd

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

added theorem CategoryTheory.Limits.BinaryCofan.ext_hom_hom

added theorem CategoryTheory.Limits.BinaryFan.ext_hom_hom