English
Let M → N be a linear map between finitely generated modules over a local ring R. Then l is split injective iff the induced map on the residue field tensor is injective.
Русский
Пусть M → N — линейный отображение между модулями, порождаемыми над локальным кольцом R. Тогда l — расщепимая инъекция тогда и только тогда, когда тензорное отображение после тигра модуля на остаточное поле инъективно.
LaTeX
$$$ (\exists l',\; l' \circ l = \mathrm{id}) \iff (l.lTensor( k )\neq 0).$$$
Lean4
/-- Given `M₁ → M₂ → M₃ → 0` and `N₁ → N₂ → N₃ → 0`,
if `M₁ ⊗ N₃ → M₂ ⊗ N₃` and `M₂ ⊗ N₁ → M₂ ⊗ N₂` are both injective,
then `M₃ ⊗ N₁ → M₃ ⊗ N₂` is also injective.
-/
theorem lTensor_injective_of_exact_of_exact_of_rTensor_injective {M₁ M₂ M₃ N₁ N₂ N₃} [AddCommGroup M₁] [Module R M₁]
[AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₁] [Module R N₁] [AddCommGroup N₂]
[Module R N₂] [AddCommGroup N₃] [Module R N₃] {f₁ : M₁ →ₗ[R] M₂} {f₂ : M₂ →ₗ[R] M₃} {g₁ : N₁ →ₗ[R] N₂}
{g₂ : N₂ →ₗ[R] N₃} (hfexact : Exact f₁ f₂) (hfsurj : Surjective f₂) (hgexact : Exact g₁ g₂) (hgsurj : Surjective g₂)
(hfinj : Injective (f₁.rTensor N₃)) (hginj : Injective (g₁.lTensor M₂)) : Injective (g₁.lTensor M₃) :=
by
rw [injective_iff_map_eq_zero]
intro x hx
obtain ⟨x, rfl⟩ := f₂.rTensor_surjective N₁ hfsurj x
have : f₂.rTensor N₂ (g₁.lTensor M₂ x) = 0 := by
rw [← hx, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
LinearMap.lTensor_comp_rTensor]
obtain ⟨y, hy⟩ := (rTensor_exact N₂ hfexact hfsurj _).mp this
have : g₂.lTensor M₁ y = 0 := by
apply hfinj
trans g₂.lTensor M₂ (g₁.lTensor M₂ x)
·
rw [← hy, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
LinearMap.lTensor_comp_rTensor]
rw [← LinearMap.comp_apply, ← LinearMap.lTensor_comp, hgexact.linearMap_comp_eq_zero]
simp
obtain ⟨z, rfl⟩ := (lTensor_exact _ hgexact hgsurj _).mp this
obtain rfl : f₁.rTensor N₁ z = x := by
apply hginj
simp only [← hy, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.lTensor_comp_rTensor,
LinearMap.rTensor_comp_lTensor]
rw [← LinearMap.comp_apply, ← LinearMap.rTensor_comp, hfexact.linearMap_comp_eq_zero]
simp
