English
If N is faithfully flat, Subsingleton(M ⊗R N) iff Subsingleton M.
Русский
Если N верноподобна, то Subsingleton(M ⊗R N) ⇔ Subsingleton M.
LaTeX
$$[simp] \forall M,N\ (\text{Module }R N)\ [\text{Module.FaithfullyFlat }R N] : \operatorname{Subsingleton}(M \otimes_R N) \iff \operatorname{Subsingleton}(M)$$
Lean4
theorem iff_exact_iff_rTensor_exact :
FaithfullyFlat R M ↔
(∀ {N1 : Type max u v} [AddCommGroup N1] [Module R N1] {N2 : Type max u v} [AddCommGroup N2] [Module R N2]
{N3 : Type max u v} [AddCommGroup N3] [Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
Function.Exact l12 l23 ↔ Function.Exact (l12.rTensor M) (l23.rTensor M)) :=
⟨fun fl _ _ _ _ _ _ _ _ _ l12 l23 => (rTensor_exact_iff_exact R M l12 l23).symm, fun iff_exact =>
iff_flat_and_rTensor_reflects_triviality _ _ |>.2
⟨Flat.iff_rTensor_exact.2 <| fun _ _ _ => iff_exact .. |>.1, fun N _ _ h =>
subsingleton_iff_forall_eq 0 |>.2 <| fun y => by
simpa [eq_comm] using
(iff_exact (0 : PUnit →ₗ[R] N) (0 : N →ₗ[R] PUnit) |>.2 fun x => by simpa using Subsingleton.elim _ _) y⟩⟩
