AlgebraicCurve.exists_finiteDimensional_isSeparable_adjoin_of_constantFieldExtension_of_perfectField
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurve
open _root_.AlgebraicCurves.FunctionFields.Proofs in
open Exists_finiteDimensional_isSeparable_adjoin_of_constantFieldExtension_of_perfectField in
open IntermediateField inLean source · statement
theorem exists_finiteDimensional_isSeparable_adjoin_of_constantFieldExtension_of_perfectField
(K F K' F' : Type*)
[Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
[Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
[PerfectField K]
(hfg : ∃ x : F, Transcendental K x ∧
FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
(_hfg' : ∃ x : F', Transcendental K' x ∧
FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
(hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤) :
∃ t' : F', FiniteDimensional (IntermediateField.adjoin K' ({t'} : Set F')) F' ∧
Algebra.IsSeparable (IntermediateField.adjoin K' ({t'} : Set F')) F'