English
If l12:N1→N2 and l23:N2→N3 are R-linear and the rTensor with M is exact, then Im(l12) ⊆ Ker(l23).
Русский
Если линейные отображения l12 и l23 становятся точными после рTensor с M, то образ l12 лежит в ядре l23.
LaTeX
$$If $l_{12}:N_1\to N_2$ and $l_{23}:N_2\to N_3$ are linear maps and $l_{12}\!\rTensor M\, ,\ l_{23}\!\rTensor M$ form an exact sequence, then $\operatorname{Im}(l_{12}) \subseteq \ker(l_{23})$.$$
Lean4
/-- If `M` is faithfully flat, then exactness of `N₁ ⊗ M -> N₂ ⊗ M -> N₃ ⊗ M` implies that the
composition `N₁ -> N₂ -> N₃` is `0`.
Implementation detail, please use `rTensor_reflects_exact` instead.
-/
theorem range_le_ker_of_exact_rTensor [fl : FaithfullyFlat R M] (ex : Function.Exact (l12.rTensor M) (l23.rTensor M)) :
LinearMap.range l12 ≤ LinearMap.ker l23 := by
-- let `n1 ∈ N1`. We need to show `l23 (l12 n1) = 0`. Suppose this is not the case.
rintro _ ⟨n1, rfl⟩
rw [LinearMap.mem_ker]
by_contra! hn1
let E : Submodule R N3 := Submodule.span R {l23 (l12 n1)}
have hE : Nontrivial E :=
⟨0, ⟨⟨l23 (l12 n1), Submodule.mem_span_singleton_self _⟩, Subtype.coe_ne_coe.1 hn1.symm⟩⟩
-- Since `N1 ⊗ M -> N2 ⊗ M -> N3 ⊗ M` is exact, we have `l23 (l12 n1) ⊗ₜ m = 0` for all `m : M`.
have eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0 := fun m ↦
ex.apply_apply_eq_zero
(n1 ⊗ₜ[R] m)
-- Then `E ⊗ M = 0`. Indeed,
have eq0 : (⊤ : Submodule R (E ⊗[R] M)) = ⊥ := by
-- suppose `x ∈ E ⊗ M`. We will show `x = 0`.
ext x
simp only [Submodule.mem_top, Submodule.mem_bot, true_iff]
have mem : x ∈ (⊤ : Submodule R _) := ⟨⟩
rw [← TensorProduct.span_tmul_eq_top, Submodule.mem_span_set] at mem
obtain ⟨c, hc, rfl⟩ := mem
choose b a hy using hc
let r : ⦃a : E ⊗[R] M⦄ → a ∈ ↑c.support → R := fun a ha => Submodule.mem_span_singleton.1 (b ha).2 |>.choose
have hr :
∀ ⦃i : E ⊗[R] M⦄ (hi : i ∈ c.support), b hi = r hi • ⟨l23 (l12 n1), Submodule.mem_span_singleton_self _⟩ :=
fun a ha => Subtype.ext <| Submodule.mem_span_singleton.1 (b ha).2 |>.choose_spec.symm
refine
Finset.sum_eq_zero fun i hi =>
show c i • i = 0 from
(Module.Flat.rTensor_preserves_injective_linearMap (M := M) E.subtype <| Submodule.injective_subtype E) ?_
rw [← hy hi, hr hi, smul_tmul, map_smul, LinearMap.rTensor_tmul, Submodule.subtype_apply, eq1, smul_zero, map_zero]
have : Subsingleton (E ⊗[R] M) :=
subsingleton_iff_forall_eq 0 |>.2 fun x =>
show x ∈ (⊥ : Submodule R _) from
eq0 ▸
⟨⟩
-- but `E ⊗ M = 0` implies `E = 0` because `M` is faithfully flat and this is a contradiction.
exact not_subsingleton_iff_nontrivial.2 inferInstance <| fl.rTensor_reflects_triviality R M E
