English
If A and B are linearly disjoint, A is free, and B is flat, then the rank of Adjoin_B(A) equals the rank of A over R.
Русский
Если A и B линейно независимы, A свободен, а B плосок, то ранг присоединения A к B равен рангу A над R.
LaTeX
$$$\\operatorname{rank}_B\\big(\\operatorname{Algebra.adjoin}_B(A)\\big) = \\operatorname{rank}_R(A).$$$
Lean4
/-- If `A` and `B` are linearly disjoint, if `A` is free and `B` is flat,
then `[B[A] : B] = [A : R]`. See also `Subalgebra.adjoin_rank_le`. -/
theorem adjoin_rank_eq_rank_left [Module.Free R A] [Module.Flat R B] [Nontrivial R] [Nontrivial S] :
Module.rank B (Algebra.adjoin B (A : Set S)) = Module.rank R A :=
by
rw [← rank_toSubmodule, Module.Free.rank_eq_card_chooseBasisIndex R A,
A.adjoin_eq_span_basis B (Module.Free.chooseBasis R A)]
change Module.rank B (Submodule.span B (Set.range (A.val ∘ Module.Free.chooseBasis R A))) = _
have := H.linearIndependent_left_of_flat (Module.Free.chooseBasis R A).linearIndependent
rw [rank_span this, Cardinal.mk_range_eq _ this.injective]
