flatness and torsionfreeness

Stream: Is there code for X?

[Kevin Buzzard]

In the FLT project we seem to need that an abelian group is flat as a $\Z$-module iff it's torsionfree. I guess flat => tf is true for general $R$, and I guess the other way will be true for PIDs or something, but I couldn't find either of these things and so I thought I'd try and get my hands dirty and learn about flatness in Lean. Here's what looks to me like a rather poor effort to prove the key fact that multiplication by a nonzerodivisor is injective for a flat module:

import Mathlib.RingTheory.Flat.Basic

open scoped nonZeroDivisors TensorProduct

variable (R : Type*) [CommRing R]
    (M : Type*) [AddCommGroup M] [Module R M]

-- Is this even stated correctly? Do we have (r • _) as an R-linear map from M to M?

/-- Multiplication by a nonzerodivisor is injective on a flat module. -/
lemma smul_injective_of_flat {r : R} (hr : r ∈ R⁰) [Module.Flat R M] :
    Function.Injective ((r • ·) : M → M) := by
  -- closest I could find: the corresponding map `R ⊗[R] M →ₗ[R] R ⊗[R] M` is injective
  have h := Module.Flat.rTensor_preserves_injective_linearMap (M := M)
    (LinearMap.toSpanSingleton R R r) <|
    (injective_iff_map_eq_zero (LinearMap.toSpanSingleton R R r)).mpr hr
  -- now muddle through
  have h2 : (fun (x : M) ↦ r • x) = ((TensorProduct.lid R M).toLinearMap ∘ₗ
            (LinearMap.rTensor M (LinearMap.toSpanSingleton R R r)) ∘ₗ
            (TensorProduct.lid R M).symm.toLinearMap) := by ext; simp
  rw [h2]
  simp [h, LinearEquiv.injective]

Do we have any of this stuff already? Is the proof supposed to look so awful?

[Damiano Testa]

Without looking deep into this, I think that docs#IsSMulRegular may be a thing?

[Damiano Testa]

(I had introduced the "regular-mul" version to talk about regular sequences, so "smul-regular" should be some API for flatness.)

[Kevin Buzzard]

Nice! No mention of flatness in Mathlib/Algebra/Regular/* but at least it gives me a nicer way of stating it.

[Damiano Testa]

No, even the IsRegular --> regular sequences is probably underdeveloped, but I feel like this could be a "principled starting point".

[Kevin Buzzard]

The defining property is that an element `a ∈ R` is `M`-regular if the smultiplication map
`M → M`, defined by `m ↦ a • m`, is injective.

"smultiplication" :-)

[Damiano Testa]

And you could probably get for free results about products of smul-regular elements, trivialities about 0 and units...

[Kevin Buzzard]

So the statement can be rewritten as

lemma isSMulRegular_of_flat {r : R} (hr : r ∈ R⁰) [Module.Flat R M] : IsSMulRegular M r := by

[Andrew Yang]

@Brendan Seamas Murphy recently did a lot on regular sequences. Maybe Brendan has something close?

[Mitchell Lee]

One option is to use the equational criterion for flatness (#12666).

[Mitchell Lee]

I'm not sure if that's actually easier than what you did though

[Brendan Seamas Murphy]

I don't think this has come up for me? I have a currently open (edit: but failing to build, oops) PR which includes the fact that tensoring with a flat module preserves regularity, which is close to this result

[Brendan Seamas Murphy]

And lemmas that let you transport regularity across a linear equivalence

[Brendan Seamas Murphy]

lemma lTensor [Module.Flat R M] (h : IsSMulRegular M' r) :
    IsSMulRegular (M ⊗[R] M') r :=
  have h1 := congrArg DFunLike.coe (LinearMap.lTensor_smul_action M M' r)
  h1.subst (Module.Flat.lTensor_preserves_injective_linearMap _ h)

and see Equiv.isSMulRegular_congr (already in mathlib)

[Brendan Seamas Murphy]

What proof did you end up using?

[Brendan Seamas Murphy]

If it hasn't been finished yet, here's a proof

section

open scoped nonZeroDivisors

variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]

open IsSMulRegular in
lemma isSMulRegular_of_flat {r : R} (hr : r ∈ R⁰) [Module.Flat R M] :
    IsSMulRegular M r :=
  ((TensorProduct.rid R M).isSMulRegular_congr r).mp <|
    lTensor M <| isSMulRegular_of_smul_eq_zero_imp_eq_zero fun x h =>
      hr x <| Eq.trans (mul_comm x r) h
end

[Brendan Seamas Murphy]

The open IsSMulRegular in is due to some poor choices in namespacing by me in a recent PR that is fixed in #13582

The anonymous function here is necessary because we don't have an existing lemma that says a non zero divisor, meaning a right non zero divisor, is a non smul zero divisor in a commutative ring. Why is nonZeroDivisors defined as right non zero divisors? I thought mathlib convention was to have things on the left by default

[Andrew Yang]

TBH nonZeroDivisors should be the intersection of left and right.