Module

SmoothOfRelativeDimension_le_topologicalKrullDim.lean

Nyll.AlgebraicCurves.Geometry.Schemes.SmoothOfRelativeDimension_le_topologicalKrullDim

4 declarations indexed from sourceView source ↗

Module documentation

Smooth Of Relative Dimension le topological Krull Dim

Imports4

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.RingTheory.RingHom.StandardSmooth
Mathlib.Tactic.Algebraize
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_height_add_ringKrullDim_quotient_eq_ringKrullDim_of_finiteType

Imported by5

theorem

height_eq_of_isMaximal_mvPolynomial

L32 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_le_topologicalKrullDim.P2mSmoothDimGe.height_eq_of_isMaximal_mvPolynomial

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_le_topologicalKrullDim
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace P2mSmoothDimGe

Lean source · statement

theorem height_eq_of_isMaximal_mvPolynomial (L : Type u) [Field L] (n : ℕ)
    (𝔭 : Ideal (MvPolynomial (Fin n) L)) [h𝔭 : 𝔭.IsMaximal] : 𝔭.height = n

theorem

le_ringKrullDim_of_isStandardSmoothOfRelativeDimension

L44 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_le_topologicalKrullDim.P2mSmoothDimGe.le_ringKrullDim_of_isStandardSmoothOfRelativeDimension

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_le_topologicalKrullDim
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace P2mSmoothDimGe

Lean source · statement

theorem le_ringKrullDim_of_isStandardSmoothOfRelativeDimension {L R : Type u} [CommRing L] (hL :
  IsField L)
    [CommRing R] [Nontrivial R] (φ : L →+* R) (n : ℕ) (hφ : φ.IsStandardSmoothOfRelativeDimension
      n) :
    (n : WithBot ℕ∞) ≤ ringKrullDim R

theorem

le_topologicalKrullDim

L81 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_le_topologicalKrullDim.P2mSmoothDimGe.le_topologicalKrullDim

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_le_topologicalKrullDim
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace P2mSmoothDimGe

Lean source · statement

theorem le_topologicalKrullDim {K : Type u} [Field K] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of K)) (n : ℕ) [SmoothOfRelativeDimension n f] [Nonempty X] :
    (n : WithBot ℕ∞) ≤ topologicalKrullDim X

theorem

le_topologicalKrullDim

L111 ↗

AlgebraicGeometry.SmoothOfRelativeDimension.le_topologicalKrullDim

Source context 4 commands

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

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

Lean source · statement

theorem _root_.AlgebraicGeometry.SmoothOfRelativeDimension.le_topologicalKrullDim
    {K : Type u} [Field K] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of K)) (n : ℕ)
    [SmoothOfRelativeDimension n f] [Nonempty X] :
    (n : WithBot ℕ∞) ≤ topologicalKrullDim X

Module documentation

Smooth Of Relative Dimension le topological Krull Dim

Declarations

height_eq_of_isMaximal_mvPolynomial

le_ringKrullDim_of_isStandardSmoothOfRelativeDimension

le_topologicalKrullDim

le_topologicalKrullDim