English
Let f: M → N be linear, and t ∈ S ⊗R M such that f.baseChange S t = 0. Then there exists a finitely generated subalgebra A ⊆ S and u ∈ A ⊗R M with f.baseChange A u = 0 and A.val.toLinearMap.rTensor M u = t.
Русский
Пусть f: M → N линейно, и некоторый элемент t в S⊗R M так, что при базовом изменении равен нулю; тогда существует конечная FG-подалгебра A и элемент u, удовлетворяющие аналогичным условиям.
LaTeX
$$$\exists A \,(hA : A.FG) (u : A ⊗R M),\ f.baseChange A u = 0 \land A.val.toLinearMap.rTensor M u = t.$$$
Lean4
/-- Every `x : N ⊗ M` is the image of some `y : J ⊗ M`, where `J` is a finitely generated
submodule of `N`, under the tensor product of the inclusion `J → N` and the identity `M → M`. -/
theorem exists_fg_le_eq_rTensor_subtype (x : N ⊗ M) :
∃ (J : Submodule R N) (_ : J.FG) (y : J ⊗ M), x = rTensor M J.subtype y := by
induction x with
| zero => exact ⟨⊥, fg_bot, 0, rfl⟩
| tmul i m => exact ⟨R ∙ i, fg_span_singleton i, ⟨i, mem_span_singleton_self _⟩ ⊗ₜ[R] m, rfl⟩
| add x₁ x₂ ihx₁ ihx₂ =>
obtain ⟨J₁, fg₁, y₁, rfl⟩ := ihx₁
obtain ⟨J₂, fg₂, y₂, rfl⟩ := ihx₂
refine
⟨J₁ ⊔ J₂, fg₁.sup fg₂, rTensor M (J₁.inclusion le_sup_left) y₁ + rTensor M (J₂.inclusion le_sup_right) y₂, ?_⟩
rw [map_add, ← rTensor_comp_apply, ← rTensor_comp_apply]
rfl
