Smooth algebras over fields

We show that separably generated extensions of fields are smooth. In particular finitely generated field extensions over perfect fields are smooth.

theorem Algebra.FormallySmooth.adjoin_of_algebraicIndependent {K : Type u_1} {L : Type u_2} {ι : Type u_3} [Field L] [Field K] [Algebra K L] {v : ι → L} (hb : AlgebraicIndependent K v) : FormallySmooth K ↥(IntermediateField.adjoin K (Set.range v))

theorem Algebra.FormallySmooth.of_algebraicIndependent {K : Type u_1} {L : Type u_2} {ι : Type u_3} [Field L] [Field K] [Algebra K L] {v : ι → L} (hb : AlgebraicIndependent K v) (hb' : IntermediateField.adjoin K (Set.range v) = ⊤) : FormallySmooth K L

Purely transcendental extensions are formally smooth.

theorem Algebra.FormallySmooth.of_algebraicIndependent_of_isSeparable {K : Type u_1} {L : Type u_2} {ι : Type u_3} [Field L] [Field K] [Algebra K L] [EssFiniteType K L] {v : ι → L} (hb : AlgebraicIndependent K v) [Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range v))) L] : FormallySmooth K L

Separably generated extensions are formally smooth.

@[instance 100]

instance Algebra.FormallySmooth.of_perfectField {K : Type u_1} {L : Type u_2} [Field L] [Field K] [Algebra K L] [PerfectField K] [EssFiniteType K L] : FormallySmooth K L