rTensor_shortComplex_exact — Mathlib

English

Flatness of M is equivalent to the property that tensorLeft by M preserves exactness of short complexes in ModuleCat R.

Русский

Плоскость M эквивалентна тому, что тензор слева тензорирует точность коротких комплексов в ModuleCat R.

LaTeX

$$$\\text{Flat } R M \\;\\Leftrightarrow\\; (\\forall C,\\; C.Exact \\Rightarrow (C.map( tensorLeft M)).Exact)$$$

Lean4

theorem rTensor_shortComplex_exact [Flat R M] (C : ShortComplex <| ModuleCat R) (hC : C.Exact) :
    C.map (tensorRight M) |>.Exact :=
  by
  rw [moduleCat_exact_iff_function_exact] at hC ⊢
  exact rTensor_exact M hC

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