Commit 2024-07-14 15:55 df963657

View on Github →

feat(AlgebraicGeometry/Pullbacks): Fibred product of affine schemes. (#14711) This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Estimated changes

Modified Mathlib/Algebra/Category/Ring/Constructions.lean

modified def CommRingCat.pushoutCocone

modified def CommRingCat.pushoutCoconeIsColimit

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

added def AlgebraicGeometry.pullbackSpecIso

added theorem AlgebraicGeometry.pullbackSpecIso_hom_fst

added theorem AlgebraicGeometry.pullbackSpecIso_hom_snd

added theorem AlgebraicGeometry.pullbackSpecIso_inv_fst

added theorem AlgebraicGeometry.pullbackSpecIso_inv_snd

Modified Mathlib/RingTheory/RingHomProperties.lean