Flat quotients by universally regular elements

Let B be a flat algebra over a commutative ring R and g ∈ B. If multiplication by g on (R ⧸ I) ⊗[R] B is injective for every finitely generated ideal I of R, then B ⧸ (g) is a flat R-module.

Conversely, if g is a nonzerodivisor on B and B ⧸ (g) is flat over R, then g stays a nonzerodivisor after every base change. Thus, when B itself is flat over R and g is a nonzerodivisor on B, flatness of the quotient is equivalent to universal regularity of g. This is the algebraic criterion that makes a relative effective Cartier divisor remain an effective Cartier divisor after arbitrary base change.

This is the claim inside Wedhorn's proof of Lemma 8.31(2): for B = A⟨X⟩ over a complete noetherian Tate ring A, and g = f - X or g = 1 - f X, the quotient is flat because multiplication by g is injective on M⟨X⟩ = M ⊗[A] A⟨X⟩ for every finitely generated M — in particular for every M = A ⧸ I, which is all the argument uses. Wedhorn proves the claim with the long exact Tor sequence. What the sequence encodes is a diagram chase, and that chase is what is carried out here, against Mathlib's ideal criterion for flatness: B ⧸ (g) is flat once I ⊗[R] (B ⧸ (g)) → R ⊗[R] (B ⧸ (g)) is injective for every finitely generated ideal I.

Main results

• Module.Flat.quotient_span_singleton_of_lTensor_mulLeft_injective: the statement above.
• Module.Flat.lTensor_mulLeft_injective_of_quotient_span_singleton: flatness of B ⧸ (g) makes multiplication by a regular g stay injective after tensoring with any module.
• Module.Flat.isSMulRegular_one_tmul_of_quotient_span_singleton: after any algebra base change R → S, the element 1 ⊗ g is a nonzerodivisor on S ⊗[R] B.
• Module.Flat.quotient_span_singleton_iff_forall_lTensor_mulLeft_injective: for a flat R-algebra B and a nonzerodivisor g on B, flatness of B ⧸ (g) is equivalent to injectivity after tensoring with every R-module.
• Module.Flat.quotient_span_singleton_iff_forall_isSMulRegular_one_tmul: for a flat R-algebra B and a nonzerodivisor g on B, flatness of B ⧸ (g) is equivalent to this universal regularity.

Implementation notes

The forward implication asks only about (R ⧸ I) ⊗[R] B for finitely generated ideals I, which is exactly what the chase consumes; a hypothesis on every finitely generated module, as Wedhorn states it, specialises to this. The converse applies the standard fact that tensoring a short exact sequence whose cokernel is flat preserves injectivity. Statements use the coefficient module on the left, matching the orientation of Mathlib's flatness API.

The chase, for a finitely generated ideal I: an element of I ⊗ (B ⧸ (g)) killed in R ⊗ (B ⧸ (g)) lifts to I ⊗ B, is there the image of g times some w in R ⊗ B, and injectivity of g on (R ⧸ I) ⊗ B shows that w comes from I ⊗ B, so the element is g times an element of I ⊗ B and dies in I ⊗ (B ⧸ (g)). Flatness of B enters twice: as exactness of I ⊗ B → R ⊗ B → (R ⧸ I) ⊗ B, and as injectivity of I ⊗ B → R ⊗ B.

References

• Wedhorn, Adic Spaces, Lemma 8.31.

A flat quotient gives universal regularity

theorem Module.Flat.lTensor_mulLeft_injective_of_quotient_span_singleton {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B] {g : B} (hg : IsSMulRegular B g) [Flat R (B ⧸ Ideal.span {g})] (M : Type w) [AddCommGroup M] [Module R M] : Function.Injective ⇑(LinearMap.lTensor M (LinearMap.mulLeft R g))

If g is a nonzerodivisor on B and B ⧸ (g) is flat over R, multiplication by g remains injective after tensoring B with any R-module. This is the short exact sequence 0 → B → B → B ⧸ (g) → 0 tensored with that module.

theorem Module.Flat.isSMulRegular_one_tmul_of_quotient_span_singleton {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B] {g : B} (hg : IsSMulRegular B g) [Flat R (B ⧸ Ideal.span {g})] (S : Type w) [CommRing S] [Algebra R S] : IsSMulRegular (TensorProduct R S B) (1 ⊗ₜ[R] g)

If g is a nonzerodivisor on B and B ⧸ (g) is flat over R, then 1 ⊗ g is a nonzerodivisor after every algebra base change R → S. No flatness assumption on S is needed.

Universal regularity gives a flat quotient

theorem Module.Flat.quotient_span_singleton_of_lTensor_mulLeft_injective {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B] [Flat R B] (g : B) (hg : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (LinearMap.mulLeft R g))) : Flat R (B ⧸ Ideal.span {g})

A flat algebra modulo an element acting injectively on each (R ⧸ I) ⊗[R] B is flat. Let B be a flat R-algebra and g ∈ B. If id ⊗ (g • ·) : (R ⧸ I) ⊗[R] B → (R ⧸ I) ⊗[R] B is injective for every finitely generated ideal I, then B ⧸ (g) is a flat R-module. This is the Tor-sequence step of Wedhorn's Lemma 8.31(2); a consumer holding injectivity for every finitely generated module, as Wedhorn states it, passes it at M = R ⧸ I.

theorem Module.Flat.quotient_span_singleton_iff_forall_lTensor_mulLeft_injective {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B] [Flat R B] (g : B) (hg : IsSMulRegular B g) : Flat R (B ⧸ Ideal.span {g}) ↔ ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R M], Function.Injective ⇑(LinearMap.lTensor M (LinearMap.mulLeft R g))

For a flat R-algebra B and a nonzerodivisor g, the quotient B ⧸ (g) is flat over R if and only if multiplication by g remains injective after tensoring with every R-module.

theorem Module.Flat.quotient_span_singleton_iff_forall_isSMulRegular_one_tmul {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B] [Flat R B] (g : B) (hg : IsSMulRegular B g) : Flat R (B ⧸ Ideal.span {g}) ↔ ∀ (S : Type u) [inst : CommRing S] [inst_1 : Algebra R S], IsSMulRegular (TensorProduct R S B) (1 ⊗ₜ[R] g)

Flatness of a quotient by a nonzerodivisor is equivalent to universal regularity. If B is flat over R and g is a nonzerodivisor on B, then B ⧸ (g) is flat over R exactly when 1 ⊗ g is a nonzerodivisor on S ⊗[R] B for every R-algebra S.