Commit 2025-11-30 12:04 e56018af

View on Github →

feat: a pullback of schemes is canonically over the second component (#31475) From Toric

Estimated changes

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

added theorem AlgebraicGeometry.pullbackSpecIso_hom_base

added theorem AlgebraicGeometry.pullbackSpecIso_hom_fst'

added theorem AlgebraicGeometry.pullbackSpecIso_inv_fst'

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Over.lean

added theorem CategoryTheory.Over.preservesTerminalIso_pullback

added theorem CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst'

added theorem CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst

added theorem CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd'

added theorem CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd'

modified theorem CategoryTheory.Over.tensorObj_left

added theorem CategoryTheory.Over.ε_pullback_left

added theorem CategoryTheory.Over.η_pullback_left

added theorem CategoryTheory.Over.μ_pullback_left_fst_fst'

added theorem CategoryTheory.Over.μ_pullback_left_fst_fst

added theorem CategoryTheory.Over.μ_pullback_left_fst_snd'

added theorem CategoryTheory.Over.μ_pullback_left_fst_snd

added theorem CategoryTheory.Over.μ_pullback_left_snd'

added theorem CategoryTheory.Over.μ_pullback_left_snd