The subring and subfield fixed by an iterated Frobenius

Let A be a commutative ring of exponential characteristic p and let q = p ^ n. The elements of A satisfying a ^ q = a are the equalizer of the ring homomorphism iterateFrobenius A p n and the identity, hence a subring: this file names it TauCeti.frobeniusFixedSubring and records its elementary properties. Over a field the equalizer is closed under inverses as well, giving TauCeti.frobeniusFixedSubfield.

For p prime, 0 < n and A an algebraic closure of ZMod p this subring is the field of q elements sitting inside A, which is why the construction is the ring-theoretic half of "the fixed points of the q-power Frobenius are the 𝔽_q-points"; at n = 0 it is instead the whole of A, since q = 1. Nothing about finiteness or about the field of q elements is proved here: the subring statements below are about an arbitrary commutative ring of exponential characteristic p and the subfield ones about an arbitrary field of exponential characteristic p, and Mathlib's iterateFrobenius supplies every proof.

Main definitions

• TauCeti.frobeniusFixedSubring: the subring of elements fixed by the p ^ n-power Frobenius.
• TauCeti.frobeniusFixedSubfield: the same elements of a field, as a subfield.

Main results

• TauCeti.mem_frobeniusFixedSubring: membership is the equation a ^ p ^ n = a.
• TauCeti.mem_frobeniusFixedSubring_mul_iff_iterate_eq: at exponent m * k, membership is being fixed by the k-th iterate of the p ^ m-power Frobenius.
• TauCeti.frobeniusFixedSubring_zero and TauCeti.frobeniusFixedSubfield_zero: the zeroth iterate fixes everything.
• TauCeti.frobeniusFixedSubring_le_of_dvd and TauCeti.frobeniusFixedSubfield_le_of_dvd: the fixed subrings and subfields grow along divisibility of the exponent, the inclusion 𝔽_{p ^ m} ⊆ 𝔽_{p ^ k} in the motivating case.
• TauCeti.map_le_frobeniusFixedSubring: a ring homomorphism carries fixed elements to fixed elements.

References

Mathlib's Mathlib/Algebra/CharP/Frobenius.lean supplies the Frobenius endomorphisms and their iteration and naturality laws. The fixed subring and subfield use Mathlib's RingHom.eqLocus and RingHom.eqLocusField equalizer constructions.

def TauCeti.frobeniusFixedSubring (A : Type u_1) [CommRing A] (p n : ℕ) [ExpChar A p] : Subring A

The subring of elements of A fixed by the p ^ n-power Frobenius, that is, the solutions of a ^ p ^ n = a. It is the equalizer of iterateFrobenius A p n with the identity.

When p is prime, 0 < n and A is an algebraic closure of ZMod p this is the subring of p ^ n elements, but nothing of the sort is asserted here: A is an arbitrary commutative ring of exponential characteristic p, and for p = 1 — that is, in characteristic zero — or for n = 0 the whole of A is fixed.

Equations

• TauCeti.frobeniusFixedSubring A p n = (iterateFrobenius A p n).eqLocus (RingHom.id A)

instance TauCeti.instExpCharSubtypeMemSubringFrobeniusFixedSubring (A : Type u_1) [CommRing A] (p n : ℕ) [ExpChar A p] : ExpChar (↥(frobeniusFixedSubring A p n)) p

The Frobenius-fixed subring is again of exponential characteristic p, so it is itself a legitimate value algebra for the Frobenius: iterateFrobenius and everything built on it apply to it. Mathlib has this for a Subfield (Subfield.expChar) but not for a Subring.

@[simp]

theorem TauCeti.mem_frobeniusFixedSubring {A : Type u_1} [CommRing A] {p n : ℕ} [ExpChar A p] {a : A} : a ∈ frobeniusFixedSubring A p n ↔ a ^ p ^ n = a

Membership in the Frobenius-fixed subring is the equation a ^ p ^ n = a.

theorem TauCeti.mem_frobeniusFixedSubring_mul_iff_iterate_eq {A : Type u_1} [CommRing A] {p : ℕ} [ExpChar A p] {m k : ℕ} {a : A} : a ∈ frobeniusFixedSubring A p (m * k) ↔ (⇑(iterateFrobenius A p m))^[k] a = a

At an exponent m * k, being fixed by the p ^ (m * k)-power Frobenius is being fixed by the k-th iterate of the p ^ m-power one, since that iterate is the p ^ (m * k)-power Frobenius.

@[simp]

theorem TauCeti.frobeniusFixedSubring_zero (A : Type u_1) [CommRing A] (p : ℕ) [ExpChar A p] : frobeniusFixedSubring A p 0 = ⊤

The zeroth Frobenius iterate is the identity, so it fixes every element.

theorem TauCeti.frobeniusFixedSubring_le_of_dvd {A : Type u_1} [CommRing A] {p : ℕ} [ExpChar A p] {m k : ℕ} (h : m ∣ k) : frobeniusFixedSubring A p m ≤ frobeniusFixedSubring A p k

Fixed subrings grow along divisibility of the exponent: an element fixed by the p ^ m-power Frobenius is fixed by the p ^ k-power Frobenius whenever m ∣ k. In the motivating case this is the inclusion 𝔽_{p ^ m} ⊆ 𝔽_{p ^ k} of subfields of an algebraic closure.

theorem TauCeti.map_le_frobeniusFixedSubring {A : Type u_1} [CommRing A] {p n : ℕ} [ExpChar A p] {B : Type u_2} [CommRing B] [ExpChar B p] (φ : A →+* B) : Subring.map φ (frobeniusFixedSubring A p n) ≤ frobeniusFixedSubring B p n

A ring homomorphism commutes with the Frobenius, so it carries elements fixed by the p ^ n-power Frobenius to elements fixed by it.

theorem TauCeti.map_mem_frobeniusFixedSubring {A : Type u_1} [CommRing A] {p n : ℕ} [ExpChar A p] {B : Type u_2} [CommRing B] [ExpChar B p] (φ : A →+* B) {a : A} (ha : a ∈ frobeniusFixedSubring A p n) : φ a ∈ frobeniusFixedSubring B p n

The pointwise form of map_le_frobeniusFixedSubring.

def TauCeti.frobeniusFixedSubfield (K : Type u_1) [Field K] (p n : ℕ) [ExpChar K p] : Subfield K

The subfield of elements of a field K fixed by the p ^ n-power Frobenius, that is, the solutions of a ^ p ^ n = a. It is the equalizer of iterateFrobenius K p n with the identity, taken as a subfield: over a field the equalizer is closed under inverses, since (a⁻¹) ^ p ^ n = (a ^ p ^ n)⁻¹.

As with the subring, nothing about finiteness is asserted at this level of generality: at n = 0, or in characteristic zero, it is the whole of K.

Equations

• TauCeti.frobeniusFixedSubfield K p n = (iterateFrobenius K p n).eqLocusField (RingHom.id K)

@[simp]

theorem TauCeti.mem_frobeniusFixedSubfield {K : Type u_1} [Field K] {p n : ℕ} [ExpChar K p] {a : K} : a ∈ frobeniusFixedSubfield K p n ↔ a ^ p ^ n = a

Membership in the Frobenius-fixed subfield is the equation a ^ p ^ n = a.

@[simp]

theorem TauCeti.toSubring_frobeniusFixedSubfield (K : Type u_1) [Field K] (p n : ℕ) [ExpChar K p] : (frobeniusFixedSubfield K p n).toSubring = frobeniusFixedSubring K p n

The Frobenius-fixed subfield has the Frobenius-fixed subring as its underlying subring.

@[simp]

theorem TauCeti.frobeniusFixedSubfield_zero (K : Type u_1) [Field K] (p : ℕ) [ExpChar K p] : frobeniusFixedSubfield K p 0 = ⊤

The zeroth Frobenius iterate is the identity, so it fixes every element.

theorem TauCeti.frobeniusFixedSubfield_le_of_dvd {K : Type u_1} [Field K] {p : ℕ} [ExpChar K p] {m k : ℕ} (h : m ∣ k) : frobeniusFixedSubfield K p m ≤ frobeniusFixedSubfield K p k

Fixed subfields grow along divisibility of the exponent, the subfield form of frobeniusFixedSubring_le_of_dvd: in the motivating case this is the inclusion 𝔽_{p ^ m} ⊆ 𝔽_{p ^ k} of subfields of an algebraic closure.