Kähler differentials

TheoremDifferential of a transcendental element is nonzero#✓fully proved

The differential of a transcendental separable element is nonzero.

theorem D_ne_zero_of_transcendental (K : Type*) [Field K] {F : Type*} [Field F]
    [Algebra K F] (x : F) (hx : Transcendental K x)
    [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F] :
    KaehlerDifferential.D K F x ≠ 0

Used by 1

Used byKähler differentials are unique multiples of dt for transcendental t

TheoremDifferential of a transcendental element spans the differentials#✓fully proved

The differential of a transcendental separable element spans the Kähler differentials.

theorem span_D_eq_top_of_transcendental (K : Type*) [Field K] {F : Type*} [Field F]
    [Algebra K F] (x : F) (hx : Transcendental K x)
    [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F] :
    Submodule.span F ({KaehlerDifferential.D K F x} : Set (KaehlerDifferential K F)) = ⊤

Used by 1

Used byKähler differentials are unique multiples of dt for transcendental t

TheoremKähler differentials are unique multiples of dt for transcendental t#✓fully proved

Every Kähler differential is uniquely a scalar multiple of the differential of a transcendental separable element.

theorem exists_unique_smul_D_of_transcendental (K : Type*) [Field K] {F : Type*}
    [Field F] [Algebra K F] (x : F) (hx : Transcendental K x)
    [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F]
    (ω : KaehlerDifferential K F) :
    ∃! c : F, ω = c • KaehlerDifferential.D K F x

Uses 2

Proof usesDifferential of a transcendental element is nonzero · Differential of a transcendental element spans the differentials

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.