Frobenius-root ideals in perfect rings

Let R be a perfect ring of exponential characteristic p and let f ∈ R. Writing f ^ (1 / p ^ n) for the unique p ^ n-th root (iterateFrobeniusEquiv R p n).symm f of f, the Frobenius-root ideal of f is the increasing union J_f = ⋃ₙ (f ^ (1 / p ^ n)) of principal ideals.

When p is prime, we show that J_f is the radical of the principal ideal (f) and that it is idempotent. When moreover R is a ring, J_f is a flat R-module, with no assumption that R be a domain, and we present J_f as a sequential colimit: the colimit of copies of R along the multiplication maps by f ^ (1 / p ^ n - 1 / p ^ (n + 1)) maps isomorphically onto J_f, by sending a at stage n to f ^ (1 / p ^ n) * a.

Thus 0 → J_f → R → R ⧸ √(f) → 0 is a flat resolution of length one. Such resolutions are the building blocks of the Tor independence of perfect rings.

Main definitions

• TauCeti.frobeniusRootIdeal R p f: the ideal J_f = ⋃ₙ (f ^ (1 / p ^ n)).
• TauCeti.frobeniusRootTransition R p f: the transition maps of the sequential colimit presentation of J_f.
• TauCeti.frobeniusRootDirectLimitEquiv R p f: the colimit presentation of J_f.

Main results

• TauCeti.mem_frobeniusRootIdeal: x ∈ J_f iff some f ^ (1 / p ^ n) divides x.
• TauCeti.map_iterateFrobeniusEquiv_frobeniusRootIdeal: J_f is stable under Frobenius.
• TauCeti.frobeniusRootIdeal_eq_radical: J_f = √(f).
• TauCeti.frobeniusRootDirectLimitEquiv_of: the colimit presentation on each stage.
• TauCeti.isIdempotentElem_frobeniusRootIdeal: J_f * J_f = J_f.
• TauCeti.flat_frobeniusRootIdeal: J_f is a flat R-module.

References

• B. Bhatt and P. Scholze, Projectivity of the Witt vector affine Grassmannian, Invent. Math. 209 (2017), proof of Lemma 3.16.

noncomputable def TauCeti.frobeniusRootIdeal (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] [PerfectRing R p] (f : R) : Ideal R

The Frobenius-root ideal J_f = ⋃ₙ (f ^ (1 / p ^ n)) of an element f of a perfect ring R of exponential characteristic p: the supremum of the principal ideals generated by the p ^ n-th roots of f. For prime p, it equals the radical of (f) (TauCeti.frobeniusRootIdeal_eq_radical).

theorem TauCeti.frobeniusRootIdeal_eq_span_range {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] (f : R) : frobeniusRootIdeal R p f = Ideal.span (Set.range fun (n : ℕ) => (iterateFrobeniusEquiv R p n).symm f)

The Frobenius-root ideal of f is the ideal generated by all p ^ n-th roots of f.

theorem TauCeti.mem_frobeniusRootIdeal {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] {f x : R} : x ∈ frobeniusRootIdeal R p f ↔ ∃ (n : ℕ), (iterateFrobeniusEquiv R p n).symm f ∣ x

An element of R belongs to the Frobenius-root ideal of f if and only if it is divisible by some p ^ n-th root of f.

theorem TauCeti.iterateFrobeniusEquiv_symm_mem_frobeniusRootIdeal {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] (f : R) (n : ℕ) : (iterateFrobeniusEquiv R p n).symm f ∈ frobeniusRootIdeal R p f

Every p ^ n-th root of f lies in the Frobenius-root ideal of f.

@[simp]

theorem TauCeti.self_mem_frobeniusRootIdeal {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] (f : R) : f ∈ frobeniusRootIdeal R p f

An element lies in its own Frobenius-root ideal.

@[simp]

theorem TauCeti.map_iterateFrobeniusEquiv_frobeniusRootIdeal {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] (f : R) (n : ℕ) : Ideal.map (iterateFrobeniusEquiv R p n) (frobeniusRootIdeal R p f) = frobeniusRootIdeal R p f

The Frobenius-root ideal of f is stable under the iterated Frobenius x ↦ x ^ p ^ n. With this lemma, simp proves that every p ^ n-th root of f lies in the Frobenius-root ideal of f.

@[simp]

theorem TauCeti.frobeniusRootIdeal_zero {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] : frobeniusRootIdeal R p 0 = ⊥

The Frobenius-root ideal of 0 is zero.

@[simp]

theorem TauCeti.frobeniusRootIdeal_one {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] : frobeniusRootIdeal R p 1 = ⊤

The Frobenius-root ideal of 1 is the unit ideal.

noncomputable def TauCeti.frobeniusRootTransition (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] [PerfectRing R p] (f : R) (m n : ℕ) : m ≤ n → R →ₗ[R] R

The transition maps of the sequential colimit presentation of the Frobenius-root ideal of f: from stage m to stage n ≥ m, multiplication by f ^ (1 / p ^ m - 1 / p ^ n), the (p ^ (n - m) - 1)-st power of the p ^ n-th root of f.

@[simp]

theorem TauCeti.frobeniusRootTransition_apply {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] (f : R) {m n : ℕ} (h : m ≤ n) (a : R) : (frobeniusRootTransition R p f m n h) a = (iterateFrobeniusEquiv R p n).symm f ^ (p ^ (n - m) - 1) * a

The transition from stage m to stage n multiplies by the (p ^ (n - m) - 1)-st power of the p ^ n-th root of f.

theorem TauCeti.frobeniusRootTransition_apply_mul_iterateFrobeniusEquiv_symm {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] (f : R) {m n : ℕ} (h : m ≤ n) (a : R) : (frobeniusRootTransition R p f m n h) a * (iterateFrobeniusEquiv R p n).symm f = a * (iterateFrobeniusEquiv R p m).symm f

The transition from stage m to stage n, followed by multiplication by the p ^ n-th root of f, is multiplication by the p ^ m-th root of f.

instance TauCeti.instDirectedSystemNatCoeLinearMapIdFrobeniusRootTransition {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] (f : R) : DirectedSystem (fun (x : ℕ) => R) fun (m n : ℕ) (h : m ≤ n) => ⇑(frobeniusRootTransition R p f m n h)

The transition maps of the colimit presentation of the Frobenius-root ideal form a directed system.

theorem TauCeti.frobeniusRootIdeal_eq_radical {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] [hp : Fact (Nat.Prime p)] (f : R) : frobeniusRootIdeal R p f = (Ideal.span {f}).radical

Frobenius-root ideals are radicals. In a perfect ring, the Frobenius-root ideal of f is the radical of the principal ideal (f).

theorem TauCeti.isIdempotentElem_frobeniusRootIdeal {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] [hp : Fact (Nat.Prime p)] (f : R) : IsIdempotentElem (frobeniusRootIdeal R p f)

Frobenius-root ideals are idempotent: J_f * J_f = J_f.

instance TauCeti.flat_frobeniusRootIdeal {R : Type u_1} [CommRing R] {p : ℕ} [ExpChar R p] [PerfectRing R p] [hp : Fact (Nat.Prime p)] (f : R) : Module.Flat R ↥(frobeniusRootIdeal R p f)

Frobenius-root ideals are flat, also when R has zero divisors.

noncomputable def TauCeti.frobeniusRootDirectLimitEquiv (R : Type u_1) [CommRing R] (p : ℕ) [ExpChar R p] [PerfectRing R p] [hp : Fact (Nat.Prime p)] (f : R) : Module.DirectLimit (fun (x : ℕ) => R) (frobeniusRootTransition R p f) ≃ₗ[R] ↥(frobeniusRootIdeal R p f)

The colimit presentation of a Frobenius-root ideal. The sequential colimit of copies of R along frobeniusRootTransition is isomorphic to the Frobenius-root ideal of f, by sending a at stage n to f ^ (1 / p ^ n) * a.

@[simp]

theorem TauCeti.frobeniusRootDirectLimitEquiv_of {R : Type u_1} [CommRing R] {p : ℕ} [ExpChar R p] [PerfectRing R p] [hp : Fact (Nat.Prime p)] (f : R) (n : ℕ) (a : R) : ↑((frobeniusRootDirectLimitEquiv R p f) ((Module.DirectLimit.of R ℕ (fun (x : ℕ) => R) (frobeniusRootTransition R p f) n) a)) = a * (iterateFrobeniusEquiv R p n).symm f

The colimit presentation sends a at stage n to f ^ (1 / p ^ n) * a.