Commit 2024-11-13 21:29 50913e62

View on Github →

feat(AlgebraicGeometry): universally closed morphisms are topologically proper (#18863) from the valuative criterion project

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Variables.lean

added theorem MvPolynomial.aeval_ite_mem_eq_self

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

added theorem AlgebraicGeometry.Scheme.Hom.isClosedMap

added theorem AlgebraicGeometry.Scheme.Hom.isProperMap

added theorem AlgebraicGeometry.compactSpace_of_universallyClosed

added theorem AlgebraicGeometry.universallyClosed_eq_universallySpecializing

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.default_asIdeal

added theorem AlgebraicGeometry.Spec.map_base_apply

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

added theorem CategoryTheory.MorphismProperty.universally_inf