English
If A is integral over R and for every finitely generated subalgebra A' of A, A' is linearly disjoint from B, then A is linearly disjoint from B.
Русский
Если A интегралы над R и для каждого конечного подалгебра A' ⊆ A A' линейно несвязана с B, тогда A линейно несвязана с B.
LaTeX
$$$\\operatorname{IsIntegral}_R(A) \\land \\left( \\forall A'\\le A, \\; [\\operatorname{Module.Finite}_R(A')] \\Rightarrow A'\\mathrel{\\mathrm{LinearDisjoint}} B \\right) \\Rightarrow A \\mathrel{\\mathrm{LinearDisjoint}} B.$$$
Lean4
/-- If `A/R` is integral, such that `A'` and `B` are linearly disjoint for all subalgebras `A'`
of `A` which are finitely generated `R`-modules, then `A` and `B` are linearly disjoint. -/
theorem of_linearDisjoint_finite_left [Algebra.IsIntegral R A]
(H : ∀ A' : Subalgebra R S, A' ≤ A → [Module.Finite R A'] → A'.LinearDisjoint B) : A.LinearDisjoint B :=
by
rw [linearDisjoint_iff, Submodule.linearDisjoint_iff]
intro x y hxy
obtain ⟨M', hM, hf, h⟩ := TensorProduct.exists_finite_submodule_left_of_setFinite' { x, y } (Set.toFinite _)
obtain ⟨s, hs⟩ := Module.Finite.iff_fg.1 hf
have hs' : (s : Set S) ⊆ A := by rwa [← hs, Submodule.span_le] at hM
let A' := Algebra.adjoin R (s : Set S)
have hf' : Submodule.FG (toSubmodule A') :=
fg_adjoin_of_finite s.finite_toSet fun x hx ↦
(isIntegral_algHom_iff A.val Subtype.val_injective).2
(Algebra.IsIntegral.isIntegral (R := R) (A := A) ⟨x, hs' hx⟩)
replace hf' : Module.Finite R A' := Module.Finite.iff_fg.2 hf'
have hA : toSubmodule A' ≤ toSubmodule A := Algebra.adjoin_le_iff.2 hs'
replace h : { x, y } ⊆ (LinearMap.range (LinearMap.rTensor (toSubmodule B) (Submodule.inclusion hA)) : Set _) :=
fun _ hx ↦
by
have :
Submodule.inclusion hM =
Submodule.inclusion hA ∘ₗ
Submodule.inclusion
(show M' ≤ toSubmodule A' by rw [← hs, Submodule.span_le]; exact Algebra.adjoin_le_iff.1 (le_refl _)) :=
rfl
rw [this, LinearMap.rTensor_comp] at h
exact LinearMap.range_comp_le_range _ _ (h hx)
obtain ⟨x', hx'⟩ := h (show x ∈ { x, y } by simp)
obtain ⟨y', hy'⟩ := h (show y ∈ { x, y } by simp)
rw [← hx', ← hy']; congr
exact (H A' hA).injective (by simp [← Submodule.mulMap_comp_rTensor _ hA, hx', hy', hxy])
