Kähler differentials of separable elements #
This file records how the universal derivation detects separability and transcendence for field extensions.
Main results #
TauCeti.D_eq_zero_of_isSeparable: a separable algebraic element has vanishing differential.TauCeti.transcendental_of_D_ne_zero: over a perfect base field, an element with nonzero differential is transcendental.
theorem
TauCeti.D_eq_zero_of_isSeparable
{k : Type u_1}
{F : Type u_2}
[Field k]
[Field F]
[Algebra k F]
{x : F}
(hx : IsSeparable k x)
:
A separable algebraic element has vanishing universal differential, so the universal derivation detects only the inseparable or transcendental part of an extension.
theorem
TauCeti.transcendental_of_D_ne_zero
{k : Type u_1}
{F : Type u_2}
[Field k]
[Field F]
[Algebra k F]
{x : F}
[PerfectField k]
(hx : (KaehlerDifferential.D k F) x ≠ 0)
:
Transcendental k x
Over a perfect base field, an element with nonzero universal differential is transcendental: an algebraic element is separable, hence has vanishing differential.