Commit 2024-11-11 07:17 83b4d7d6

View on Github →

feat(AlgebraicGeometry): quasi-compact + specializing => closed map (#18032) Partially from the valuative criterion project

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

added theorem AlgebraicGeometry.compactSpace_iff_exists

added theorem AlgebraicGeometry.isClosedMap_iff_specializingMap

added theorem AlgebraicGeometry.isCompact_iff_exists

Modified Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

added theorem PrimeSpectrum.closure_range_comap

added theorem PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical

added theorem PrimeSpectrum.denseRange_comap_iff_minimalPrimes

added theorem PrimeSpectrum.isClosed_image_of_stableUnderSpecialization

added theorem PrimeSpectrum.isClosed_range_of_stableUnderSpecialization

added theorem PrimeSpectrum.stableUnderSpecialization_image_iff

added theorem PrimeSpectrum.stableUnderSpecialization_range_iff

added theorem PrimeSpectrum.vanishingIdeal_range_comap

Modified Mathlib/AlgebraicGeometry/Scheme.lean

modified theorem AlgebraicGeometry.Scheme.Hom.continuous

Modified Mathlib/Topology/Inseparable.lean

added theorem GeneralizingMap.comp

added theorem SpecializingMap.comp

Modified scripts/noshake.json