Commit 2026-04-28 05:54 56770c87

View on Github →

feat(AlgebraicGeometry): The codimension of a point of a scheme is equal to the krull dimension of the stalk (#26735) In this PR we show that the codimension of a point in a scheme is equal to the krull dimension of the local ring at that point, as in stacks 02IZ.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Properties.lean

added theorem AlgebraicGeometry.coheight_eq_of_isOpenImmersion

added theorem AlgebraicGeometry.idealHeight_eq_coheight

added theorem AlgebraicGeometry.ringKrullDim_stalk_eq_coheight

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added def AlgebraicGeometry.primeSpectrumOrderIsoSpec

added def AlgebraicGeometry.specOrderIsoPrimeSpectrum

Modified Mathlib/Order/KrullDimension.lean

added theorem Order.coheight_eq_of_strictMono

added theorem Order.height_eq_of_strictMono

Modified Mathlib/Topology/Continuous.lean

added theorem nonempty_preimage_closure_image

Modified Mathlib/Topology/Irreducible.lean

added theorem closure_image_preimage_of_isPreirreducible

Modified Mathlib/Topology/KrullDimension.lean

added theorem Topology.IsOpenEmbedding.coheight_eq

added theorem Topology.IsOpenEmbedding.coheight_map

Modified Mathlib/Topology/Maps/Basic.lean

added theorem Topology.IsInducing.IsOpenMap.preimage_closure_image

Modified Mathlib/Topology/Sets/Closeds.lean

added def TopologicalSpace.IrreducibleCloseds.orderIsoOfIsOpenEmbedding

Modified Mathlib/Topology/Sober.lean

added theorem coe_irreducibleEquivPoints_symm_apply