English
If M is faithfully flat and l12,l23 are R-linear with an exact N1⊗M → N2⊗M → N3⊗M, then l12,l23 are exact.
Русский
Если M верноподобна, и отображения l12,l23 образуют точную последовательность после rTensor с M, тогда они точны до оригинальных отображений.
LaTeX
$$$\forall l_{12},l_{23}\, [\mathrm{Module.FaithfullyFlat}_R(M)]\;\big( \mathrm{Function.Exact}(l_{12}\!\rTensor M)(l_{23}\!\rTensor M) \Rightarrow \mathrm{Function.Exact}(l_{12},l_{23})\big)$$$
Lean4
theorem rTensor_reflects_exact [fl : FaithfullyFlat R M] (ex : Function.Exact (l12.rTensor M) (l23.rTensor M)) :
Function.Exact l12 l23 :=
LinearMap.exact_iff.2 <|
by
have complex : LinearMap.range l12 ≤ LinearMap.ker l23 := range_le_ker_of_exact_rTensor R M _ _ ex
let H := LinearMap.ker l23 ⧸ LinearMap.range (Submodule.inclusion complex)
suffices triv_coh : Subsingleton H
by
rw [Submodule.subsingleton_quotient_iff_eq_top, Submodule.range_inclusion,
Submodule.comap_subtype_eq_top] at triv_coh
exact le_antisymm triv_coh complex
suffices Subsingleton (H ⊗[R] M) from rTensor_reflects_triviality R M H
let e : H ⊗[R] M ≃ₗ[R] _ :=
TensorProduct.quotientTensorEquiv _
_
-- Note that `H ⊗ M` is isomorphic to `ker l12 ⊗ M ⧸ range ((range l12 ⊗ M) -> (ker l23 ⊗ M))`.
-- So the problem is reduced to proving surjectivity of `range l12 ⊗ M → ker l23 ⊗ M`.
rw [e.toEquiv.subsingleton_congr, Submodule.subsingleton_quotient_iff_eq_top, LinearMap.range_eq_top]
intro x
induction x using TensorProduct.induction_on with
| zero =>
exact
⟨0, by simp⟩
-- let `x ⊗ m` be an element in `ker l23 ⊗ M`, then `x ⊗ m` is in the kernel of `l23 ⊗ 𝟙M`.
-- Since `N1 ⊗ M -l12 ⊗ M-> N2 ⊗ M -l23 ⊗ M-> N3 ⊗ M` is exact, we have that `x ⊗ m` is in
-- the range of `l12 ⊗ 𝟙M`, i.e. `x ⊗ m = (l12 ⊗ 𝟙M) y` for some `y ∈ N1 ⊗ M` as elements of
-- `N2 ⊗ M`. We need to prove that `x ⊗ m = (l12 ⊗ 𝟙M) y` still holds in `(ker l23) ⊗ M`.
-- This is okay because `M` is flat and `ker l23 -> N2` is injective.
| tmul x m =>
rcases x with ⟨x, (hx : l23 x = 0)⟩
have mem : x ⊗ₜ[R] m ∈ LinearMap.ker (l23.rTensor M) := by simp [hx]
rw [LinearMap.exact_iff.1 ex] at mem
obtain ⟨y, hy⟩ := mem
refine
⟨LinearMap.rTensor M (LinearMap.rangeRestrict _ ∘ₗ LinearMap.rangeRestrict l12) y,
Module.Flat.rTensor_preserves_injective_linearMap (LinearMap.ker l23).subtype Subtype.val_injective ?_⟩
simp only [LinearMap.comp_codRestrict, LinearMap.rTensor_tmul, Submodule.coe_subtype, ← hy]
rw [← LinearMap.comp_apply, ← LinearMap.rTensor_def, ← LinearMap.rTensor_comp, ← LinearMap.comp_apply, ←
LinearMap.rTensor_comp, LinearMap.comp_assoc, LinearMap.subtype_comp_codRestrict, ← LinearMap.comp_assoc,
Submodule.subtype_comp_inclusion, LinearMap.subtype_comp_codRestrict]
| add x y hx hy =>
obtain ⟨x, rfl⟩ := hx; obtain ⟨y, rfl⟩ := hy
exact ⟨x + y, by simp⟩
