English
If A and B are free subalgebras of finite rank over R and the rank of their supremum A ⊔ B equals the product of their ranks, then A and B are linearly disjoint over R.
Русский
Если A и B — свободные подалгебры над R с конечной размерностью, и ранг их объединения A ⊔ B равен рангам A и B произведению, то A и B линейно несовместимы над R.
LaTeX
$$$\\displaystyle (\\operatorname{finrank}_R(A \\vee B) = \\operatorname{finrank}_R(A) \\cdot \\operatorname{finrank}_R(B)) \\Rightarrow A \\perp_{\\mathrm{lin}} B$$$
Lean4
/-- In a commutative ring, if `A` and `B` are subalgebras which are free modules of finite rank,
such that rank of `A ⊔ B` is equal to the product of the rank of `A` and `B`,
then `A` and `B` are linearly disjoint. -/
theorem of_finrank_sup_of_free [Module.Free R A] [Module.Free R B] [Module.Finite R A] [Module.Finite R B]
(H : Module.finrank R ↥(A ⊔ B) = Module.finrank R A * Module.finrank R B) : A.LinearDisjoint B :=
by
nontriviality R
rw [← Module.finrank_tensorProduct] at H
obtain ⟨j, hj⟩ := exists_linearIndependent_of_le_finrank H.ge
rw [LinearIndependent] at hj
let j' := Finsupp.linearCombination R j ∘ₗ (LinearEquiv.ofFinrankEq (A ⊗[R] B) _ (by simp)).toLinearMap
replace hj : Function.Injective j' := by simpa [j']
have hf : Function.Surjective (mulMap' A B).toLinearMap := mulMap'_surjective A B
haveI := Subalgebra.finite_sup A B
rw [linearDisjoint_iff, Submodule.linearDisjoint_iff]
exact Subtype.val_injective.comp (OrzechProperty.injective_of_surjective_of_injective j' _ hj hf)
