Filtered-graded transfer for complete rings (source code)

= Filtered-graded transfer for complete rings

For a complete separated multiplicatively filtered <ring> with nonnegative integer valuations, a domain <associated graded ring> makes the original ring a domain: the leading symbols of two nonzero elements have nonzero product. If the graded ring is left Noetherian, lift finitely many homogeneous generators of the graded ideal of a left ideal. Successively cancelling leading terms leaves remainders of increasing valuation. Completeness makes the coefficient series converge, expressing every ideal element as a finite sum of the chosen generators with completed coefficients. The right-handed argument is identical. Completeness is necessary for this infinite cancellation proof.