Module

IsAffineOpen_ringKrullDim_stalk_le.lean

Nyll.AlgebraicCurves.Geometry.Schemes.IsAffineOpen_ringKrullDim_stalk_le

1 declaration indexed from sourceView source ↗

Module documentation

Is Affine Open ring Krull Dim stalk le

Imports2

Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.RingTheory.Ideal.Height

Imported by1

Nyll.AlgebraicCurves.Geometry.Schemes.All

theorem

ringKrullDim_stalk_le

L28 ↗

AlgebraicGeometry.IsAffineOpen.ringKrullDim_stalk_le

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.IsAffineOpen_ringKrullDim_stalk_le
universe u
open CategoryTheory AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.IsAffineOpen.ringKrullDim_stalk_le
    {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U) (x : X) (hx : x ∈ U) :
    ringKrullDim (X.presheaf.stalk x) ≤ ringKrullDim Γ(X, U)

Module documentation

Is Affine Open ring Krull Dim stalk le

Declarations

ringKrullDim_stalk_le