Commit 2025-02-04 06:00 d3675333

View on Github →

feat(AlgebraicGeometry): integral = universally closed + affine (#19419) as a corollary, finite = proper + affine

Estimated changes

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

added theorem CommRingCat.isPushout_of_isPushout

Modified Mathlib/Algebra/Polynomial/Eval/Defs.lean

modified theorem Polynomial.mapRingHom_comp_C

Modified Mathlib/AlgebraicGeometry/Morphisms/Integral.lean

added theorem AlgebraicGeometry.IsIntegralHom.SpecMap_iff

added theorem AlgebraicGeometry.IsIntegralHom.eq_universallyClosed_inf_isAffineHom

added theorem AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHom

Modified Mathlib/AlgebraicGeometry/Morphisms/Proper.lean

added theorem AlgebraicGeometry.IsFinite.eq_isProper_inf_isAffineHom

added theorem AlgebraicGeometry.IsFinite.iff_isProper_and_isAffineHom

Modified Mathlib/RingTheory/IsTensorProduct.lean

added def Algebra.IsPushout.equiv

added theorem Algebra.IsPushout.equiv_symm_algebraMap_left

added theorem Algebra.IsPushout.equiv_symm_algebraMap_right

added theorem Algebra.IsPushout.equiv_tmul

Modified Mathlib/RingTheory/PolynomialAlgebra.lean

added def Polynomial.algebra