English
If A,B are subalgebras of S with suitable freeness hypotheses over R, then the rank of their join satisfies a multiplicative formula: rank_R(A ⊔ B) = rank_R A · rank_A(Algebra.adjoin_A(B)).
Русский
Если A и B — подалгебры S, удовлетворяющие достаточным условиям свободы над R, то число ранга суммасоединения равна произведению ранга: rank_R(A ⊔ B) = rank_R A · rank_A(adjoin_A(B)).
LaTeX
$$rank_sup_eq_rank_left_mul_rank_of_free : Module.rank R ↥(A ⊔ B) = Module.rank R A * Module.rank A (Algebra.adjoin A (B : Set S))$$
Lean4
theorem rank_sup_eq_rank_left_mul_rank_of_free :
Module.rank R ↥(A ⊔ B) = Module.rank R A * Module.rank A (Algebra.adjoin A (B : Set S)) :=
by
rcases subsingleton_or_nontrivial R with _ | _
· haveI := Module.subsingleton R S; simp
nontriviality S using rank_subsingleton'
letI : Algebra A (Algebra.adjoin A (B : Set S)) := Subalgebra.algebra _
letI : SMul A (Algebra.adjoin A (B : Set S)) := Algebra.toSMul
haveI : IsScalarTower R A (Algebra.adjoin A (B : Set S)) := IsScalarTower.of_algebraMap_eq (congrFun rfl)
rw [rank_mul_rank R A (Algebra.adjoin A (B : Set S))]
change _ = Module.rank R ((Algebra.adjoin A (B : Set S)).restrictScalars R)
rw [Algebra.restrictScalars_adjoin]; rfl
