Iterated absolute Frobenius

The n-fold absolute Frobenius of a scheme in characteristic p is the endomorphism obtained by composing its absolute Frobenius n times. It fixes the underlying topological space and raises sections to their p ^ n-th powers. These iterates are the absolute maps underlying relative Frobenius twists and finite-field Frobenius morphisms.

Main definitions

• AlgebraicGeometry.Scheme.iterateFrobenius: the n-fold absolute Frobenius of a scheme.

Main results

• AlgebraicGeometry.Scheme.iterateFrobenius_zero, _succ, and _add: the iteration laws.
• AlgebraicGeometry.Scheme.iterateFrobenius_naturality: every morphism of characteristic-p schemes commutes with every iterate.
• AlgebraicGeometry.Scheme.iterateFrobenius_appTop_apply: the iterate raises global sections to their p ^ n-th powers.
• AlgebraicGeometry.Scheme.frobenius_spec_zmod: the absolute Frobenius of Spec 𝔽_p is the identity.
• AlgebraicGeometry.Scheme.qPowerFrobenius: the absolute q-power map of a scheme over a finite field of cardinality q.

References

• The Stacks Project, chapter Varieties, section Frobenii, Remark 33.36.11.

noncomputable def AlgebraicGeometry.Scheme.iterateFrobenius (X : Scheme) (p : ℕ) [Fact (Nat.Prime p)] (hX : ↑p = 0) : ℕ → (X ⟶ X)

The n-fold absolute Frobenius of a scheme in which the prime p vanishes.

@[simp]

theorem AlgebraicGeometry.Scheme.iterateFrobenius_zero {X : Scheme} {p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) : X.iterateFrobenius p hX 0 = CategoryTheory.CategoryStruct.id X

The zeroth absolute Frobenius iterate is the identity.

theorem AlgebraicGeometry.Scheme.iterateFrobenius_succ {X : Scheme} {p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) (n : ℕ) : X.iterateFrobenius p hX (n + 1) = CategoryTheory.CategoryStruct.comp (X.iterateFrobenius p hX n) (X.frobenius p hX)

A successor absolute Frobenius iterate is obtained by composing with one Frobenius.

@[simp]

theorem AlgebraicGeometry.Scheme.iterateFrobenius_one {X : Scheme} {p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) : X.iterateFrobenius p hX 1 = X.frobenius p hX

The first absolute Frobenius iterate is the absolute Frobenius.

theorem AlgebraicGeometry.Scheme.iterateFrobenius_add {X : Scheme} {p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) (m n : ℕ) : X.iterateFrobenius p hX (m + n) = CategoryTheory.CategoryStruct.comp (X.iterateFrobenius p hX m) (X.iterateFrobenius p hX n)

Adding iteration exponents corresponds to composition of absolute Frobenius iterates.

theorem AlgebraicGeometry.Scheme.iterateFrobenius_apply {X : Scheme} {p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) (n : ℕ) (x : ↥X) : (X.iterateFrobenius p hX n) x = x

Every absolute Frobenius iterate fixes the underlying point of the scheme.

@[simp]

theorem AlgebraicGeometry.Scheme.iterateFrobenius_base {X : Scheme} {p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) (n : ℕ) : (X.iterateFrobenius p hX n).base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace

Every absolute Frobenius iterate has the identity map on the underlying space.

@[simp]

theorem AlgebraicGeometry.Scheme.iterateFrobenius_appTop_apply {X : Scheme} {p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) (n : ℕ) (s : ↑(X.presheaf.obj (Opposite.op ⊤))) : (CategoryTheory.ConcreteCategory.hom (Hom.appTop (X.iterateFrobenius p hX n))) s = s ^ p ^ n

The n-fold absolute Frobenius raises global sections to their p ^ n-th powers.

theorem AlgebraicGeometry.Scheme.natCast_spec_eq_zero {p : ℕ} (R : CommRingCat) [CharP (↑R) p] : ↑p = 0

The prime p vanishes on the global sections of the spectrum of a ring of characteristic p.

theorem AlgebraicGeometry.Scheme.Spec_map_iterateFrobenius {p : ℕ} [Fact (Nat.Prime p)] (R : Type u) [CommRing R] [CharP R p] (n : ℕ) : Spec.map (CommRingCat.ofHom (_root_.iterateFrobenius R p n)) = (Spec ↧R).iterateFrobenius p ⋯ n

On an affine scheme, iterated absolute Frobenius is induced by the corresponding iterated Frobenius of the coordinate ring.

theorem AlgebraicGeometry.Scheme.frobenius_spec_zmod {p : ℕ} [Fact (Nat.Prime p)] : (Spec ↧(ULift.{u, 0} (ZMod p))).frobenius p ⋯ = CategoryTheory.CategoryStruct.id (Spec ↧(ULift.{u, 0} (ZMod p)))

The absolute Frobenius of Spec 𝔽_p is the identity, since a ^ p = a for every a ∈ 𝔽_p.

theorem AlgebraicGeometry.Scheme.iterateFrobenius_naturality {X Y : Scheme} {p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) (hY : ↑p = 0) (f : X ⟶ Y) (n : ℕ) : CategoryTheory.CategoryStruct.comp (X.iterateFrobenius p hX n) f = CategoryTheory.CategoryStruct.comp f (Y.iterateFrobenius p hY n)

Every morphism of schemes in characteristic p commutes with every absolute Frobenius iterate.

theorem AlgebraicGeometry.Scheme.iterateFrobenius_naturality_assoc {X Y : Scheme} {p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) (hY : ↑p = 0) (f : X ⟶ Y) (n : ℕ) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.iterateFrobenius p hX n) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (Y.iterateFrobenius p hY n) h)

Every morphism of schemes in characteristic p commutes with every absolute Frobenius iterate.

noncomputable def AlgebraicGeometry.Scheme.qPowerFrobenius {p : ℕ} [Fact (Nat.Prime p)] (k : Type u) [Field k] [CharP k p] {X : Scheme} (f : X ⟶ Spec ↧k) (a : ℕ) (_ha : Nat.card k = p ^ a) : X ⟶ X

The absolute q-power Frobenius of a scheme over a finite field k, where q = Nat.card k = p ^ a.

theorem AlgebraicGeometry.Scheme.qPowerFrobenius_eq_iterated {p : ℕ} [Fact (Nat.Prime p)] (k : Type u) [Field k] [CharP k p] {X : Scheme} (f : X ⟶ Spec ↧k) (a : ℕ) (ha : Nat.card k = p ^ a) : qPowerFrobenius k f a ha = X.iterateFrobenius p ⋯ a

The finite-field q-power Frobenius is the specified absolute Frobenius iterate.

@[simp]

theorem AlgebraicGeometry.Scheme.qPowerFrobenius_appTop_apply {p : ℕ} [Fact (Nat.Prime p)] (k : Type u) [Field k] [CharP k p] {X : Scheme} (f : X ⟶ Spec ↧k) (a : ℕ) (ha : Nat.card k = p ^ a) (s : ↑(X.presheaf.obj (Opposite.op ⊤))) : (CategoryTheory.ConcreteCategory.hom (Hom.appTop (qPowerFrobenius k f a ha))) s = s ^ Nat.card k

The finite-field q-power Frobenius raises global sections to their q-th powers.

theorem AlgebraicGeometry.Scheme.qPowerFrobenius_naturality {p : ℕ} [Fact (Nat.Prime p)] (k : Type u) [Field k] [CharP k p] {X Y : Scheme} (fX : X ⟶ Spec ↧k) (fY : Y ⟶ Spec ↧k) (g : X ⟶ Y) (a : ℕ) (ha : Nat.card k = p ^ a) : CategoryTheory.CategoryStruct.comp (qPowerFrobenius k fX a ha) g = CategoryTheory.CategoryStruct.comp g (qPowerFrobenius k fY a ha)

Every morphism between schemes over the same finite field commutes with their q-power Frobenius maps.

theorem AlgebraicGeometry.Scheme.qPowerFrobenius_naturality_assoc {p : ℕ} [Fact (Nat.Prime p)] (k : Type u) [Field k] [CharP k p] {X Y : Scheme} (fX : X ⟶ Spec ↧k) (fY : Y ⟶ Spec ↧k) (g : X ⟶ Y) (a : ℕ) (ha : Nat.card k = p ^ a) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (qPowerFrobenius k fX a ha) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (qPowerFrobenius k fY a ha) h)

Every morphism between schemes over the same finite field commutes with their q-power Frobenius maps.

theorem AlgebraicGeometry.Scheme.iterateFrobenius_spec_eq_id {p : ℕ} [Fact (Nat.Prime p)] (k : Type u) [Field k] [Finite k] [CharP k p] (a : ℕ) (ha : Nat.card k = p ^ a) : (Spec ↧k).iterateFrobenius p ⋯ a = CategoryTheory.CategoryStruct.id (Spec ↧k)

The a-fold absolute Frobenius of the spectrum of a field with p ^ a elements is the identity.

@[simp]

theorem AlgebraicGeometry.Scheme.qPowerFrobenius_over {p : ℕ} [Fact (Nat.Prime p)] (k : Type u) [Field k] [Finite k] [CharP k p] {X : Scheme} (f : X ⟶ Spec ↧k) (a : ℕ) (ha : Nat.card k = p ^ a) : CategoryTheory.CategoryStruct.comp (qPowerFrobenius k f a ha) f = f

The finite-field q-power Frobenius is a morphism over the given finite field.

@[simp]

theorem AlgebraicGeometry.Scheme.qPowerFrobenius_over_assoc {p : ℕ} [Fact (Nat.Prime p)] (k : Type u) [Field k] [Finite k] [CharP k p] {X : Scheme} (f : X ⟶ Spec ↧k) (a : ℕ) (ha : Nat.card k = p ^ a) {Z : Scheme} (h : Spec ↧k ⟶ Z) : CategoryTheory.CategoryStruct.comp (qPowerFrobenius k f a ha) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp f h

The finite-field q-power Frobenius is a morphism over the given finite field.