English
Given A, A' FG, if t ∈ A ⊗R N and t' ∈ A' ⊗R N satisfy the equality of their rTensor images, there exists B ⊇ A, B ⊇ A' with FG such that the rTensor of t and t' coincide after inclusion to B.
Русский
Пусть A и A' — FG, и т, т' удовлетворяют равенству образов под тензорированием; найдется B, FG, включение которого объединяет A и A', при этом тензорное отображение совпадает.
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
/-- Lift an element that maps to 0 -/
theorem exists_fg_of_baseChange_eq_zero (f : M →ₗ[R] N) {t : S ⊗[R] M} (ht : f.baseChange S t = 0) :
∃ (A : Subalgebra R S) (_ : A.FG) (u : A ⊗[R] M), f.baseChange A u = 0 ∧ A.val.toLinearMap.rTensor M u = t := by
classical
obtain ⟨A, hA, ht_memA⟩ := TensorProduct.Algebra.exists_of_fg t
obtain ⟨u, hu⟩ := _root_.id ht_memA
have := TensorProduct.Algebra.eq_of_fg_of_subtype_eq hA (t := f.baseChange _ u) (t' := 0)
simp only [map_zero, exists_and_left] at this
have hu' : (A.val.toLinearMap.rTensor N) (f.baseChange (↥A) u) = 0 := by rw [← ht, ← hu, rTensor_baseChange]
obtain ⟨B, hB, hAB, hu'⟩ := this hu'
use B, hB, rTensor M (Subalgebra.inclusion hAB).toLinearMap u
constructor
· rw [← rTensor_baseChange, hu']
· rw [← comp_apply, ← rTensor_comp, ← hu]
congr
