Ideals generated by compatible roots

Let r : ℕ → R satisfy r (n + 1) ^ p = r n, where p ≥ 2. The ideal generated by the r n is an increasing union of principal ideals: an element belongs to it exactly when some r n divides it, and any two of its elements are divisible by a common root. This ideal is idempotent, and the k-th powers of the roots still generate it for every positive k. Discarding finitely many roots leaves it unchanged.

These are the algebraic properties of the root ideal used in almost mathematics. They require neither a topology nor regularity of the roots, and apply even to compatible nilpotent roots. The ideal is written as Ideal.span (Set.range r) throughout, using the existing ideal API.

References

• O. Gabber and L. Ramero, Almost ring theory, §2.1, conditions (A) and (B).
• B. Bhatt, Lecture notes for a class on perfectoid spaces, §4.1, Example 4.1.3.

theorem TauCeti.mem_span_range_compatible_roots_iff {R : Type u_1} [CommSemiring R] {p : ℕ} {r : ℕ → R} (hr : ∀ (n : ℕ), r (n + 1) ^ p = r n) {x : R} : x ∈ Ideal.span (Set.range r) ↔ ∃ (n : ℕ), r n ∣ x

The ideal of a compatible root sequence is the union of its principal root ideals.

theorem TauCeti.exists_dvd_and_dvd_of_mem_span_range_compatible_roots {R : Type u_1} [CommSemiring R] {p : ℕ} {r : ℕ → R} (hr : ∀ (n : ℕ), r (n + 1) ^ p = r n) {x y : R} (hx : x ∈ Ideal.span (Set.range r)) (hy : y ∈ Ideal.span (Set.range r)) : ∃ (n : ℕ), r n ∣ x ∧ r n ∣ y

Two elements of the ideal of a compatible root sequence are divisible by a common root.

theorem TauCeti.exists_pow_dvd_of_mem_span_range_compatible_roots {R : Type u_1} [CommSemiring R] {p : ℕ} {r : ℕ → R} (hp : 2 ≤ p) (hr : ∀ (n : ℕ), r (n + 1) ^ p = r n) {x : R} (hx : x ∈ Ideal.span (Set.range r)) (k : ℕ) : ∃ (n : ℕ), r n ^ k ∣ x

For every k, an element of the root ideal is divisible by the k-th power of some root.

theorem TauCeti.span_range_pow_compatible_roots {R : Type u_1} [CommSemiring R] {p : ℕ} {r : ℕ → R} (hp : 2 ≤ p) (hr : ∀ (n : ℕ), r (n + 1) ^ p = r n) {k : ℕ} (hk : 0 < k) : Ideal.span (Set.range fun (n : ℕ) => r n ^ k) = Ideal.span (Set.range r)

Every positive power of the roots generates the same ideal as the roots themselves.

theorem TauCeti.isIdempotentElem_span_range_compatible_roots {R : Type u_1} [CommSemiring R] {p : ℕ} {r : ℕ → R} (hp : 2 ≤ p) (hr : ∀ (n : ℕ), r (n + 1) ^ p = r n) : IsIdempotentElem (Ideal.span (Set.range r))

The ideal generated by a compatible root sequence is idempotent, even when the roots are zero divisors.

theorem TauCeti.span_range_compatible_roots_shift {R : Type u_1} [CommSemiring R] {p : ℕ} {r : ℕ → R} (hr : ∀ (n : ℕ), r (n + 1) ^ p = r n) (k : ℕ) : Ideal.span (Set.range fun (n : ℕ) => r (n + k)) = Ideal.span (Set.range r)

Removing an initial segment of a compatible root sequence does not change its ideal.