English
Let F and E be fields with E an algebra over F, and A, B be intermediate fields of E containing F. Then the F-rank (dimension) of the compositum A ⊔ B is at most the product of the F-ranks of A and B.
Русский
Пусть F и E — поля, E является расширением над F, а A, B — промежуточные поля E, содержащие F. Тогда ранг по F от объединения A ⊔ B не превосходит произведения рангов по F от A и по F от B.
LaTeX
$$$\operatorname{rank}_F \big( A \lor B \big) \le \operatorname{rank}_F(A) \cdot \operatorname{rank}_F(B)$$$
Lean4
theorem rank_sup_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
Module.rank F ↥(A ⊔ B) ≤ Module.rank F A * Module.rank F B :=
by
by_cases hA : Algebra.IsAlgebraic F A
· exact rank_sup_le_of_isAlgebraic A B (Or.inl hA)
by_cases hB : Algebra.IsAlgebraic F B
· exact rank_sup_le_of_isAlgebraic A B (Or.inr hB)
rw [← Algebra.transcendental_iff_not_isAlgebraic] at hA hB
haveI : Algebra.Transcendental F ↥(A ⊔ B) :=
.ringHom_of_comp_eq (RingHom.id F) (inclusion le_sup_left) Function.surjective_id (inclusion_injective _) rfl
haveI := Algebra.Transcendental.infinite F A
haveI := Algebra.Transcendental.infinite F B
simp_rw [Algebra.Transcendental.rank_eq_cardinalMk]
rw [sup_def, mul_mk_eq_max, ← Cardinal.lift_le.{u}]
refine (lift_cardinalMk_adjoin_le _ _).trans ?_
calc
_ ≤ Cardinal.lift.{v} #F ⊔ Cardinal.lift.{u} (#A ⊔ #B) ⊔ ℵ₀ :=
by
gcongr
rw [Cardinal.lift_le]
exact (mk_union_le _ _).trans_eq (by simp)
_ = _ := by simp [lift_mk_le_lift_mk_of_injective (algebraMap F A).injective]
