English
If E/F is a separable extension, then finSepDegree F E = finrank F E.
Русский
Если расширение E/F является сепарабельным, то finSepDegree F E = finrank F E.
LaTeX
$$$ finSepDegree F E = finrank F E $$$
Lean4
/-- If `E / F` is a separable extension, then its separable degree is equal to its degree.
When `E / F` is infinite, it means that `Field.Emb F E` has infinitely many elements.
(But the cardinality of `Field.Emb F E` is not equal to `Module.rank F E` in general!) -/
theorem finSepDegree_eq_finrank_of_isSeparable [Algebra.IsSeparable F E] : finSepDegree F E = finrank F E :=
by
wlog hfd : FiniteDimensional F E generalizing E with H
· rw [finrank_of_infinite_dimensional hfd]
obtain ⟨L, h, h'⟩ := exists_lt_finrank_of_infinite_dimensional hfd (finSepDegree F E)
have hd := finSepDegree_mul_finSepDegree_of_isAlgebraic F L E
rw [H L h] at hd
by_cases hd' : finSepDegree L E = 0
· rw [← hd, hd', mul_zero]
linarith only [h', hd, Nat.le_mul_of_pos_right (finrank F L) (Nat.pos_of_ne_zero hd')]
rw [← finSepDegree_top F, ← finrank_top F E]
refine
induction_on_adjoin (fun K : IntermediateField F E ↦ finSepDegree F K = finrank F K)
(by simp_rw [finSepDegree_bot, IntermediateField.finrank_bot]) (fun L x h ↦ ?_) ⊤
simp only at h ⊢
have heq : _ * _ = _ * _ :=
congr_arg₂ (· * ·) h <|
(finSepDegree_adjoin_simple_eq_finrank_iff L E x (IsAlgebraic.of_finite L x)).2 <|
IsSeparable.tower_top L (Algebra.IsSeparable.isSeparable F x)
set M := L⟮x⟯
rwa [finSepDegree_mul_finSepDegree_of_isAlgebraic F L M, Module.finrank_mul_finrank F L M] at heq
