English
If the ranks of A and B are coprime and A,B satisfy certain freeness conditions, then A and B are linearly disjoint.
Русский
Если ранги A и B взаимно просты и выполняются некоторые условия свободы, то A и B линейно несвязаны.
LaTeX
$$$\\left( \\operatorname{finrank}_R(A) \\right) \\; \\mathrm{Coprime} \\; \\left( \\operatorname{finrank}_R(B) \\right) \\Rightarrow A \\mathrel{\\mathrm{LinearDisjoint}} B.$$$
Lean4
/-- If the rank of `A` and `B` are coprime, and they satisfy some freeness condition,
then `A` and `B` are linearly disjoint. -/
theorem of_finrank_coprime_of_free [Module.Free R A] [Module.Free R B] [Module.Free A (Algebra.adjoin A (B : Set S))]
[Module.Free B (Algebra.adjoin B (A : Set S))] (H : (Module.finrank R A).Coprime (Module.finrank R B)) :
A.LinearDisjoint B := by
nontriviality R
by_cases h1 : Module.finrank R A = 0
· rw [h1, Nat.coprime_zero_left] at H
rw [eq_bot_of_finrank_one H]
exact bot_right _
by_cases h2 : Module.finrank R B = 0
· rw [h2, Nat.coprime_zero_right] at H
rw [eq_bot_of_finrank_one H]
exact bot_left _
haveI := Module.finite_of_finrank_pos (Nat.pos_of_ne_zero h1)
haveI := Module.finite_of_finrank_pos (Nat.pos_of_ne_zero h2)
haveI := finite_sup A B
have : Module.finrank R A ≤ Module.finrank R ↥(A ⊔ B) :=
LinearMap.finrank_le_finrank_of_injective <|
Submodule.inclusion_injective (show toSubmodule A ≤ toSubmodule (A ⊔ B) by simp)
exact
of_finrank_sup_of_free <|
(finrank_sup_le_of_free A B).antisymm <|
Nat.le_of_dvd (lt_of_lt_of_le (Nat.pos_of_ne_zero h1) this) <|
H.mul_dvd_of_dvd_of_dvd (finrank_left_dvd_finrank_sup_of_free A B) (finrank_right_dvd_finrank_sup_of_free A B)
