An invertible ideal generated by finitely many elements is generated by one of them

In a local ring R, an ideal generated by a non-zero-divisor a and also by a finite family z₁, …, z_c is generated by one of the zᵢ, which is a times a unit. Not in the sources; it is the ring-theoretic step of the universal property of the monoidal transformation [Hir64, Ch. 0, §2]: at a point y of a space Y' mapping to the centre C, the inverse image ideal of C in 𝒪_{Y',y} is generated by the pulled-back coordinates z₁ ∘ f', …, z_c ∘ f' of the centre and, being invertible, also by one non-zero-divisor a; the lemma picks the coordinate that generates it.

The argument: writing a = Σ bᵢ zᵢ and zᵢ = aᵢ a gives (Σ bᵢ aᵢ) a = a, so Σ bᵢ aᵢ = 1 because a is a non-zero-divisor; in a local ring one summand bᵢ aᵢ is then a unit, so aᵢ is a unit and zᵢ = aᵢ a generates the ideal.

AlgebraicGeometry.exists_span_singleton_eq_of_span_range_eq is the special case of a local domain and a nonzero generator (there every nonzero element is a non-zero-divisor); the local rings of a general analytic space are not domains, so the non-zero-divisor form is the one used for the uniqueness of monoidal transformations of analytic spaces.

theorem Algebra.exists_unit_mul_eq_of_span_range_eq_span_singleton {R : Type u_1} [CommRing R] [IsLocalRing R] {ι : Type u_2} [Finite ι] (z : ι → R) (a : R) (ha : a ∈ nonZeroDivisors R) (h : Ideal.span (Set.range z) = Ideal.span {a}) : ∃ (i : ι) (u : R), IsUnit u ∧ z i = u * a

In a local ring, an ideal generated by a non-zero-divisor a and also by finitely many elements z i is generated by one of the z i, which is a times a unit. Not in the sources; the non-zero-divisor form of AlgebraicGeometry.exists_span_singleton_eq_of_span_range_eq, which assumes a local domain.