Module

IsOpenImmersion_ringKrullDim_stalk_eq.lean

Nyll.AlgebraicCurves.Geometry.Schemes.IsOpenImmersion_ringKrullDim_stalk_eq

1 declaration indexed from sourceView source ↗

Module documentation

Is Open Immersion ring Krull Dim stalk eq

Imports2

Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.RingTheory.KrullDimension.Basic

Imported by1

Nyll.AlgebraicCurves.Geometry.Schemes.All

theorem

ringKrullDim_stalk_eq

L28 ↗

AlgebraicGeometry.IsOpenImmersion.ringKrullDim_stalk_eq

Source context 4 commands

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

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

Lean source · statement

theorem _root_.AlgebraicGeometry.IsOpenImmersion.ringKrullDim_stalk_eq
    {U X : Scheme.{u}} (i : U ⟶ X) [IsOpenImmersion i] (u : U) :
    ringKrullDim (U.presheaf.stalk u) = ringKrullDim (X.presheaf.stalk (i.base u))

Module documentation

Is Open Immersion ring Krull Dim stalk eq

Declarations

ringKrullDim_stalk_eq