Commit 2025-05-18 16:59 7abfd576

View on Github →

feat(AlgebraicGeometry): finite type points in jacobson schemes (#24938)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

added theorem AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion

Modified Mathlib/AlgebraicGeometry/Morphisms/Finite.lean

added theorem AlgebraicGeometry.IsFinite.SpecMap_iff

added theorem AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints

added theorem AlgebraicGeometry.isClosed_singleton_iff_locallyOfFiniteType

added theorem AlgebraicGeometry.isFinite_iff_locallyOfFiniteType_of_jacobsonSpace

Modified Mathlib/AlgebraicGeometry/ResidueField.lean

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

added theorem IsLocalRing.isClosed_singleton_closedPoint

Modified Mathlib/Topology/Irreducible.lean