Module

SmoothOfRelativeDimension_topologicalKrullDim_le.lean

Nyll.AlgebraicCurves.Geometry.Schemes.SmoothOfRelativeDimension_topologicalKrullDim_le

10 declarations indexed from sourceView source ↗

Module documentation

Smooth Of Relative Dimension topological Krull Dim le

Imports9

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.RingTheory.Smooth.Local
Mathlib.RingTheory.Smooth.Field
Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Mathlib.Algebra.Module.SpanRankOperations
Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Mathlib.Topology.KrullDimension

Imported by8

theorem

spanFinrank_maximalIdeal_le_finrank_kaehler

L39 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le.P2mSmoothOfRelativeDimensionKrullDim.spanFinrank_maximalIdeal_le_finrank_kaehler

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mSmoothOfRelativeDimensionKrullDim
open TensorProduct IsLocalRing TopologicalSpace Topology

Lean source · statement

theorem spanFinrank_maximalIdeal_le_finrank_kaehler
    (L P : Type*) [CommRing L] [CommRing P] [Algebra L P] [IsLocalRing P] [IsNoetherianRing P]
    [Algebra.FormallySmooth L P] [Module.Free P Ω[P⁄L]] [Module.Finite P Ω[P⁄L]]
    [Algebra.FormallySmooth L (ResidueField P)] :
    (maximalIdeal P).spanFinrank ≤ Module.finrank P Ω[P⁄L]

theorem

ringKrullDim_le_finrank_kaehler

L74 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le.P2mSmoothOfRelativeDimensionKrullDim.ringKrullDim_le_finrank_kaehler

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mSmoothOfRelativeDimensionKrullDim
open TensorProduct IsLocalRing TopologicalSpace Topology

Lean source · statement

theorem ringKrullDim_le_finrank_kaehler
    (L P : Type*) [CommRing L] [CommRing P] [Algebra L P] [IsLocalRing P] [IsNoetherianRing P]
    [Algebra.FormallySmooth L P] [Module.Free P Ω[P⁄L]] [Module.Finite P Ω[P⁄L]]
    [Algebra.FormallySmooth L (ResidueField P)] :
    ringKrullDim P ≤ Module.finrank P Ω[P⁄L]

theorem

ringKrullDim_localization_le

L86 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le.P2mSmoothOfRelativeDimensionKrullDim.ringKrullDim_localization_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mSmoothOfRelativeDimensionKrullDim
open TensorProduct IsLocalRing TopologicalSpace Topology
section PerfectBase
variable {L : Type*} [Field L] {B : Type*} [CommRing B] [Algebra L B]

Lean source · statement

theorem ringKrullDim_localization_le [PerfectField L] (n : ℕ)
    [Algebra.IsStandardSmoothOfRelativeDimension n L B] (m : Ideal B) [m.IsPrime] :
    ringKrullDim (Localization.AtPrime m) ≤ n

theorem

ringKrullDim_le_of_perfectField

L119 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le.P2mSmoothOfRelativeDimensionKrullDim.ringKrullDim_le_of_perfectField

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mSmoothOfRelativeDimensionKrullDim
open TensorProduct IsLocalRing TopologicalSpace Topology
section PerfectBase
variable {L : Type*} [Field L] {B : Type*} [CommRing B] [Algebra L B]

Lean source · statement

theorem ringKrullDim_le_of_perfectField [PerfectField L] (n : ℕ)
    [Algebra.IsStandardSmoothOfRelativeDimension n L B] : ringKrullDim B ≤ n

theorem

ringKrullDim_le_of_faithfullyFlat

L128 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le.P2mSmoothOfRelativeDimensionKrullDim.ringKrullDim_le_of_faithfullyFlat

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mSmoothOfRelativeDimensionKrullDim
open TensorProduct IsLocalRing TopologicalSpace Topology

Lean source · statement

theorem ringKrullDim_le_of_faithfullyFlat (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    [Module.FaithfullyFlat R S] : ringKrullDim R ≤ ringKrullDim S

theorem

ringKrullDim_le_of_isStandardSmoothOfRelativeDimension

L138 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le.P2mSmoothOfRelativeDimensionKrullDim.ringKrullDim_le_of_isStandardSmoothOfRelativeDimension

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mSmoothOfRelativeDimensionKrullDim
open TensorProduct IsLocalRing TopologicalSpace Topology

Lean source · statement

theorem ringKrullDim_le_of_isStandardSmoothOfRelativeDimension
    {K : Type*} [Field K] {B : Type*} [CommRing B] [Algebra K B] (n : ℕ)
    [Algebra.IsStandardSmoothOfRelativeDimension n K B] : ringKrullDim B ≤ n

theorem

ringKrullDim_le_of_ringHom

L148 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le.P2mSmoothOfRelativeDimensionKrullDim.ringKrullDim_le_of_ringHom

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mSmoothOfRelativeDimensionKrullDim
open TensorProduct IsLocalRing TopologicalSpace Topology

Lean source · statement

theorem ringKrullDim_le_of_ringHom {R S : Type*} [CommRing R] [CommRing S] (hR : IsField R)
    (φ : R →+* S) (n : ℕ) (hφ : φ.IsStandardSmoothOfRelativeDimension n) :
    ringKrullDim S ≤ n

theorem

topologicalKrullDim_le_of_forall_exists_isOpenEmbedding

L160 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le.P2mSmoothOfRelativeDimensionKrullDim.topologicalKrullDim_le_of_forall_exists_isOpenEmbedding

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mSmoothOfRelativeDimensionKrullDim
open TensorProduct IsLocalRing TopologicalSpace Topology
section Sober
attribute [local instance] specializationOrder

Lean source · statement

theorem topologicalKrullDim_le_of_forall_exists_isOpenEmbedding {X : Type u} [TopologicalSpace X]
    [QuasiSober X] [T0Space X] (n : WithBot ℕ∞)
    (h : ∀ x : X, ∃ (U : Type u) (_ : TopologicalSpace U) (g : U → X),
      IsOpenEmbedding g ∧ x ∈ Set.range g ∧ topologicalKrullDim U ≤ n) :
    topologicalKrullDim X ≤ n

theorem

topologicalKrullDim_le

L179 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le.P2mSmoothOfRelativeDimensionKrullDim.topologicalKrullDim_le

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SmoothOfRelativeDimension_topologicalKrullDim_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mSmoothOfRelativeDimensionKrullDim
open TensorProduct IsLocalRing TopologicalSpace Topology

Lean source · statement

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

theorem

topologicalKrullDim_le

L206 ↗

AlgebraicGeometry.SmoothOfRelativeDimension.topologicalKrullDim_le

Source context 4 commands

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

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

Lean source · statement

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

Module documentation

Smooth Of Relative Dimension topological Krull Dim le

Declarations