English
If at least one of E1 or E2 is algebraic over K, then the rank inequality for the join holds: rank(E1 ⊔ E2) ≤ rank(E1) × rank(E2).
Русский
Если хотя бы одно из E1 или E2 алгебраическое над K, верно неравенство рангов от объединения: rank(E1 ⊔ E2) ≤ rank(E1) × rank(E2).
LaTeX
$$$\text{If } E_1 \text{ or } E_2 \text{ is algebraic over } K, \; \operatorname{rank}_K(E_1 \sqcup E_2) \le \operatorname{rank}_K(E_1) \cdot \operatorname{rank}_K(E_2)$$$
Lean4
/-- If `E1` and `E2` are intermediate fields, then the `Module.finrank` of
the compositum of `E1` and `E2` is less than or equal to the product of that of `E1` and `E2`. -/
theorem finrank_sup_le : finrank K ↥(E1 ⊔ E2) ≤ finrank K E1 * finrank K E2 :=
by
by_cases h : FiniteDimensional K E1
· have := E1.toSubalgebra.finrank_sup_le_of_free E2.toSubalgebra
change _ ≤ finrank K E1 * finrank K E2 at this
rwa [← sup_toSubalgebra_of_left] at this
rw [FiniteDimensional, ← rank_lt_aleph0_iff, not_lt] at h
have :=
LinearMap.rank_le_of_injective _ <|
Submodule.inclusion_injective <|
show Subalgebra.toSubmodule E1.toSubalgebra ≤ Subalgebra.toSubmodule (E1 ⊔ E2).toSubalgebra by simp
rw [show finrank K E1 = 0 from Cardinal.toNat_apply_of_aleph0_le h,
show finrank K ↥(E1 ⊔ E2) = 0 from Cardinal.toNat_apply_of_aleph0_le (h.trans this), zero_mul]
