English
If E/F is purely inseparable and finite-dimensional, then there exists n with finrank_F E = q^n, where q is the characteristic exponent.
Русский
Если расширение E/F чисто безразделимо и конечномерно, существует n такое, что finrank_F E = q^n, где q — характеристика.
LaTeX
$$$ \exists n:\, \mathbb{N}, \ \operatorname{finrank}_F E = q^n$$$
Lean4
theorem finrank_eq_pow (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E] :
∃ n, finrank F E = q ^ n :=
by
suffices
∀ (F E : Type v) [Field F] [Field E] [Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E]
[FiniteDimensional F E], ∃ n, finrank F E = q ^ n
by simpa using this (⊥ : IntermediateField F E) E q
intro F E _ _ _ q _ _ _
generalize hd : finrank F E = d
induction d using Nat.strongRecOn generalizing F with
| ind d IH =>
by_cases h : (⊥ : IntermediateField F E) = ⊤
· rw [← finrank_top', ← h, IntermediateField.finrank_bot] at hd
exact ⟨0, ((pow_zero q).trans hd).symm⟩
obtain ⟨x, -, hx⟩ := SetLike.exists_of_lt (lt_of_le_of_ne bot_le h :)
obtain ⟨m, y, e⟩ := IsPurelyInseparable.minpoly_eq_X_pow_sub_C F q x
have : finrank F F⟮x⟯ = q ^ m := by
rw [adjoin.finrank (Algebra.IsIntegral.isIntegral x), e, natDegree_sub_C, natDegree_X_pow]
obtain ⟨n, hn⟩ :=
IH _
(by
rw [← hd, ← finrank_mul_finrank F F⟮x⟯, Nat.lt_mul_iff_one_lt_left finrank_pos, this]
by_contra! H
refine hx (finrank_adjoin_simple_eq_one_iff.mp (le_antisymm (this ▸ H) ?_))
exact Nat.one_le_iff_ne_zero.mpr Module.finrank_pos.ne')
(F⟮x⟯) rfl
exact ⟨m + n, by rw [← hd, ← finrank_mul_finrank F F⟮x⟯, hn, pow_add, this]⟩
