English
FaithfullyFlat M is equivalent to Flat M plus the tensor-fidelity condition on all nontrivial N.
Русский
FaithfullyFlat эквивалентно Flat M плюс тензорная достоверность для всех не тривиальных N.
LaTeX
$$FaithfullyFlat R M ↔ (Flat R M ∧ ∀ N, Nontrivial N → Nontrivial (N ⊗_R M))$$
Lean4
theorem iff_flat_and_rTensor_faithful :
FaithfullyFlat R M ↔
(Flat R M ∧ ∀ (N : Type max u v) [AddCommGroup N] [Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)) :=
by
refine ⟨fun fl => ⟨inferInstance, rTensor_nontrivial R M⟩, fun ⟨flat, faithful⟩ => ⟨?_⟩⟩
intro m hm rid
specialize faithful (ULift (R ⧸ m)) inferInstance
haveI : Nontrivial ((R ⧸ m) ⊗[R] M) :=
(congr (ULift.moduleEquiv : ULift (R ⧸ m) ≃ₗ[R] R ⧸ m) (LinearEquiv.refl R M)).symm.toEquiv.nontrivial
have := (quotTensorEquivQuotSMul M m).toEquiv.symm.nontrivial
haveI H : Subsingleton (M ⧸ m • (⊤ : Submodule R M)) := by rwa [Submodule.subsingleton_quotient_iff_eq_top]
rw [← not_nontrivial_iff_subsingleton] at H
contradiction
