NYLL
Module

IsCurveOver_exists_separating_transcendental.lean

Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_exists_separating_transcendental
16 declarations indexed from sourceView source ↗

Module documentation

IsCurveOver exists separating transcendental

A curve function field over a perfect field admits a separating transcendental element, with bases of differentials transported through the generated intermediate field.

Imports11
Imported by37

Declarations

theorem

not_isSeparable

L50 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.IsCurveOver.not_isSeparable
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem not_isSeparable [IsCurveOver K F] : ¬ Algebra.IsSeparable K F
theorem

not_isAlgebraic

L55 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.IsCurveOver.not_isAlgebraic
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem not_isAlgebraic [PerfectField K] [IsCurveOver K F] :
    ¬ Algebra.IsAlgebraic K F
instance

instTranscendental

L60 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.IsCurveOver.instTranscendental
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
instance instTranscendental [PerfectField K] [IsCurveOver K F] :
    Algebra.Transcendental K F
theorem

exists_transcendental

L64 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.IsCurveOver.exists_transcendental
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_transcendental [PerfectField K] [IsCurveOver K F] :
    ∃ t : F, Transcendental K t
theorem

trdeg_pos

L68 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.IsCurveOver.trdeg_pos
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem trdeg_pos [PerfectField K] [IsCurveOver K F] :
    0 < Algebra.trdeg K F
theorem

trdeg_ne_zero

L72 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.IsCurveOver.trdeg_ne_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem trdeg_ne_zero [PerfectField K] [IsCurveOver K F] :
    Algebra.trdeg K F ≠ 0
theorem

one_le_trdeg

L76 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.IsCurveOver.one_le_trdeg
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem one_le_trdeg [PerfectField K] [IsCurveOver K F] :
    1 ≤ Algebra.trdeg K F
theorem

trdeg_eq_one

L88 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.IsCurveOver.trdeg_eq_one
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.IsCurveOver in
Lean source · statement
theorem IsCurveOver.trdeg_eq_one [PerfectField K] [IsCurveOver K F]
    (htrdeg : Algebra.trdeg K F ≤ 1) :
    Algebra.trdeg K F = 1
def

kaehlerAdjoinBasis

L116 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.kaehlerAdjoinBasis
Documentation

The differential basis indexed by an algebraically independent family in its generated field.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
noncomputable section
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
open _root_.Module
open scoped IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
universe u₁ u₂
variable {K : Type u₁} {F : Type u₂} [Field K] [Field F] [Algebra K F]
variable {ι : Type*} {v : ι → F}
Lean source · statement
def kaehlerAdjoinBasis (hv : AlgebraicIndependent K v) :
    Basis ι (IntermediateField.adjoin K (Set.range v))
      Ω[(IntermediateField.adjoin K (Set.range v))⁄K]
def

kaehlerOfSeparatingTranscendentalBasis

L137 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.kaehlerOfSeparatingTranscendentalBasis
Documentation

The differential basis transported along the finite separable extension of the generated field.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
noncomputable section
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
open _root_.Module
open scoped IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
universe u₁ u₂
variable {K : Type u₁} {F : Type u₂} [Field K] [Field F] [Algebra K F]
variable {ι : Type*} {v : ι → F}
Lean source · statement
def kaehlerOfSeparatingTranscendentalBasis (hv : AlgebraicIndependent K v)
    [Algebra.IsSeparable (IntermediateField.adjoin K (Set.range v)) F] : Basis ι F Ω[F⁄K]
theorem

finrank_kaehler_eq_card_of_separating

L145 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.finrank_kaehler_eq_card_of_separating
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
noncomputable section
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
open _root_.Module
open scoped IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
universe u₁ u₂
variable {K : Type u₁} {F : Type u₂} [Field K] [Field F] [Algebra K F]
variable {ι : Type*} {v : ι → F}
Lean source · statement
theorem finrank_kaehler_eq_card_of_separating {s : Finset F}
    (hs : AlgebraicIndependent K ((↑) : s → F))
    [Algebra.IsSeparable (IntermediateField.adjoin K (Set.range ((↑) : s → F))) F] :
    Module.finrank F Ω[F⁄K] = s.card
theorem

finrank_kaehler_eq_card_of_separating'

L152 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.finrank_kaehler_eq_card_of_separating'
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
noncomputable section
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
open _root_.Module
open scoped IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
universe u₁ u₂
variable {K : Type u₁} {F : Type u₂} [Field K] [Field F] [Algebra K F]
variable {ι : Type*} {v : ι → F}
Lean source · statement
theorem finrank_kaehler_eq_card_of_separating' {s : Finset F}
    (hs : AlgebraicIndependent K ((↑) : s → F))
    [hsep : Algebra.IsSeparable (IntermediateField.adjoin K (s : Set F)) F] :
    Module.finrank F Ω[F⁄K] = s.card
theorem

trdeg_le_one

L171 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.IsCurveOver.trdeg_le_one
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
noncomputable section
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
open _root_.Module
open scoped IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
universe u₁ u₂
variable {K : Type u₁} {F : Type u₂} [Field K] [Field F] [Algebra K F]
variable {ι : Type*} {v : ι → F}
namespace IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
Lean source · statement
theorem trdeg_le_one [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F] :
    Algebra.trdeg K F ≤ 1
theorem

trdeg_eq_one_of_perfectField

L181 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.IsCurveOver.trdeg_eq_one_of_perfectField
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
noncomputable section
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
open _root_.Module
open scoped IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
universe u₁ u₂
variable {K : Type u₁} {F : Type u₂} [Field K] [Field F] [Algebra K F]
variable {ι : Type*} {v : ι → F}
namespace IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
Lean source · statement
theorem trdeg_eq_one_of_perfectField [PerfectField K] [Algebra.EssFiniteType K F]
    [IsCurveOver K F] : Algebra.trdeg K F = 1
theorem

exists_separating_transcendental_s6

L206 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental.AlgebraicCurve.IsCurveOver.exists_separating_transcendental_s6
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
noncomputable section
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
open _root_.Module
open scoped IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.Algebra
open _root_.TensorProduct.Algebra
open _root_.Algebra.TensorProduct.Algebra
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
universe u₁ u₂
variable {K : Type u₁} {F : Type u₂} [Field K] [Field F] [Algebra K F]
namespace IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
open _root_.AlgebraicCurve.IsCurveOver
Lean source · statement
theorem exists_separating_transcendental_s6 [PerfectField K] [Algebra.EssFiniteType K F]
    [IsCurveOver K F] :
    ∃ t : F, Transcendental K t ∧ FiniteDimensional K⟮t⟯ F ∧ Algebra.IsSeparable K⟮t⟯ F
theorem

exists_separating_transcendental

L235 ↗
AlgebraicCurve.IsCurveOver.exists_separating_transcendental
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_exists_separating_transcendental
noncomputable section
open KaehlerDifferential Algebra IntermediateField
noncomputable section
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
open _root_.Module
open scoped IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.Algebra
open _root_.TensorProduct.Algebra
open _root_.Algebra.TensorProduct.Algebra
open IntermediateField _root_.Algebra _root_.TensorProduct.Algebra
  _root_.Algebra.TensorProduct.Algebra in
Lean source · statement
theorem _root_.AlgebraicCurve.IsCurveOver.exists_separating_transcendental {K : Type*} {F :
  Type*} [Field K] [Field F] [Algebra K F]
    [PerfectField K] [Algebra.EssFiniteType K F] [AlgebraicCurve.IsCurveOver K F] :
    ∃ t : F, Transcendental K t ∧ FiniteDimensional K⟮t⟯ F ∧ Algebra.IsSeparable K⟮t⟯ F

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.