iff_rTensor_preserves_shortComplex_exact

English

Equivalence between flatness of M as a module and the preservation of exactness by tensorRight on all short complexes in ModuleCat R.

Русский

Эквивалентность плоскости M и сохранение точности тензора справа в любом коротком комплексе.

LaTeX

$$$\\text{Flat } R M \\iff (\\forall C, C.Exact \\Rightarrow (C.map( tensorRight M)).Exact)$$$

Lean4

theorem iff_rTensor_preserves_shortComplex_exact :
    Flat R M ↔ ∀ (C : ShortComplex <| ModuleCat R) (_ : C.Exact), (C.map (tensorRight M) |>.Exact) :=
  ⟨fun _ _ ↦ rTensor_shortComplex_exact _ _, fun H ↦
    iff_rTensor_exact.2 fun _ _ _ _ _ _ _ _ _ f g h ↦
      moduleCat_exact_iff_function_exact _ |>.1 <|
        H (.mk (ModuleCat.ofHom f) (ModuleCat.ofHom g) (ModuleCat.hom_ext (DFunLike.ext _ _ h.apply_apply_eq_zero)))
          (moduleCat_exact_iff_function_exact _ |>.2 h)⟩

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