English
If A and L are linearly disjoint over F and one of A or L is algebraic over F, then the rank of the adjoin of A to L over L equals the rank of A over F: [L(A) : L] = [A : F].
Русский
Если A и L линейно независимы над F и либо A, либо L алгебраически над F, тогда ранг присоединения A к L над L равен рангу A над F.
LaTeX
$$$\operatorname{rank}_L(\operatorname{adjoin}__L(A)) = \operatorname{rank}_F(A)$$
Lean4
/-- If `A` and `L` are linearly disjoint over `F`, one of them is algebraic,
then `[L(A) : L] = [A : F]`. -/
theorem adjoin_rank_eq_rank_left_of_isAlgebraic (H : A.LinearDisjoint L)
(halg : Algebra.IsAlgebraic F A ∨ Algebra.IsAlgebraic F L) :
Module.rank L (adjoin L (A : Set E)) = Module.rank F A :=
by
refine Eq.trans ?_ (Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left H)
set L' := (IsScalarTower.toAlgHom F L E).range
let i : L ≃ₐ[F] L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
have heq : (adjoin L (A : Set E)).toSubalgebra.toSubsemiring = (Algebra.adjoin L' (A : Set E)).toSubsemiring :=
by
rw [adjoin_toSubalgebra_of_isAlgebraic _ _ halg.symm, Algebra.adjoin_toSubsemiring, Algebra.adjoin_toSubsemiring]
congr 2
ext x
simp only [Set.mem_range, Subtype.exists]
exact ⟨fun ⟨y, h⟩ ↦ ⟨x, ⟨y, h⟩, rfl⟩, fun ⟨a, ⟨y, h1⟩, h2⟩ ↦ ⟨y, h1.trans h2⟩⟩
refine rank_eq_of_equiv_equiv i (RingEquiv.subsemiringCongr heq).toAddEquiv i.bijective fun a ⟨x, hx⟩ ↦ ?_
ext
simp_rw [Algebra.smul_def]
rfl
