The relative Frobenius of a scheme over a base of characteristic p

Let p be a prime, S a scheme in which p vanishes, with absolute Frobenius F_S : S ⟶ S, and π : X ⟶ S a scheme over S. The Frobenius twist of X is the base change X^{(p)} = X ×_{S, F_S} S, a scheme over S through its second projection. Since the absolute Frobenius commutes with π, the absolute Frobenius F_X and π define the relative Frobenius

F_{X/S} : X ⟶ X^{(p)},

a morphism over S whose composite with the first projection X^{(p)} ⟶ X is F_X.

Unlike F_X, the relative Frobenius is a morphism over S, natural in X over S (AlgebraicGeometry.Scheme.Hom.relativeFrobenius_naturality), and both the Frobenius twist and the relative Frobenius commute with base change along any T ⟶ S (AlgebraicGeometry.Scheme.Hom.isPullback_frobeniusTwistMap and AlgebraicGeometry.Scheme.Hom.isPullback_relativeFrobenius). It is a natural transformation from the identity of Over S to the base change functor Over.pullback F_S. Since both of these functors preserve finite products, it lifts to group objects, so it carries every group scheme G over S to a homomorphism of group schemes G ⟶ G^{(p)} (AlgebraicGeometry.Scheme.relativeFrobeniusGrpHom).

Main definitions

• AlgebraicGeometry.Scheme.Hom.relativeFrobenius π p hS: the relative Frobenius F_{X/S} : X ⟶ X ×_{S, F_S} S of π : X ⟶ S.
• AlgebraicGeometry.Scheme.Hom.frobeniusTwistMap π p hS f: the projection from the Frobenius twist of the base change of X along f : T ⟶ S to the Frobenius twist of X.
• AlgebraicGeometry.Scheme.relativeFrobeniusNatTrans S p hS: the relative Frobenius as a natural transformation 𝟭 (Over S) ⟶ Over.pullback F_S.
• AlgebraicGeometry.Scheme.relativeFrobeniusGrpHom S p hS G and AlgebraicGeometry.Scheme.relativeFrobeniusCommGrpHom S p hS G: the relative Frobenius of a (commutative) group scheme G over S, as a homomorphism of group schemes G ⟶ G^{(p)}.

Main results

• AlgebraicGeometry.Scheme.Hom.relativeFrobenius_fst and AlgebraicGeometry.Scheme.Hom.relativeFrobenius_snd: F_{X/S} followed by the projections of X^{(p)} is F_X and π.
• AlgebraicGeometry.Scheme.Hom.relativeFrobenius_naturality: F_{X/S} is natural in X over S.
• AlgebraicGeometry.Scheme.Hom.isPullback_frobeniusTwistMap: the Frobenius twist of X ×_S T over T is the base change of the Frobenius twist of X along T ⟶ S.
• AlgebraicGeometry.Scheme.Hom.isPullback_relativeFrobenius: the relative Frobenius of X ×_S T over T is the base change of the relative Frobenius of X along T ⟶ S.
• AlgebraicGeometry.Scheme.Hom.isPullback_frobeniusTwist_of_isPullback and AlgebraicGeometry.Scheme.Hom.isPullback_relativeFrobenius_of_isPullback: the same, for a base change X' ⟶ S' of X ⟶ S given by an arbitrary cartesian square.

References

• The Stacks Project, chapter Varieties, section Frobenii, for the relative Frobenius morphism and its compatibility with base change.

noncomputable def AlgebraicGeometry.Scheme.Hom.relativeFrobenius {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) : X ⟶ CategoryTheory.Limits.pullback π (S.frobenius p hS)

The relative Frobenius F_{X/S} : X ⟶ X^{(p)} = X ×_{S, F_S} S of a scheme π : X ⟶ S over a scheme S in which the prime p vanishes: the morphism to the Frobenius twist whose components are the absolute Frobenius F_X and π.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeFrobenius_fst {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) : CategoryTheory.CategoryStruct.comp (relativeFrobenius π p hS) (CategoryTheory.Limits.pullback.fst π (S.frobenius p hS)) = X.frobenius p ⋯

The relative Frobenius followed by the projection X^{(p)} ⟶ X is the absolute Frobenius.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeFrobenius_fst_assoc {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeFrobenius π p hS) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π (S.frobenius p hS)) h) = CategoryTheory.CategoryStruct.comp (X.frobenius p ⋯) h

The relative Frobenius followed by the projection X^{(p)} ⟶ X is the absolute Frobenius.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeFrobenius_snd {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) : CategoryTheory.CategoryStruct.comp (relativeFrobenius π p hS) (CategoryTheory.Limits.pullback.snd π (S.frobenius p hS)) = π

The relative Frobenius is a morphism over S.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeFrobenius_snd_assoc {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) {Z : Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeFrobenius π p hS) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd π (S.frobenius p hS)) h) = CategoryTheory.CategoryStruct.comp π h

The relative Frobenius is a morphism over S.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.fst_relativeFrobenius {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π (S.frobenius p hS)) (relativeFrobenius π p hS) = (CategoryTheory.Limits.pullback π (S.frobenius p hS)).frobenius p ⋯

The projection X^{(p)} ⟶ X from the Frobenius twist, followed by the relative Frobenius, is the absolute Frobenius of the twist.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.fst_relativeFrobenius_assoc {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) {Z : Scheme} (h : CategoryTheory.Limits.pullback π (S.frobenius p hS) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π (S.frobenius p hS)) (CategoryTheory.CategoryStruct.comp (relativeFrobenius π p hS) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pullback π (S.frobenius p hS)).frobenius p ⋯) h

The projection X^{(p)} ⟶ X from the Frobenius twist, followed by the relative Frobenius, is the absolute Frobenius of the twist.

noncomputable def AlgebraicGeometry.Scheme.Hom.frobeniusTwistMap {X S T : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (f : T ⟶ S) : CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.snd π f) (T.frobenius p ⋯) ⟶ CategoryTheory.Limits.pullback π (S.frobenius p hS)

The projection from the Frobenius twist (X ×_S T)^{(p)} of the base change of X along f : T ⟶ S to the Frobenius twist X^{(p)} of X, induced by the projection X ×_S T ⟶ X and by f.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.frobeniusTwistMap_fst {X S T : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (f : T ⟶ S) : CategoryTheory.CategoryStruct.comp (frobeniusTwistMap π p hS f) (CategoryTheory.Limits.pullback.fst π (S.frobenius p hS)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd π f) (T.frobenius p ⋯)) (CategoryTheory.Limits.pullback.fst π f)

The projection between Frobenius twists, followed by the projection X^{(p)} ⟶ X, is the projection (X ×_S T)^{(p)} ⟶ X ×_S T followed by the projection X ×_S T ⟶ X.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.frobeniusTwistMap_fst_assoc {X S T : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (f : T ⟶ S) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (frobeniusTwistMap π p hS f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π (S.frobenius p hS)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd π f) (T.frobenius p ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π f) h)

The projection between Frobenius twists, followed by the projection X^{(p)} ⟶ X, is the projection (X ×_S T)^{(p)} ⟶ X ×_S T followed by the projection X ×_S T ⟶ X.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.frobeniusTwistMap_snd {X S T : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (f : T ⟶ S) : CategoryTheory.CategoryStruct.comp (frobeniusTwistMap π p hS f) (CategoryTheory.Limits.pullback.snd π (S.frobenius p hS)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd π f) (T.frobenius p ⋯)) f

The projection between Frobenius twists lies over f : T ⟶ S.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.frobeniusTwistMap_snd_assoc {X S T : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (f : T ⟶ S) {Z : Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (frobeniusTwistMap π p hS f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd π (S.frobenius p hS)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd π f) (T.frobenius p ⋯)) (CategoryTheory.CategoryStruct.comp f h)

The projection between Frobenius twists lies over f : T ⟶ S.

theorem AlgebraicGeometry.Scheme.Hom.relativeFrobenius_naturality {X Y S : Scheme} {π : X ⟶ S} {p : ℕ} [Fact (Nat.Prime p)] (hS : ↑p = 0) (πY : Y ⟶ S) (g : X ⟶ Y) (hg : CategoryTheory.CategoryStruct.comp g πY = π) : CategoryTheory.CategoryStruct.comp (relativeFrobenius π p hS) (CategoryTheory.Limits.pullback.map π (S.frobenius p hS) πY (S.frobenius p hS) g (CategoryTheory.CategoryStruct.id S) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) = CategoryTheory.CategoryStruct.comp g (relativeFrobenius πY p hS)

The relative Frobenius is natural in the scheme over S: for a morphism g : X ⟶ Y over S, the relative Frobenius of Y after g is the relative Frobenius of X followed by the morphism X^{(p)} ⟶ Y^{(p)} induced by g.

theorem AlgebraicGeometry.Scheme.Hom.relativeFrobenius_naturality_assoc {X Y S : Scheme} {π : X ⟶ S} {p : ℕ} [Fact (Nat.Prime p)] (hS : ↑p = 0) (πY : Y ⟶ S) (g : X ⟶ Y) (hg : CategoryTheory.CategoryStruct.comp g πY = π) {Z : Scheme} (h : CategoryTheory.Limits.pullback πY (S.frobenius p hS) ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeFrobenius π p hS) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map π (S.frobenius p hS) πY (S.frobenius p hS) g (CategoryTheory.CategoryStruct.id S) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (relativeFrobenius πY p hS) h)

The relative Frobenius is natural in the scheme over S: for a morphism g : X ⟶ Y over S, the relative Frobenius of Y after g is the relative Frobenius of X followed by the morphism X^{(p)} ⟶ Y^{(p)} induced by g.

theorem AlgebraicGeometry.Scheme.Hom.isPullback_frobeniusTwist_of_isPullback {X S : Scheme} {π : X ⟶ S} {p : ℕ} [Fact (Nat.Prime p)] (hS : ↑p = 0) {X' S' : Scheme} {π' : X' ⟶ S'} {g : X' ⟶ X} {f : S' ⟶ S} (h : CategoryTheory.IsPullback g π' π f) : CategoryTheory.IsPullback (CategoryTheory.Limits.pullback.map π' (S'.frobenius p ⋯) π (S.frobenius p hS) g f f ⋯ ⋯) (CategoryTheory.Limits.pullback.snd π' (S'.frobenius p ⋯)) (CategoryTheory.Limits.pullback.snd π (S.frobenius p hS)) f

The Frobenius twist commutes with base change, for an arbitrary cartesian square. If X' over S' is the base change of X over S along f : S' ⟶ S, then the Frobenius twist of X' over S' is the base change of the Frobenius twist X^{(p)} of X along f.

theorem AlgebraicGeometry.Scheme.Hom.isPullback_frobeniusTwistMap {X S T : Scheme} {π : X ⟶ S} {p : ℕ} [Fact (Nat.Prime p)] (hS : ↑p = 0) (f : T ⟶ S) : CategoryTheory.IsPullback (frobeniusTwistMap π p hS f) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd π f) (T.frobenius p ⋯)) (CategoryTheory.Limits.pullback.snd π (S.frobenius p hS)) f

The Frobenius twist commutes with base change. For f : T ⟶ S, the Frobenius twist of X ×_S T over T is the base change of the Frobenius twist X^{(p)} of X along f.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeFrobenius_frobeniusTwistMap {X S T : Scheme} {π : X ⟶ S} {p : ℕ} [Fact (Nat.Prime p)] (hS : ↑p = 0) (f : T ⟶ S) : CategoryTheory.CategoryStruct.comp (relativeFrobenius (CategoryTheory.Limits.pullback.snd π f) p ⋯) (frobeniusTwistMap π p hS f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π f) (relativeFrobenius π p hS)

The relative Frobenius of the base change X ×_S T over T, followed by the projection to the Frobenius twist of X, is the projection X ×_S T ⟶ X followed by the relative Frobenius of X.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeFrobenius_frobeniusTwistMap_assoc {X S T : Scheme} {π : X ⟶ S} {p : ℕ} [Fact (Nat.Prime p)] (hS : ↑p = 0) (f : T ⟶ S) {Z : Scheme} (h : CategoryTheory.Limits.pullback π (S.frobenius p hS) ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeFrobenius (CategoryTheory.Limits.pullback.snd π f) p ⋯) (CategoryTheory.CategoryStruct.comp (frobeniusTwistMap π p hS f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π f) (CategoryTheory.CategoryStruct.comp (relativeFrobenius π p hS) h)

The relative Frobenius of the base change X ×_S T over T, followed by the projection to the Frobenius twist of X, is the projection X ×_S T ⟶ X followed by the relative Frobenius of X.

theorem AlgebraicGeometry.Scheme.Hom.isPullback_relativeFrobenius_of_isPullback {X S : Scheme} {π : X ⟶ S} {p : ℕ} [Fact (Nat.Prime p)] (hS : ↑p = 0) {X' S' : Scheme} {π' : X' ⟶ S'} {g : X' ⟶ X} {f : S' ⟶ S} (h : CategoryTheory.IsPullback g π' π f) : CategoryTheory.IsPullback (relativeFrobenius π' p ⋯) g (CategoryTheory.Limits.pullback.map π' (S'.frobenius p ⋯) π (S.frobenius p hS) g f f ⋯ ⋯) (relativeFrobenius π p hS)

The relative Frobenius commutes with base change, for an arbitrary cartesian square. If X' over S' is the base change of X over S along f : S' ⟶ S, then the relative Frobenius of X' over S' is the base change of the relative Frobenius of X over S.

theorem AlgebraicGeometry.Scheme.Hom.isPullback_relativeFrobenius {X S T : Scheme} {π : X ⟶ S} {p : ℕ} [Fact (Nat.Prime p)] (hS : ↑p = 0) (f : T ⟶ S) : CategoryTheory.IsPullback (relativeFrobenius (CategoryTheory.Limits.pullback.snd π f) p ⋯) (CategoryTheory.Limits.pullback.fst π f) (frobeniusTwistMap π p hS f) (relativeFrobenius π p hS)

The relative Frobenius commutes with base change. For f : T ⟶ S, the relative Frobenius of X ×_S T over T is the base change along f of the relative Frobenius of X over S.

noncomputable def AlgebraicGeometry.Scheme.relativeFrobeniusNatTrans (S : Scheme) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) : CategoryTheory.Functor.id (CategoryTheory.Over S) ⟶ CategoryTheory.Over.pullback (S.frobenius p hS)

The relative Frobenius as a natural transformation from the identity of Over S to the Frobenius twist, that is, the base change functor Over.pullback F_S along the absolute Frobenius of S.

@[simp]

theorem AlgebraicGeometry.Scheme.relativeFrobeniusNatTrans_app_left (S : Scheme) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (X : CategoryTheory.Over S) : CategoryTheory.Over.Hom.left ((S.relativeFrobeniusNatTrans p hS).app X) = Hom.relativeFrobenius X.hom p hS

noncomputable def AlgebraicGeometry.Scheme.relativeFrobeniusGrpHom (S : Scheme) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (G : CategoryTheory.Grp (CategoryTheory.Over S)) : G ⟶ (CategoryTheory.Over.pullback (S.frobenius p hS)).mapGrp.obj G

The relative Frobenius of a group scheme is a homomorphism. For a group scheme G over S, the relative Frobenius F_{G/S} : G ⟶ G^{(p)} is a homomorphism to the Frobenius twist of G with its group structure as a base change.

@[simp]

theorem AlgebraicGeometry.Scheme.relativeFrobeniusGrpHom_hom_hom_left (S : Scheme) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (G : CategoryTheory.Grp (CategoryTheory.Over S)) : CategoryTheory.Over.Hom.left (S.relativeFrobeniusGrpHom p hS G).hom.hom = Hom.relativeFrobenius G.X.hom p hS

noncomputable def AlgebraicGeometry.Scheme.relativeFrobeniusCommGrpHom (S : Scheme) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) : G ⟶ (CategoryTheory.Over.pullback (S.frobenius p hS)).mapCommGrp.obj G

The relative Frobenius of a commutative group scheme G over S, as a homomorphism of commutative group schemes G ⟶ G^{(p)}.

@[simp]

theorem AlgebraicGeometry.Scheme.relativeFrobeniusCommGrpHom_hom_hom_hom_left (S : Scheme) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) : CategoryTheory.Over.Hom.left (S.relativeFrobeniusCommGrpHom p hS G).hom.hom.hom = Hom.relativeFrobenius G.X.hom p hS