English
If A and A' are FG subalgebras of S, and t ∈ A ⊗(Subtype) N, t' ∈ A' ⊗(Subtype) N satisfy the rTensor equality, then there exists B with hAB, hA'B, FG(B) such that the two rTensor images are equal after inclusion.
Русский
Если A и A' — FG-подалгебры S, и т и т' из соответствующих тензорных произведений удовлетворяют равенству образов, то есть существует B с FG, включениями, для которых тензорные изображения совпадают.
LaTeX
$$$\exists B (hAB : A \le B) (hA'B : A' \le B), FG(B) \land rTensor N (Subalgebra.inclusion hAB).toLinearMap t = rTensor N (Subalgebra.inclusion hA'B).toLinearMap t'.$$$
Lean4
theorem exists_fg_le_subset_range_rTensor_inclusion (s : Set (I ⊗[R] M)) (hs : s.Finite) :
∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I), s ⊆ LinearMap.range (rTensor M (J.inclusion hle)) :=
by
choose J fg hle y eq using exists_fg_le_eq_rTensor_inclusion (M := M) (I := I)
rw [← Set.finite_coe_iff] at hs
refine
⟨⨆ x : s, J x, fg_iSup _ fun _ ↦ fg _, iSup_le fun _ ↦ hle _, fun x hx ↦
⟨rTensor M (inclusion <| le_iSup _ ⟨x, hx⟩) (y x), .trans ?_ (eq x).symm⟩⟩
rw [← comp_apply, ← rTensor_comp]; rfl
