Transcendental separable extensions

In this file we introduce the concept of separably generated field extensions and transcendental separable field extensions.

Main definitions and results

• Algebra.IsSeparablyGenerated : A field extension is separably generated if there exists a transcendence basis such that the extension above it is separable.

• Algebra.IsTranscendentalSeparable : A field extension is transcendental separable if every finitely generated subextension is separably generated.

class Algebra.IsSeparablyGenerated (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : Prop

A field extension is separably generated if there exists a transcendence basis such that the extension above it is separable.

• isSeparable : ∃ (s : Set K), IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(IntermediateField.adjoin k s)) K

theorem Algebra.isSeparablyGenerated_iff (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : IsSeparablyGenerated k K ↔ ∃ (s : Set K), IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(IntermediateField.adjoin k s)) K

theorem AlgEquiv.isSeparablyGenerated {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {K' : Type u_3} [Field K'] [Algebra k K'] (e : K ≃ₐ[k] K') [Algebra.IsSeparablyGenerated k K] : Algebra.IsSeparablyGenerated k K'

theorem Algebra.isSeparable_iff_isSeparablyGenerated_and_isAlgebraic (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : Algebra.IsSeparable k K ↔ IsSeparablyGenerated k K ∧ Algebra.IsAlgebraic k K

@[instance 100]

instance instIsSeparablyGeneratedOfIsSeparable (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra.IsSeparable k K] : Algebra.IsSeparablyGenerated k K

instance instIsSeparablyGeneratedOfPerfectFieldOfEssFiniteType (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [PerfectField k] [Algebra.EssFiniteType k K] : Algebra.IsSeparablyGenerated k K

class Algebra.IsTranscendentalSeparable (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : Prop

A field extension is transcendental separable if every finitely generated subextension is separably generated.

• forall_isSeparablyGenerated (L : IntermediateField k K) : EssFiniteType k ↥L → IsSeparablyGenerated k ↥L

theorem Algebra.isTranscendentalSeparable_iff (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : IsTranscendentalSeparable k K ↔ ∀ (L : IntermediateField k K), EssFiniteType k ↥L → IsSeparablyGenerated k ↥L

theorem Algebra.isSeparable_iff_isTranscendentalSeparable_and_isAlgebraic (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : Algebra.IsSeparable k K ↔ IsTranscendentalSeparable k K ∧ Algebra.IsAlgebraic k K

@[instance 100]

instance instIsTranscendentalSeparableOfIsSeparable (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra.IsSeparable k K] : Algebra.IsTranscendentalSeparable k K

instance instIsTranscendentalSeparableOfPerfectField (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [PerfectField k] : Algebra.IsTranscendentalSeparable k K