theorem weil_differentials_dim_eq_one {F : Type u_1} [Field F] {k : Type u_2} [Field k] [Algebra k F] {Ω : Type u_3} [AddCommGroup Ω] [Module F Ω] [Module k Ω] [Nontrivial Ω] (hsd : WeilDifferentialSubspaceData F k Ω) : Module.finrank F Ω = 1

Theorem 22.14. The space $\Omega$ of Weil differentials of the function field $F/k$ is a one-dimensional $F$-vector space: $\dim_F \Omega = 1$.

theorem weil_differentials_one_dim_basis {F : Type u_1} [Field F] {k : Type u_2} [Field k] [Algebra k F] {Ω : Type u_3} [AddCommGroup Ω] [Module F Ω] [Module k Ω] [Nontrivial Ω] (hsd : WeilDifferentialSubspaceData F k Ω) (ω₁ ω₂ : Ω) (hω₁ : ω₁ ≠ 0) (hω₂ : ω₂ ≠ 0) : ∃ (f : F), f ≠ 0 ∧ ω₂ = f • ω₁

Any two nonzero Weil differentials are proportional over $F$: there exists a nonzero scalar $f \in F$ with $\omega_2 = f \cdot \omega_1$.

theorem weil_differentials_span_singleton {F : Type u_1} [Field F] {k : Type u_2} [Field k] [Algebra k F] {Ω : Type u_3} [AddCommGroup Ω] [Module F Ω] [Module k Ω] [Nontrivial Ω] (hsd : WeilDifferentialSubspaceData F k Ω) (ω₀ : Ω) (hω₀ : ω₀ ≠ 0) (ω : Ω) : ∃ (f : F), ω = f • ω₀

Every Weil differential $\omega$ is an $F$-multiple of any fixed nonzero differential $\omega_0$.

theorem weil_differentials_faithful_action {F : Type u_1} [Field F] {k : Type u_2} [Field k] [Algebra k F] {Ω : Type u_3} [AddCommGroup Ω] [Module F Ω] [Module k Ω] (ω₀ : Ω) (hω₀ : ω₀ ≠ 0) (f : F) (hf : f • ω₀ = 0) : f = 0

The action of $F$ on a nonzero Weil differential is faithful: if $f \cdot \omega_0 = 0$ and $\omega_0 \neq 0$, then $f = 0$.