Module

SmoothRelativeDimension.lean

Nyll.AlgebraicCurves.Geometry.Schemes.SmoothRelativeDimension

11 declarations indexed from sourceView source ↗

Module documentation

Smooth Relative Dimension

Imports15

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.FieldTheory.Perfect
Mathlib.FieldTheory.Minpoly.Field
Mathlib.LinearAlgebra.Dimension.Finite
Mathlib.RingTheory.Derivation.Basic
Mathlib.RingTheory.RingHom.StandardSmooth
Mathlib.RingTheory.RingHom.LocallyStandardSmooth
Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Mathlib.Tactic.Algebraize
Mathlib.Tactic.ByContra
Mathlib.Tactic.Convert
Mathlib.Tactic.Ext
Mathlib.Tactic.Ring

Imported by2

theorem

kw_isStandardSmoothOfRelativeDimension_finrank

L43 ↗

AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_isStandardSmoothOfRelativeDimension_finrank

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry RingHom
noncomputable section
universe u
namespace AlgebraicGeometry
namespace KwSmoothIrredRelDimConstantEngine

Lean source · statement

theorem kw_isStandardSmoothOfRelativeDimension_finrank
    {R : Type*} {S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.IsStandardSmooth R S] [Nontrivial S] :
    Algebra.IsStandardSmoothOfRelativeDimension (Module.finrank S (Ω[S⁄R])) R S

theorem

kw_isStandardSmoothOfRelativeDimension_unique

L51 ↗

AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_isStandardSmoothOfRelativeDimension_unique

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry RingHom
noncomputable section
universe u
namespace AlgebraicGeometry
namespace KwSmoothIrredRelDimConstantEngine

Lean source · statement

theorem kw_isStandardSmoothOfRelativeDimension_unique
    {R : Type*} {S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Nontrivial S] {n m : ℕ}
    (hn : Algebra.IsStandardSmoothOfRelativeDimension n R S)
    (hm : Algebra.IsStandardSmoothOfRelativeDimension m R S) : n = m

theorem

kw_isStandardSmoothOfRelDim_basicOpen

L63 ↗

AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_isStandardSmoothOfRelDim_basicOpen

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry RingHom
noncomputable section
universe u
namespace AlgebraicGeometry
namespace KwSmoothIrredRelDimConstantEngine
section SchemeLevel
variable {X Y : Scheme.{u}}

Lean source · statement

theorem kw_isStandardSmoothOfRelDim_basicOpen {g : X ⟶ Y} [IsAffine Y]
    {V : X.Opens} (hV : IsAffineOpen V) {n : ℕ}
    (h : (g.appLE ⊤ V le_top).hom.IsStandardSmoothOfRelativeDimension n) (s : Γ(X, V)) :
    (g.appLE ⊤ (X.basicOpen s) le_top).hom.IsStandardSmoothOfRelativeDimension n

theorem

kw_exists_relDim_appLE_top_of_relDim

L74 ↗

AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_exists_relDim_appLE_top_of_relDim

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry RingHom
noncomputable section
universe u
namespace AlgebraicGeometry
namespace KwSmoothIrredRelDimConstantEngine
section SchemeLevel
variable {X Y : Scheme.{u}}

Lean source · statement

theorem kw_exists_relDim_appLE_top_of_relDim
    (g : X ⟶ Y) [IsAffine Y] (n : ℕ) [hg : SmoothOfRelativeDimension n g] (x : X) :
    ∃ (V : X.Opens) (_ : IsAffineOpen V), x ∈ V ∧
      (g.appLE ⊤ V le_top).hom.IsStandardSmoothOfRelativeDimension n

theorem

kw_exists_relDim_appLE_top

L103 ↗

AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_exists_relDim_appLE_top

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry RingHom
noncomputable section
universe u
namespace AlgebraicGeometry
namespace KwSmoothIrredRelDimConstantEngine
section SchemeLevel
variable {X Y : Scheme.{u}}

Lean source · statement

theorem kw_exists_relDim_appLE_top
    (g : X ⟶ Y) [IsAffine Y] [Smooth g] (x : X) :
    ∃ (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (r : ℕ),
      (g.appLE ⊤ V le_top).hom.IsStandardSmoothOfRelativeDimension r

theorem

kw_relDim_eq_of_mem_both

L136 ↗

AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_relDim_eq_of_mem_both

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry RingHom
noncomputable section
universe u
namespace AlgebraicGeometry
namespace KwSmoothIrredRelDimConstantEngine
section SchemeLevel
variable {X Y : Scheme.{u}}

Lean source · statement

theorem kw_relDim_eq_of_mem_both {g : X ⟶ Y} [IsAffine Y]
    {V₁ V₂ : X.Opens} (hV₁ : IsAffineOpen V₁) (hV₂ : IsAffineOpen V₂) {n₁ n₂ : ℕ}
    (h₁ : (g.appLE ⊤ V₁ le_top).hom.IsStandardSmoothOfRelativeDimension n₁)
    (h₂ : (g.appLE ⊤ V₂ le_top).hom.IsStandardSmoothOfRelativeDimension n₂)
    {z : X} (hz₁ : z ∈ V₁) (hz₂ : z ∈ V₂) : n₁ = n₂

theorem

kw_appLE_top_opensImage

L159 ↗

AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_appLE_top_opensImage

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry RingHom
noncomputable section
universe u
namespace AlgebraicGeometry
namespace KwSmoothIrredRelDimConstantEngine
section SchemeLevel
variable {X Y : Scheme.{u}}

Lean source · statement

theorem kw_appLE_top_opensImage {W : X.Opens} {g : X ⟶ Y} [IsAffine Y]
    {V : (W : Scheme.{u}).Opens} {n : ℕ}
    (h : ((W.ι ≫ g).appLE ⊤ V le_top).hom.IsStandardSmoothOfRelativeDimension n) :
    (g.appLE ⊤ (W.ι ''ᵁ V) le_top).hom.IsStandardSmoothOfRelativeDimension n

theorem

kw_smoothOfRelativeDimension_of_irreducible_of_nonempty_open

L180 ↗

AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_smoothOfRelativeDimension_of_irreducible_of_nonempty_open

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry RingHom
noncomputable section
universe u
namespace AlgebraicGeometry
namespace KwSmoothIrredRelDimConstantEngine
section SchemeLevel
variable {X Y : Scheme.{u}}

Lean source · statement

theorem kw_smoothOfRelativeDimension_of_irreducible_of_nonempty_open
    (g : X ⟶ Y) [IsAffine Y] [Smooth g] [IrreducibleSpace X]
    (n : ℕ) (W : X.Opens) (hWne : (W : Set X).Nonempty)
    (hWg : SmoothOfRelativeDimension n (W.ι ≫ g)) :
    SmoothOfRelativeDimension n g

theorem

kw_of_comp_isOpenImmersion

L203 ↗

AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_of_comp_isOpenImmersion

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry RingHom
noncomputable section
universe u
namespace AlgebraicGeometry
namespace KwSmoothIrredRelDimConstantEngine
section SchemeLevel
variable {X Y : Scheme.{u}}

Lean source · statement

theorem kw_of_comp_isOpenImmersion (P : MorphismProperty Scheme.{u})
    [IsZariskiLocalAtTarget P] {Z : Scheme.{u}} (f : X ⟶ Y) (i : Y ⟶ Z) [IsOpenImmersion i]
    (h : P (f ≫ i)) : P f

theorem

kw_smoothOfRelativeDimension_of_irreducible_of_isOpenImmersion

L222 ↗

AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_smoothOfRelativeDimension_of_irreducible_of_isOpenImmersion

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry RingHom
noncomputable section
universe u
namespace AlgebraicGeometry
namespace KwSmoothIrredRelDimConstantEngine
section SchemeLevel
variable {X Y : Scheme.{u}}

Lean source · statement

theorem kw_smoothOfRelativeDimension_of_irreducible_of_isOpenImmersion
    (g : X ⟶ Y) [IsAffine Y] [Smooth g] [IrreducibleSpace X]
    (n : ℕ) {W : Scheme.{u}} (i : W ⟶ X) [IsOpenImmersion i] [Nonempty W]
    (hig : SmoothOfRelativeDimension n (i ≫ g)) :
    SmoothOfRelativeDimension n g

theorem

kw_not_isStandardSmoothOfRelDim_succ_of_finite

L248 ↗

AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_not_isStandardSmoothOfRelDim_succ_of_finite

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry RingHom
noncomputable section
universe u
namespace AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine

Lean source · statement

theorem kw_not_isStandardSmoothOfRelDim_succ_of_finite
    {k : Type*} [Field k] [PerfectField k]
    {A : Type*} [CommRing A] [Algebra k A] [Nontrivial A] [Module.Finite k A]
    [_root_.IsReduced A] (n : ℕ) :
    ¬ Algebra.IsStandardSmoothOfRelativeDimension (n + 1) k A

Module documentation

Smooth Relative Dimension

Declarations