English
If A,B are linearly disjoint and one of them is flat, the rank of A ∩ B is 1 under injectivity and commutativity conditions.
Русский
Если A и B линейно несовместимы и хотя бы одна из них плоская, ранг пересечения A ∩ B равен 1 при выполнении условий коммутативности и инъекции.
LaTeX
$$$A \\perp_L B \\land \\bigl(\\mathbf{Flat}_R(A) \\lor \\mathbf{Flat}_R(B)\\bigr) \\Rightarrow (\\forall a,b \\in A\\cap B, \\, [a,b]=0) \\Rightarrow \\text{inj}(\\text{algebraMap}) \\Rightarrow \\operatorname{rank}_R(A\\cap B)=1$$$
Lean4
theorem rank_inf_eq_one_of_commute_of_flat_of_inj (hf : Module.Flat R A ∨ Module.Flat R B)
(hc : ∀ (a b : ↥(A ⊓ B)), Commute a.1 b.1) (hinj : Function.Injective (algebraMap R S)) :
Module.rank R ↥(A ⊓ B) = 1 := by
nontriviality R
refine le_antisymm (Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat H hf hc) ?_
have : Cardinal.lift.{u} (Module.rank R (⊥ : Subalgebra R S)) = Cardinal.lift.{v} (Module.rank R R) :=
lift_rank_range_of_injective (Algebra.linearMap R S) hinj
rw [Module.rank_self, Cardinal.lift_one, Cardinal.lift_eq_one] at this
rw [← this]
change Module.rank R (toSubmodule (⊥ : Subalgebra R S)) ≤ Module.rank R (toSubmodule (A ⊓ B))
exact Submodule.rank_mono (bot_le : (⊥ : Subalgebra R S) ≤ A ⊓ B)
