Cancellation by a nonzerodivisor and the local criterion for a generator

Two elementary facts about principal ideals generated by nonzerodivisors, both extracted from step (c) of the proof of the universal property of the blow-up [Hau14, Theorem 4.18, proof (c)].

Main declarations

• AlgebraicGeometry.isUnit_of_span_mul_eq_span: if b is a nonzerodivisor and (bc) = (b), then c is a unit — write b = r·bc and cancel b, so rc = 1.
• AlgebraicGeometry.exists_unit_mul_of_span_eq_span, mem_nonZeroDivisors_of_span_eq_span: a generator of an ideal generated by a nonzerodivisor b is a unit multiple of b, hence itself a nonzerodivisor.
• AlgebraicGeometry.exists_generator_of_isLocalRing [Hau14, Theorem 4.18, proof (c)]: for β : R → S with S local and β(I)S = (h), h a nonzerodivisor, some f ∈ I has β(f) generating β(I)S. As printed: h = ∑ β(fᵢ) sᵢ with fᵢ ∈ I, β(fᵢ) = tᵢ h, so (∑ sᵢ tᵢ) h = h and ∑ sᵢ tᵢ = 1 by cancellation; in a local ring some sᵢ tᵢ, hence some tᵢ, is a unit, and then β(fᵢ) = tᵢ h generates (h).

Boundary cases

In the zero ring every element is a nonzerodivisor and a unit, and every statement is trivially true. A local ring is nontrivial by definition, so 1 ∉ 𝔪 in the last argument.

theorem AlgebraicGeometry.isUnit_of_span_mul_eq_span {S : Type u} [CommRing S] {b c : S} (hb : b ∈ nonZeroDivisors S) (h : Ideal.span {b * c} = Ideal.span {b}) : IsUnit c

If b is a nonzerodivisor and (bc) = (b), then c is a unit: the cancellation step of [Hau14, Theorem 4.18, proof (c)].

theorem AlgebraicGeometry.exists_unit_mul_of_span_eq_span {S : Type u} [CommRing S] {b b' : S} (hb : b ∈ nonZeroDivisors S) (h : Ideal.span {b'} = Ideal.span {b}) : ∃ (u : Sˣ), b' = ↑u * b

A generator of the ideal generated by a nonzerodivisor b is a unit multiple of b.

theorem AlgebraicGeometry.mem_nonZeroDivisors_of_span_eq_span {S : Type u} [CommRing S] {b b' : S} (hb : b ∈ nonZeroDivisors S) (h : Ideal.span {b'} = Ideal.span {b}) : b' ∈ nonZeroDivisors S

A generator of the ideal generated by a nonzerodivisor is a nonzerodivisor.

theorem AlgebraicGeometry.exists_generator_of_isLocalRing {S : Type u} [CommRing S] {R : Type v} [CommRing R] [IsLocalRing S] (β : R →+* S) (I : Ideal R) {h : S} (hh : h ∈ nonZeroDivisors S) (hI : Ideal.map β I = Ideal.span {h}) : ∃ f ∈ I, Ideal.map β I = Ideal.span {β f}

If β : R → S with S local and β(I)S = (h) for a nonzerodivisor h, then some f ∈ I has β(f) generating β(I)S [Hau14, Theorem 4.18, proof (c)].