English
There is an equivalence between split injectivity of a map and injectivity after tensoring with the residue field.
Русский
Существует эквивалентность между расщепляемой инъекцией отображения и инъективностью после тензорирования по остаточному полю.
LaTeX
$$$ (\exists l',\; l' \circ l = id) \iff (l.lTensor(k) \text{ is injective}). $$$
Lean4
/-- Given a linear map `l : M → N` over a local ring `(R, 𝔪, k)`
with `M` finite and `N` finite free,
`l` is a split injection if and only if `k ⊗ l` is a (split) injection.
-/
theorem split_injective_iff_lTensor_residueField_injective [IsLocalRing R] [Module.Finite R M] [Module.Finite R N]
[Module.Free R N] (l : M →ₗ[R] N) :
(∃ l', l' ∘ₗ l = LinearMap.id) ↔ Function.Injective (l.lTensor (ResidueField R)) :=
by
constructor
· intro ⟨l', hl⟩
have : l'.lTensor (ResidueField R) ∘ₗ l.lTensor (ResidueField R) = .id := by
rw [← LinearMap.lTensor_comp, hl, LinearMap.lTensor_id]
exact Function.HasLeftInverse.injective ⟨_, LinearMap.congr_fun this⟩
· intro h
have :=
Module.free_of_lTensor_residueField_injective l (LinearMap.range l).mkQ (Submodule.mkQ_surjective _)
l.exact_map_mkQ_range h
have : Module.Projective R (LinearMap.range l) :=
by
have :=
(Exact.split_tfae (LinearMap.exact_subtype_mkQ (LinearMap.range l)) Subtype.val_injective
(Submodule.mkQ_surjective _)).out
0 1
obtain ⟨l', hl'⟩ := this.mp (Module.projective_lifting_property _ _ (Submodule.mkQ_surjective _))
exact Module.Projective.of_split _ _ hl'
obtain ⟨l', hl'⟩ : ∃ l', l' ∘ₗ (LinearMap.ker l).subtype = LinearMap.id :=
by
have :
Function.Exact (LinearMap.ker l).subtype (l.codRestrict (LinearMap.range l) (LinearMap.mem_range_self l)) := by
rw [LinearMap.exact_iff, LinearMap.ker_rangeRestrict, Submodule.range_subtype]
have := (Exact.split_tfae this Subtype.val_injective (fun ⟨x, y, e⟩ ↦ ⟨y, Subtype.ext e⟩)).out 0 1
exact this.mp (Module.projective_lifting_property _ _ (fun ⟨x, y, e⟩ ↦ ⟨y, Subtype.ext e⟩))
have : Module.Finite R (LinearMap.ker l) :=
by
refine Module.Finite.of_surjective l' ?_
exact
Function.HasRightInverse.surjective
⟨_, DFunLike.congr_fun hl'⟩
-- And tensoring with `k` preserves the injectivity of the first arrow.
-- That is, `k ⊗ ker l → k ⊗ M` is also injective.
have H : Function.Injective ((LinearMap.ker l).subtype.lTensor k) :=
by
apply_fun (LinearMap.lTensor k) at hl'
rw [LinearMap.lTensor_comp, LinearMap.lTensor_id] at hl'
exact
Function.HasLeftInverse.injective
⟨l'.lTensor k, DFunLike.congr_fun hl'⟩
-- But by assumption `k ⊗ M → k ⊗ l(M)` is already injective, so `k ⊗ ker l = 0`.
have : Subsingleton (k ⊗[R] LinearMap.ker l) :=
by
refine (subsingleton_iff_forall_eq 0).mpr fun y ↦ H (h ?_)
rw [map_zero, map_zero, ← LinearMap.comp_apply, ← LinearMap.lTensor_comp,
l.exact_subtype_ker_map.linearMap_comp_eq_zero, LinearMap.lTensor_zero, LinearMap.zero_apply]
-- By Nakayama's lemma, `l` is injective.
have : Function.Injective l := by
rwa [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot, ←
IsLocalRing.subsingleton_tensorProduct (R := R)]
-- Whence `M ≃ l(M)` is projective and the result follows.
have := (Exact.split_tfae l.exact_map_mkQ_range this (Submodule.mkQ_surjective _)).out 0 1
rw [← this]
exact Module.projective_lifting_property _ _ (Submodule.mkQ_surjective _)
