Frobenius morphisms are integral universal homeomorphisms

Let p be a prime. The absolute Frobenius F_X : X ⟶ X of a scheme X in which p vanishes is the identity on points, but it is in general not an isomorphism of schemes. This file proves that it is nevertheless a universal homeomorphism: every base change of F_X is a homeomorphism of underlying spaces. The same holds for the relative Frobenius F_{X/S} : X ⟶ X^{(p)} of a scheme X over S, for their iterates, and so for every morphism f admitting a morphism g in the other direction such that both f ≫ g and g ≫ f are iterated absolute Frobenii.

Universal homeomorphisms are expressed both in Mathlib's form (topologically @IsHomeomorph).universally f and as instances of TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism. The generic instances for this class imply that the absolute and relative Frobenius and their iterates are surjective, universally injective (radicial), universally closed and integral.

The key input is AlgebraicGeometry.Scheme.universally_isHomeomorph_of_comp_eq_iterateFrobenius: if f ≫ g and g ≫ f are the n-fold absolute Frobenius of X and of Y, then on every base change X' ⟶ Y' of f, the morphism Y' ⟶ X' induced by F^n_{Y'} and g is inverse to it up to Frobenius on both sides; since Frobenius is the identity on points, the two maps are mutually inverse continuous maps of underlying spaces.

Main results

• AlgebraicGeometry.Scheme.universally_isHomeomorph_of_comp_eq_iterateFrobenius: a morphism that is invertible up to an iterated absolute Frobenius is a universal homeomorphism.
• AlgebraicGeometry.Scheme.universally_isHomeomorph_frobenius and AlgebraicGeometry.Scheme.universally_isHomeomorph_iterateFrobenius: the absolute Frobenius and its iterates are universal homeomorphisms.
• AlgebraicGeometry.Scheme.Hom.universally_isHomeomorph_relativeFrobenius and AlgebraicGeometry.Scheme.Hom.universally_isHomeomorph_iterateRelativeFrobenius: the relative Frobenius and its iterates are universal homeomorphisms.
• AlgebraicGeometry.Scheme.isUniversalHomeomorphism_of_comp_eq_iterateFrobenius: the class-valued criterion for morphisms invertible up to Frobenius.
• AlgebraicGeometry.Scheme.isUniversalHomeomorphism_frobenius and AlgebraicGeometry.Scheme.isUniversalHomeomorphism_iterateFrobenius: class instances for absolute Frobenius and its iterates.
• AlgebraicGeometry.Scheme.Hom.isUniversalHomeomorphism_relativeFrobenius and AlgebraicGeometry.Scheme.Hom.isUniversalHomeomorphism_iterateRelativeFrobenius: class instances for relative Frobenius and its iterates.

References

• The Stacks Project, Tag 0CC6, Frobenii: the absolute and relative Frobenius are integral universal homeomorphisms.

theorem AlgebraicGeometry.Scheme.universally_isHomeomorph_of_comp_eq_iterateFrobenius {X Y : Scheme} {p : ℕ} [Fact (Nat.Prime p)] {f : X ⟶ Y} (g : Y ⟶ X) (hY : ↑p = 0) (n : ℕ) (hfg : CategoryTheory.CategoryStruct.comp f g = X.iterateFrobenius p ⋯ n) (hgf : CategoryTheory.CategoryStruct.comp g f = Y.iterateFrobenius p hY n) : (topologically @IsHomeomorph).universally f

A morphism invertible up to Frobenius is a universal homeomorphism. If f : X ⟶ Y and g : Y ⟶ X compose, in either order, to the n-fold absolute Frobenius of X and of Y, then every base change of f is a homeomorphism of underlying spaces.

theorem AlgebraicGeometry.Scheme.universally_isHomeomorph_iterateFrobenius {X : Scheme} {p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) (n : ℕ) : (topologically @IsHomeomorph).universally (X.iterateFrobenius p hX n)

The iterated absolute Frobenius is a universal homeomorphism.

theorem AlgebraicGeometry.Scheme.universally_isHomeomorph_frobenius {X : Scheme} {p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) : (topologically @IsHomeomorph).universally (X.frobenius p hX)

The absolute Frobenius is a universal homeomorphism: every base change of F_X is a homeomorphism of underlying spaces.

theorem AlgebraicGeometry.Scheme.isUniversalHomeomorphism_of_comp_eq_iterateFrobenius {X Y : Scheme} {p : ℕ} [Fact (Nat.Prime p)] {f : X ⟶ Y} (g : Y ⟶ X) (hY : ↑p = 0) (n : ℕ) (hfg : CategoryTheory.CategoryStruct.comp f g = X.iterateFrobenius p ⋯ n) (hgf : CategoryTheory.CategoryStruct.comp g f = Y.iterateFrobenius p hY n) : TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism f

A morphism invertible up to iterated absolute Frobenius is a universal homeomorphism.

instance AlgebraicGeometry.Scheme.isUniversalHomeomorphism_iterateFrobenius {X : Scheme} {p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) (n : ℕ) : TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism (X.iterateFrobenius p hX n)

Iterated absolute Frobenius remains a homeomorphism after every base change.

instance AlgebraicGeometry.Scheme.isUniversalHomeomorphism_frobenius {X : Scheme} {p : ℕ} [Fact (Nat.Prime p)] (hX : ↑p = 0) : TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism (X.frobenius p hX)

Absolute Frobenius remains a homeomorphism after every base change.

theorem AlgebraicGeometry.Scheme.Hom.universally_isHomeomorph_iterateRelativeFrobenius {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (n : ℕ) : (topologically @IsHomeomorph).universally (iterateRelativeFrobenius π p hS n)

The iterated relative Frobenius is a universal homeomorphism.

theorem AlgebraicGeometry.Scheme.Hom.universally_isHomeomorph_relativeFrobenius {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) : (topologically @IsHomeomorph).universally (relativeFrobenius π p hS)

The relative Frobenius is a universal homeomorphism: every base change of F_{X/S} : X ⟶ X^{(p)} is a homeomorphism of underlying spaces.

instance AlgebraicGeometry.Scheme.Hom.isUniversalHomeomorphism_iterateRelativeFrobenius {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (n : ℕ) : TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism (iterateRelativeFrobenius π p hS n)

Iterated relative Frobenius remains a homeomorphism after every base change.

instance AlgebraicGeometry.Scheme.Hom.isUniversalHomeomorphism_relativeFrobenius {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) : TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism (relativeFrobenius π p hS)

Relative Frobenius remains a homeomorphism after every base change, with no flatness or perfectness hypothesis on the base.