Module

Smoothness.lean

Nyll.AlgebraicCurves.Models.Smoothness

17 declarations indexed from sourceView source ↗

Module documentation

Smoothness

Imports18

Nyll.AlgebraicCurves.Models.Basic
Nyll.AlgebraicCurves.Models.ChartAlgebra
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.RingTheory.Extension.Presentation.Submersive
Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Mathlib.RingTheory.Smooth.Field
Mathlib.RingTheory.Smooth.Locus
Mathlib.RingTheory.RingHom.LocallyStandardSmooth
Mathlib.RingTheory.Etale.Kaehler
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Mathlib.RingTheory.Smooth.Fiber
Mathlib.RingTheory.Unramified.LocalRing
Mathlib.RingTheory.LocalRing.ResidueField.Instances
Mathlib.RingTheory.DedekindDomain.Dvr
Mathlib.RingTheory.Flat.TorsionFree

Imported by3

def

freeSubmersivePresentation

L46 ↗

AlgebraicCurve.CurveModel.freeSubmersivePresentation

Documentation

The relation-free submersive presentation of a polynomial algebra.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel

Lean source · full declaration

def freeSubmersivePresentation (R : Type u) [CommRing R] (ι : Type) :
    SubmersivePresentation R (MvPolynomial ι R) ι (PEmpty : Type) where
  __ := Generators.mvPolynomial R ι
  relation := PEmpty.elim
  span_range_relation_eq_ker := by simp [Set.range_eq_empty, Generators.ker_mvPolynomial]
  map := PEmpty.elim
  map_inj := fun a => a.elim
  jacobian_isUnit := by
    rw [PreSubmersivePresentation.jacobian, LinearMap.det_eq_one_of_subsingleton, map_one]
    exact isUnit_one

instance

isStandardSmoothOfRelativeDimension_polynomial

L57 ↗

AlgebraicCurve.CurveModel.isStandardSmoothOfRelativeDimension_polynomial

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel

Lean source · statement

instance isStandardSmoothOfRelativeDimension_polynomial (R : Type u) [CommRing R] :
    IsStandardSmoothOfRelativeDimension 1 R R[X]

theorem

smoothOfRelativeDimension_one_Spec_polynomial

L67 ↗

AlgebraicCurve.CurveModel.smoothOfRelativeDimension_one_Spec_polynomial

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]

Lean source · statement

theorem smoothOfRelativeDimension_one_Spec_polynomial :
    SmoothOfRelativeDimension 1
      (Spec.map (CommRingCat.ofHom (algebraMap K K[X])))

theorem

exists_mem_and_maximalIdeal_eq_span

L82 ↗

AlgebraicCurve.CurveModel.exists_mem_and_maximalIdeal_eq_span

Source context 9 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]
section Coordinate
variable {A : Type u} [CommRing A] [IsDedekindDomain A] [Algebra K A]

Lean source · statement

theorem exists_mem_and_maximalIdeal_eq_span (𝔪 : Ideal A) [𝔪.IsPrime] (h𝔪 : 𝔪 ≠ ⊥) :
    ∃ u : A, u ∈ 𝔪 ∧ u ≠ 0 ∧
      maximalIdeal (Localization.AtPrime 𝔪) =
        Ideal.span {algebraMap A (Localization.AtPrime 𝔪) u}

theorem

transcendental_of_mem

L102 ↗

AlgebraicCurve.CurveModel.transcendental_of_mem

Source context 11 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]
section Coordinate
variable {A : Type u} [CommRing A] [IsDedekindDomain A] [Algebra K A]
variable [IsDomain A] in
omit [IsDedekindDomain A] in

Lean source · statement

theorem transcendental_of_mem {𝔪 : Ideal A} (hne : 𝔪 ≠ ⊤) {u : A} (hu : u ∈ 𝔪) (h0 : u ≠ 0) :
    Transcendental K u

instance

chartRing_finitePresentation

L117 ↗

AlgebraicCurve.CurveModel.chartRing_finitePresentation

Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]

Lean source · statement

instance chartRing_finitePresentation [CharZero K] (s : L) [FiniteDimensional K⟮s⟯ L] :
    FinitePresentation K (chartRing K ({s} : Set L))

theorem

formallySmooth_chartRing_localization_closed

L123 ↗

AlgebraicCurve.CurveModel.formallySmooth_chartRing_localization_closed

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem formallySmooth_chartRing_localization_closed [CharZero K]
    (s : L) [FiniteDimensional K⟮s⟯ L] (hs : Transcendental K s)
    (𝔪 : Ideal (chartRing K ({s} : Set L))) [𝔪.IsPrime] (h𝔪 : 𝔪 ≠ ⊥) :
    Algebra.FormallySmooth K (Localization.AtPrime 𝔪)

theorem

formallySmooth_chartRing_localization_bot

L184 ↗

AlgebraicCurve.CurveModel.formallySmooth_chartRing_localization_bot

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem formallySmooth_chartRing_localization_bot [CharZero K]
    (s : L) [FiniteDimensional K⟮s⟯ L] :
    FormallySmooth K (Localization.AtPrime (⊥ : Ideal (chartRing K ({s} : Set L))))

theorem

chartRing_isSmoothAt

L200 ↗

AlgebraicCurve.CurveModel.chartRing_isSmoothAt

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem chartRing_isSmoothAt [CharZero K] (s : L) [FiniteDimensional K⟮s⟯ L]
    (hs : Transcendental K s) (𝔭 : Ideal (chartRing K ({s} : Set L))) [𝔭.IsPrime] :
    IsSmoothAt K 𝔭

theorem

isStandardSmoothOfRelativeDimension_adjoin_single

L207 ↗

AlgebraicCurve.CurveModel.isStandardSmoothOfRelativeDimension_adjoin_single

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem isStandardSmoothOfRelativeDimension_adjoin_single (s : L) (hs : Transcendental K s) :
    IsStandardSmoothOfRelativeDimension 1 K (Algebra.adjoin K {s})

theorem

rank_kaehler_eq_of_formallyEtale

L215 ↗

AlgebraicCurve.CurveModel.rank_kaehler_eq_of_formallyEtale

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem rank_kaehler_eq_of_formallyEtale (B C : Type u) [CommRing B] [CommRing C]
    [Algebra K B] [Algebra K C] [Algebra B C] [IsScalarTower K B C]
    (M : Submonoid B) (hM : M ≤ nonZeroDivisors B) [IsLocalization M C] :
    Module.rank B Ω[B⁄K] = Module.rank C Ω[C⁄K]

theorem

rank_kaehler_intermediateField_adjoin_single

L226 ↗

AlgebraicCurve.CurveModel.rank_kaehler_intermediateField_adjoin_single

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem rank_kaehler_intermediateField_adjoin_single (s : L) (hs : Transcendental K s) :
    Module.rank K⟮s⟯ Ω[K⟮s⟯⁄K] = 1

theorem

rank_kaehler_eq_one_of_finite_adjoin

L235 ↗

AlgebraicCurve.CurveModel.rank_kaehler_eq_one_of_finite_adjoin

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem rank_kaehler_eq_one_of_finite_adjoin [CharZero K]
    (s : L) (hs : Transcendental K s) [FiniteDimensional K⟮s⟯ L] :
    Module.rank L Ω[L⁄K] = 1

theorem

rank_kaehler_chartRing_localization_away_eq_one

L245 ↗

AlgebraicCurve.CurveModel.rank_kaehler_chartRing_localization_away_eq_one

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem rank_kaehler_chartRing_localization_away_eq_one [CharZero K]
    (s : L) [FiniteDimensional K⟮s⟯ L] (hs : Transcendental K s)
    (t : chartRing K ({s} : Set L)) (ht : t ≠ 0) :
    Module.rank (Localization.Away t) Ω[(Localization.Away t)⁄K] = 1

theorem

formallySmooth_chartRing

L269 ↗

AlgebraicCurve.CurveModel.formallySmooth_chartRing

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem formallySmooth_chartRing [CharZero K]
    (s : L) [FiniteDimensional K⟮s⟯ L] (hs : Transcendental K s) :
    FormallySmooth K (chartRing K ({s} : Set L))

theorem

locally_isStandardSmoothOfRelativeDimension_one_chartRing

L275 ↗

AlgebraicCurve.CurveModel.locally_isStandardSmoothOfRelativeDimension_one_chartRing

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem locally_isStandardSmoothOfRelativeDimension_one_chartRing [CharZero K]
    (s : L) [FiniteDimensional K⟮s⟯ L] (hs : Transcendental K s) :
    RingHom.Locally (RingHom.IsStandardSmoothOfRelativeDimension 1)
      (algebraMap K (chartRing K ({s} : Set L)))

theorem

smoothOfRelativeDimension_one_Spec_chartRing

L295 ↗

AlgebraicCurve.CurveModel.smoothOfRelativeDimension_one_Spec_chartRing

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry Polynomial MvPolynomial Algebra IntermediateField IsLocalRing
open IntermediateField.algebraAdjoinAdjoin TensorProduct
universe u
namespace AlgebraicCurve.CurveModel
variable (K : Type u) [Field K]
variable {L : Type u} [Field L] [Algebra K L]
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem smoothOfRelativeDimension_one_Spec_chartRing [CharZero K]
    (s : L) [FiniteDimensional K⟮s⟯ L] (hs : Transcendental K s) :
    SmoothOfRelativeDimension 1
      (Spec.map (CommRingCat.ofHom (algebraMap K (chartRing K ({s} : Set L)))))

Module documentation

Smoothness

Declarations