NYLL
Module

Exists_separating_transcendental_of_perfectField.lean

Nyll.AlgebraicCurves.FunctionFields.Exists_separating_transcendental_of_perfectField
6 declarations indexed from sourceView source ↗

Module documentation

Exists separating transcendental of perfect Field

Imports2
Imported by18

Declarations

theorem

isTranscendenceBasis_of_transcendental

L31 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_separating_transcendental_of_perfectField.AlgebraicCurve.SeparatingTranscendentalOfPerfectField.isTranscendenceBasis_of_transcendental
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_separating_transcendental_of_perfectField
open IntermediateField
namespace AlgebraicCurve
namespace SeparatingTranscendentalOfPerfectField
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · full declaration
theorem isTranscendenceBasis_of_transcendental {x : F} (hx : Transcendental K x)
    (hfd : FiniteDimensional K⟮x⟯ F) : IsTranscendenceBasis K (fun _ : Fin 1 => x) := by
  have hind : AlgebraicIndependent K (fun _ : Fin 1 => x) :=
    algebraicIndependent_unique_type_iff.mpr hx
  refine hind.isTranscendenceBasis_iff_isAlgebraic.mpr ?_
  have hr : Set.range (fun _ : Fin 1 => x) = ({x} : Set F) := by
    ext y
    simp [eq_comm]
  rw [hr, ← IntermediateField.isAlgebraic_adjoin_iff_top]
  have := hfd
  exact Algebra.IsAlgebraic.of_finite K⟮x⟯ F
theorem

isAlgebraic_adjoin_of_transcendental

L43 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_separating_transcendental_of_perfectField.AlgebraicCurve.SeparatingTranscendentalOfPerfectField.isAlgebraic_adjoin_of_transcendental
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_separating_transcendental_of_perfectField
open IntermediateField
namespace AlgebraicCurve
namespace SeparatingTranscendentalOfPerfectField
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem isAlgebraic_adjoin_of_transcendental {x : F} (hx : Transcendental K x)
    (hfd : FiniteDimensional K⟮x⟯ F) {t : F} (ht : Transcendental K t) :
    Algebra.IsAlgebraic K⟮t⟯ F
theorem

finiteDimensional_adjoin_of_transcendental

L59 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_separating_transcendental_of_perfectField.AlgebraicCurve.SeparatingTranscendentalOfPerfectField.finiteDimensional_adjoin_of_transcendental
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_separating_transcendental_of_perfectField
open IntermediateField
namespace AlgebraicCurve
namespace SeparatingTranscendentalOfPerfectField
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem finiteDimensional_adjoin_of_transcendental {x : F} (hx : Transcendental K x)
    (hfd : FiniteDimensional K⟮x⟯ F) {t : F} (ht : Transcendental K t) :
    FiniteDimensional K⟮t⟯ F
theorem

transcendental_of_not_mem_fieldRange_frobenius

L101 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_separating_transcendental_of_perfectField.AlgebraicCurve.SeparatingTranscendentalOfPerfectField.transcendental_of_not_mem_fieldRange_frobenius
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_separating_transcendental_of_perfectField
open IntermediateField
namespace AlgebraicCurve
namespace SeparatingTranscendentalOfPerfectField
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem transcendental_of_not_mem_fieldRange_frobenius [PerfectField K] (p : ℕ)
    [Fact p.Prime] [CharP K p] [CharP F p] {t : F} (ht : t ∉ (frobenius F p).fieldRange) :
    Transcendental K t
theorem

exists_separating

L115 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_separating_transcendental_of_perfectField.AlgebraicCurve.SeparatingTranscendentalOfPerfectField.exists_separating
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_separating_transcendental_of_perfectField
open IntermediateField
namespace AlgebraicCurve
namespace SeparatingTranscendentalOfPerfectField
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_separating [PerfectField K] {x : F} (hx : Transcendental K x)
    (hfd : FiniteDimensional K⟮x⟯ F) :
    ∃ t : F, Transcendental K t ∧ FiniteDimensional K⟮t⟯ F ∧ Algebra.IsSeparable K⟮t⟯ F
theorem

exists_separating_transcendental_of_perfectField

L147 ↗
AlgebraicCurve.exists_separating_transcendental_of_perfectField
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_separating_transcendental_of_perfectField
open IntermediateField
Lean source · statement
theorem _root_.AlgebraicCurve.exists_separating_transcendental_of_perfectField
    {K F : Type*} [Field K] [Field F] [Algebra K F] [PerfectField K]
    {x : F} (htr : Transcendental K x)
    (hfd : FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F) :
    ∃ t : F, Transcendental K t ∧
      FiniteDimensional (IntermediateField.adjoin K ({t} : Set F)) F ∧
      Algebra.IsSeparable (IntermediateField.adjoin K ({t} : Set F)) F

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