English
If R is a Bezout domain and R is a domain, then an R-module M is flat iff it has no torsion.
Русский
Если R — область Безоу, и R — доменная, то R-модуль M плоский тогда и только тогда, когда у него нет торсиона.
LaTeX
$$$Flat\\,R\\,M \\iff torsion\\,R\\,M = \\bot$$$
Lean4
/-- If `R` is Bezout then an `R`-module is flat iff it has no torsion. -/
@[stacks 0539 "Generalized valuation ring to Bezout domain"]
theorem flat_iff_torsion_eq_bot_of_isBezout [IsBezout R] [IsDomain R] : Flat R M ↔ torsion R M = ⊥ := by
-- one way is true in general
refine
⟨fun _ ↦ torsion_eq_bot, ?_⟩
-- now assume R is a Bezout domain and M is a torsionfree R-module
intro htors
rw [iff_lift_lsmul_comp_subtype_injective]
rintro I hFG
obtain (rfl | h) := eq_or_ne I ⊥
· rintro x y -
apply Subsingleton.elim
· -- If I ≠ 0 then I ≅ R because R is Bezout and I is finitely generated
have hprinc : I.IsPrincipal := IsBezout.isPrincipal_of_FG I hFG
have : IsPrincipal.generator I ≠ 0 := by rwa [ne_eq, ← IsPrincipal.eq_bot_iff_generator_eq_zero]
apply Function.Injective.of_comp_right _ (LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)).surjective
rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp, LinearEquiv.coe_rTensor, rTensor, lift_comp_map,
LinearMap.compl₂_id, LinearMap.comp_assoc, Ideal.subtype_isoBaseOfIsPrincipal_eq_mul,
LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmul, LinearMap.coe_comp]
rw [← Submodule.noZeroSMulDivisors_iff_torsion_eq_bot] at htors
refine Function.Injective.comp (LinearMap.lsmul_injective this) ?_
rw [← Equiv.injective_comp (TensorProduct.lid R M).symm.toEquiv]
convert Function.injective_id
ext
simp
