lTensor_exact_iff_exact — Mathlib

English

Exactness of l12 and l23 is equivalent to exactness of their rTensor M versions for any M with FaithfullyFlat property.

Русский

Точность последовательности l12,l23 эквивалентна точности последовательности l12.rTensor M и l23.rTensor M для любого M с свойством FaithfullyFlat.

LaTeX

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

Lean4

@[simp]
theorem lTensor_exact_iff_exact [FaithfullyFlat R M] :
    Function.Exact (l12.lTensor M) (l23.lTensor M) ↔ Function.Exact l12 l23 :=
  ⟨fun ex ↦ lTensor_reflects_exact R M l12 l23 ex, fun e ↦ Module.Flat.lTensor_exact _ e⟩

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