lTensor_reflects_exact — Mathlib

English

If M is faithfully flat and l12,l23 are R-linear with exactness of l12.lTensor M and l23.lTensor M, then l12,l23 are exact.

Русский

Если M верноподобна, и последовательность после lTensor M точна, то исходная последовательность точна.

LaTeX

$$$\forall l_{12},l_{23}\, [\mathrm{Module.FaithfullyFlat}_R(M)]\big( \mathrm{Function.Exact}(l_{12}\lTensor M)(l_{23}\lTensor M) \Rightarrow \mathrm{Function.Exact}(l_{12},l_{23})\big)$$$

Lean4

theorem lTensor_reflects_exact [fl : FaithfullyFlat R M] (ex : Function.Exact (l12.lTensor M) (l23.lTensor M)) :
    Function.Exact l12 l23 :=
  rTensor_reflects_exact R M _ _ <|
    ex.of_ladder_linearEquiv_of_exact (e₁ := TensorProduct.comm _ _ _) (e₂ := TensorProduct.comm _ _ _) (e₃ :=
      TensorProduct.comm _ _ _) (by ext; rfl) (by ext; rfl)

Похожие утверждения