English
If every map from a finitely presented module factors through a finite free module, then the module is flat.
Русский
Если каждый гомоморфизм из конечнопредставимого модуля факorizируется через конечную свободную модульную схему, то модуль плосок.
LaTeX
$$(∀ h, h factors through a finite free) ⇒ Flat(R,M)$$
Lean4
/-- If `B` is a faithfully flat `A`-algebra, the preimage of the pushforward of any
ideal `I` is again `I`. -/
theorem comap_map_eq_self_of_faithfullyFlat (I : Ideal A) : (I.map (algebraMap A B)).comap (algebraMap A B) = I :=
by
refine le_antisymm ?_ le_comap_map
have inj :
Function.Injective
((quotIdealMapEquivTensorQuot B I).symm.toLinearMap.restrictScalars _ ∘ₗ TensorProduct.mk A B (A ⧸ I) 1) :=
by
rw [LinearMap.coe_comp]
exact (AlgEquiv.injective _).comp <| Module.FaithfullyFlat.tensorProduct_mk_injective (A ⧸ I)
intro x hx
rw [Ideal.mem_comap] at hx
rw [← Ideal.Quotient.eq_zero_iff_mem] at hx ⊢
apply inj
have :
((quotIdealMapEquivTensorQuot B I).symm.toLinearMap.restrictScalars _ ∘ₗ TensorProduct.mk A B (A ⧸ I) 1) x = 0 := by
simp [← Algebra.algebraMap_eq_smul_one, hx]
simp [this]
