Frobenius between quotient rings

Let A be a commutative ring, p a prime and I, J ideals of A with p ∈ J and x ^ p ∈ J for every x ∈ I. Then x ↦ x ^ p induces a ring homomorphism A ⧸ I →+* A ⧸ J: it is the p-th power map TauCeti.powRingHom of A ⧸ J, in which p vanishes, composed with the projection A → A ⧸ J, and it kills I. No ring in sight need have characteristic p, so this is not an instance of Mathlib's frobenius.

The main case is I = (ϖ) and J = (ϖ ^ p) for an element ϖ with ϖ ^ p ∣ p, the map A ⧸ ϖ → A ⧸ ϖ ^ p whose bijectivity on the power-bounded subring defines perfectoid Tate rings (Scholze, Étale cohomology of diamonds, Definition 3.1). When A is integrally closed in a ring in which ϖ becomes a unit, this map is automatically injective.

Main definitions

• Ideal.frobeniusQuot: the ring homomorphism A ⧸ I →+* A ⧸ J, [x] ↦ [x ^ p].
• TauCeti.frobeniusModPow: its specialisation A ⧸ (ϖ) →+* A ⧸ (ϖ ^ p) for ϖ ^ p ∣ p.

Main results

• Ideal.frobeniusQuot_surjective_iff, Ideal.frobeniusQuot_injective_iff: elementwise forms of surjectivity and injectivity.
• TauCeti.frobeniusModPow_surjective_iff, TauCeti.frobeniusModPow_injective_iff: the same for frobeniusModPow, as divisibility conditions.
• TauCeti.frobeniusModPow_injective: frobeniusModPow is injective when A is integrally closed in an algebra in which ϖ is a unit.
• TauCeti.surjective_pow_modP_iff, TauCeti.surjective_frobenius_modP_iff: the p-th power map (Frobenius) on ModP A p = A ⧸ p is surjective exactly when every element of A is a p-th power modulo p.

References

• P. Scholze, Étale cohomology of diamonds, Definition 3.1 and Remark 3.2.

noncomputable def Ideal.frobeniusQuot {A : Type u_1} [CommRing A] (I J : Ideal A) (p : ℕ) [Fact (Nat.Prime p)] (hpJ : ↑p ∈ J) (hIJ : ∀ x ∈ I, x ^ p ∈ J) : A ⧸ I →+* A ⧸ J

The Frobenius A ⧸ I →+* A ⧸ J, [x] ↦ [x ^ p], for ideals I, J with p ∈ J and x ^ p ∈ J for every x ∈ I.

@[simp]

theorem Ideal.frobeniusQuot_mk {A : Type u_1} [CommRing A] {I J : Ideal A} {p : ℕ} [Fact (Nat.Prime p)] (hpJ : ↑p ∈ J) (hIJ : ∀ x ∈ I, x ^ p ∈ J) (x : A) : (I.frobeniusQuot J p hpJ hIJ) ((Quotient.mk I) x) = (Quotient.mk J) (x ^ p)

frobeniusQuot sends the class of x to the class of x ^ p.

theorem Ideal.frobeniusQuot_surjective_iff {A : Type u_1} [CommRing A] {I J : Ideal A} {p : ℕ} [Fact (Nat.Prime p)] (hpJ : ↑p ∈ J) (hIJ : ∀ x ∈ I, x ^ p ∈ J) : Function.Surjective ⇑(I.frobeniusQuot J p hpJ hIJ) ↔ ∀ (x : A), ∃ (y : A), x - y ^ p ∈ J

[x] ↦ [x ^ p] is surjective exactly when every element is a p-th power modulo J.

theorem Ideal.frobeniusQuot_injective_iff {A : Type u_1} [CommRing A] {I J : Ideal A} {p : ℕ} [Fact (Nat.Prime p)] (hpJ : ↑p ∈ J) (hIJ : ∀ x ∈ I, x ^ p ∈ J) : Function.Injective ⇑(I.frobeniusQuot J p hpJ hIJ) ↔ ∀ (y : A), y ^ p ∈ J → y ∈ I

[x] ↦ [x ^ p] is injective exactly when y ^ p ∈ J forces y ∈ I.

noncomputable def TauCeti.frobeniusModPow {A : Type u_1} [CommRing A] {ϖ : A} (p : ℕ) [Fact (Nat.Prime p)] (h : ϖ ^ p ∣ ↑p) : A ⧸ Ideal.span {ϖ} →+* A ⧸ Ideal.span {ϖ ^ p}

The Frobenius A ⧸ (ϖ) →+* A ⧸ (ϖ ^ p), [x] ↦ [x ^ p], for an element ϖ with ϖ ^ p ∣ p.

@[simp]

theorem TauCeti.frobeniusModPow_mk {A : Type u_1} [CommRing A] {ϖ : A} {p : ℕ} [Fact (Nat.Prime p)] (h : ϖ ^ p ∣ ↑p) (x : A) : (frobeniusModPow p h) ⟦x⟧ = ⟦x ^ p⟧

frobeniusModPow sends the class of x to the class of x ^ p.

theorem TauCeti.frobeniusModPow_surjective_iff {A : Type u_1} [CommRing A] {ϖ : A} {p : ℕ} [Fact (Nat.Prime p)] (h : ϖ ^ p ∣ ↑p) : Function.Surjective ⇑(frobeniusModPow p h) ↔ ∀ (x : A), ∃ (y : A), ϖ ^ p ∣ x - y ^ p

Frobenius A ⧸ (ϖ) → A ⧸ (ϖ ^ p) is surjective exactly when every element is a p-th power modulo ϖ ^ p.

theorem TauCeti.frobeniusModPow_injective_iff {A : Type u_1} [CommRing A] {ϖ : A} {p : ℕ} [Fact (Nat.Prime p)] (h : ϖ ^ p ∣ ↑p) : Function.Injective ⇑(frobeniusModPow p h) ↔ ∀ (y : A), ϖ ^ p ∣ y ^ p → ϖ ∣ y

Frobenius A ⧸ (ϖ) → A ⧸ (ϖ ^ p) is injective exactly when ϖ ^ p ∣ y ^ p forces ϖ ∣ y.

theorem TauCeti.frobeniusModPow_injective {A : Type u_1} [CommRing A] {ϖ : A} {p : ℕ} [Fact (Nat.Prime p)] (h : ϖ ^ p ∣ ↑p) {B : Type u_2} [CommRing B] [Algebra A B] [IsIntegrallyClosedIn A B] (hϖ : IsUnit ((algebraMap A B) ϖ)) : Function.Injective ⇑(frobeniusModPow p h)

If A is integrally closed in an A-algebra B in which ϖ is a unit, then Frobenius A ⧸ (ϖ) → A ⧸ (ϖ ^ p) is injective: ϖ ^ p ∣ y ^ p makes (y / ϖ) ^ p lie in A, so y / ϖ is integral over A and lies in A (Scholze, Étale cohomology of diamonds, Remark 3.2).

theorem TauCeti.surjective_pow_modP_iff (A : Type u_1) [CommRing A] {p : ℕ} : (Function.Surjective fun (x : ModP A p) => x ^ p) ↔ ∀ (x : A), ∃ (y : A), ↑p ∣ x - y ^ p

The p-th power map on ModP A p = A ⧸ p is surjective exactly when every element of A is a p-th power modulo p. Unlike surjective_frobenius_modP_iff, this needs no characteristic assumption on ModP A p, so it applies even when p is a unit of A.

theorem TauCeti.surjective_frobenius_modP_iff (A : Type u_1) [CommRing A] {p : ℕ} [ExpChar (ModP A p) p] : Function.Surjective ⇑(frobenius (ModP A p) p) ↔ ∀ (x : A), ∃ (y : A), ↑p ∣ x - y ^ p

Frobenius on ModP A p = A ⧸ p is surjective exactly when every element of A is a p-th power modulo p.