AlgebraicGeometry.SmoothOfRelativeDimension.topologicalKrullDim_preimage_singleton_eq
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace SmoothOfRelativeDimension_topologicalKrullDim_preimage_singleton_eq
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.SmoothOfRelativeDimension.topologicalKrullDim_preimage_singleton_eq
{X Y : Scheme.{u}} (f : X ⟶ Y) (n : ℕ) [SmoothOfRelativeDimension n f]
(y : ↥Y) (hy : (f.base ⁻¹' {y}).Nonempty) :
topologicalKrullDim ↥(f.base ⁻¹' {y}) = n