of_linearEquiv — Mathlib

English

If M is faithfully flat over R and N is R-linearly isomorphic to M, then N is faithfully flat over R.

Русский

Если M является верноподобной над R, и N линейно эквивалентна M, то N также верноподобна над R.

LaTeX

$$$\forall (R,M)\ (\text{FaithfullyFlat}_R(M) \land e: N \cong_R M) \Rightarrow \text{FaithfullyFlat}_R(N)$$$

Lean4

/-- If `M` is a faithfully flat `R`-module and `N` is `R`-linearly isomorphic to `M`, then
`N` is faithfully flat. -/
theorem of_linearEquiv {N : Type*} [AddCommGroup N] [Module R N] [FaithfullyFlat R M] (e : N ≃ₗ[R] M) :
    FaithfullyFlat R N := by
  rw [iff_flat_and_lTensor_faithful]
  exact ⟨Flat.of_linearEquiv e, fun P _ _ hP ↦ (TensorProduct.congr e (LinearEquiv.refl R P)).toEquiv.nontrivial⟩

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