English
For a submodule N of a finite module M, the image of N under the canonical map into the tensor product with the residue field is the whole tensor product iff N = M.
Русский
Для подсо модуля N ⊆ M, образ N в k ⊗_R M под каноническим отображением равен всему тензорному произведению тогда и только тогда, когда N = M.
LaTeX
$$$ N.map (TensorProduct.mk R k M 1) = \top \iff N = \top. $$$
Lean4
theorem map_tensorProduct_mk_eq_top {N : Submodule R M} [Module.Finite R M] :
N.map (TensorProduct.mk R k M 1) = ⊤ ↔ N = ⊤ := by
constructor
· intro hN
letI : Module k (M ⧸ (𝔪 • ⊤ : Submodule R M)) := inferInstanceAs (Module (R ⧸ 𝔪) (M ⧸ 𝔪 • (⊤ : Submodule R M)))
letI : IsScalarTower R k (M ⧸ (𝔪 • ⊤ : Submodule R M)) :=
inferInstanceAs (IsScalarTower R (R ⧸ 𝔪) (M ⧸ 𝔪 • (⊤ : Submodule R M)))
let f :=
AlgebraTensorModule.lift
(((LinearMap.ringLmapEquivSelf k k _).symm (Submodule.mkQ (𝔪 • ⊤ : Submodule R M))).restrictScalars R)
have : f.comp (TensorProduct.mk R k M 1) = Submodule.mkQ (𝔪 • ⊤) := by ext; simp [f]
have hf : Function.Surjective f := by
intro x; obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
rw [← this, LinearMap.comp_apply]; exact ⟨_, rfl⟩
apply_fun Submodule.map f at hN
rwa [← Submodule.map_comp, this, Submodule.map_top, LinearMap.range_eq_top.2 hf, map_mkQ_eq_top] at hN
· rintro rfl; rw [Submodule.map_top, LinearMap.range_eq_top]
exact TensorProduct.mk_surjective R M k Ideal.Quotient.mk_surjective
