English
If A and A' are finitely generated subalgebras over R of S, and t ∈ A ⊗R N, t' ∈ A' ⊗R N satisfy rTensor_N A⋅toLinearMap t = rTensor_N A'⋅toLinearMap t', then there exists a finitely generated B ⊇ A, B ⊇ A' such that the induced rTensor maps agree on t and t'.
Русский
Если A и A' — FG-подалгебры S над R и существуют т, t' в соответствующих тензорных произведениях, удовлетворяющие равенству тензоров, то существует общая FG-подалгебра B, содержащая обе, для которой тензорные отображения совпадают.
LaTeX
$$$\exists B \,(hAB : A \le B) (hA''B : A' \le B),\ Subalgebra.FG B \land rTensor N (Subalgebra.inclusion hAB).toLinearMap t = rTensor N (Subalgebra.inclusion hA''B).toLinearMap t'.$$$
Lean4
theorem eq_of_fg_of_subtype_eq' {t' : A' ⊗[R] N} (h : rTensor N A.val.toLinearMap t = rTensor N A'.val.toLinearMap t') :
∃ (B : Subalgebra R S) (hAB : A ≤ B) (hA'B : A' ≤ B),
Subalgebra.FG B ∧
rTensor N (Subalgebra.inclusion hAB).toLinearMap t = rTensor N (Subalgebra.inclusion hA'B).toLinearMap t' :=
by
have hj : (A ⊔ A').val.comp (Subalgebra.inclusion le_sup_left) = A.val := by ext; rfl
have hj' : (A ⊔ A').val.comp (Subalgebra.inclusion le_sup_right) = A'.val := by ext; rfl
simp only [← hj, ← hj', AlgHom.comp_toLinearMap, rTensor_comp, comp_apply] at h
let ⟨B, hB_le, hB, h⟩ := TensorProduct.Algebra.eq_of_fg_of_subtype_eq (Subalgebra.FG.sup hA hA') h
use B, le_trans le_sup_left hB_le, le_trans le_sup_right hB_le, hB
simpa only [← rTensor_comp, ← comp_apply] using h
