Documentation

TauCeti.AlgebraicGeometry.Frobenius.Basic

The absolute Frobenius of a scheme #

Let p be a prime and X a scheme over 𝔽_p, that is, a scheme with p = 0 in Γ(X, ⊤). The absolute Frobenius F_X : X ⟶ X is the identity on the underlying topological space and the p-th power map s ↦ s ^ p on every ring of sections. It is a morphism of locally ringed spaces because s ^ p is a unit of a local ring only when s is.

Every morphism of schemes over 𝔽_p commutes with the absolute Frobenius (AlgebraicGeometry.Scheme.frobenius_naturality): unlike the relative Frobenius, it is not a morphism over the base, and it is the input from which the relative Frobenius F_{X/S} : X ⟶ X ×_{S, F_S} S of a scheme over S is built in TauCeti.AlgebraicGeometry.Frobenius.Relative. On an affine scheme Spec R it is induced by the p-th power map of R (AlgebraicGeometry.Scheme.Spec_map_powRingHom).

The hypothesis is stated on global sections, as (p : Γ(X, ⊤)) = 0, rather than through an ExpChar instance: the ring of sections over the empty open is the zero ring, which has no exponential characteristic p, so the p-th power map on sections is TauCeti.powRingHom.

Main definitions #

Main results #

References #

source
theorem AlgebraicGeometry.Scheme.natCast_app_eq_zero {X : Scheme} {p : ℕ} (hX : ↑p = 0) (U : X.Opens) :
↑p = 0

The prime p vanishes on every open of a scheme on which it vanishes globally.

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

The absolute Frobenius F_X : X ⟶ X of a scheme X in which the prime p vanishes: the identity on the underlying topological space and the p-th power map s ↦ s ^ p on sections.

Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.frobenius_base {X : Scheme} {p : ℕ} [hp : Fact (Nat.Prime p)] (hX : ↑p = 0) :
    (X.frobenius p hX).base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace

    The absolute Frobenius is the identity on the underlying topological space.

    source
    theorem AlgebraicGeometry.Scheme.frobenius_apply {X : Scheme} {p : ℕ} [hp : Fact (Nat.Prime p)] (hX : ↑p = 0) (x : ↥X) :
    (X.frobenius p hX) x = x

    The absolute Frobenius fixes every point.

    source
    theorem AlgebraicGeometry.Scheme.frobenius_preimage {X : Scheme} {p : ℕ} [hp : Fact (Nat.Prime p)] (hX : ↑p = 0) (U : X.Opens) :
    (TopologicalSpace.Opens.map (X.frobenius p hX).base).obj U = U

    The absolute Frobenius pulls back every open to itself.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.frobenius_appTop_apply {X : Scheme} {p : ℕ} [hp : Fact (Nat.Prime p)] (hX : ↑p = 0) (s : ↑(X.presheaf.obj (Opposite.op ⊤))) :
    (CategoryTheory.ConcreteCategory.hom (Hom.appTop (X.frobenius p hX))) s = s ^ p

    The absolute Frobenius is the p-th power map on global sections.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.frobenius_appLE_apply {X : Scheme} {p : ℕ} [hp : Fact (Nat.Prime p)] (hX : ↑p = 0) (U V : X.Opens) (e : V ≤ (TopologicalSpace.Opens.map (X.frobenius p hX).base).obj U) (s : ↑(X.presheaf.obj (Opposite.op U))) :
    (CategoryTheory.ConcreteCategory.hom (Hom.appLE (X.frobenius p hX) U V e)) s = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) s ^ p

    The absolute Frobenius is the p-th power map on sections: the section of X over V induced by a section s over U ⊇ V is the p-th power of the restriction of s.

    source
    theorem AlgebraicGeometry.Scheme.isIso_frobenius_app_iff {X : Scheme} {p : ℕ} [hp : Fact (Nat.Prime p)] (hX : ↑p = 0) (U : X.Opens) :
    CategoryTheory.IsIso (Hom.app (X.frobenius p hX) U) ↔ Function.Bijective fun (s : ↑(X.presheaf.obj (Opposite.op U))) => s ^ p

    The absolute Frobenius is an isomorphism on the sections over U exactly when the p-th power map of Γ(X, U) is bijective.

    source
    theorem AlgebraicGeometry.Scheme.bijective_frobenius_stalkMap_iff {X : Scheme} {p : ℕ} [hp : Fact (Nat.Prime p)] (hX : ↑p = 0) (x : ↥X) :
    Function.Bijective ⇑(CommRingCat.Hom.hom (Hom.stalkMap (X.frobenius p hX) x)) ↔ Function.Bijective fun (y : ↑(X.presheaf.stalk x)) => y ^ p

    The absolute Frobenius is bijective on the stalk at x exactly when the p-th power map of the local ring at x is bijective.

    source
    theorem AlgebraicGeometry.Scheme.natCast_eq_zero_of_hom {X Y : Scheme} {p : ℕ} (f : X ⟶ Y) (hY : ↑p = 0) :
    ↑p = 0

    A scheme over a scheme in which p vanishes is a scheme in which p vanishes.

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

    Every morphism of schemes over 𝔽_p commutes with the absolute Frobenius.

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

    Every morphism of schemes over 𝔽_p commutes with the absolute Frobenius.

    source
    theorem AlgebraicGeometry.Scheme.Spec_map_powRingHom {p : ℕ} [hp : Fact (Nat.Prime p)] (R : CommRingCat) (hR : ↑p = 0) :
    Spec.map (CommRingCat.ofHom (TauCeti.powRingHom (↑R) p hR)) = (Spec R).frobenius p ⋯

    On an affine scheme Spec R, the absolute Frobenius is induced by the p-th power map of R.