Iterated Frobenius twists and the iterated relative Frobenius

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

F^n_{X/S} : X ⟶ X^{(p^n)},

a morphism over S whose composite with the first projection X^{(p^n)} ⟶ X is F_X^n. For n = 1 it is the relative Frobenius F_{X/S} of TauCeti.AlgebraicGeometry.Frobenius.Relative.

The twists are compatible with the exponents: the zeroth twist is X, and twisting the m-th twist X^{(p^m)} (as a scheme over S through its second projection) once more by F_S^n gives the (m + n)-th twist. Under these identifications the zeroth iterated relative Frobenius is the identity, and the iterated relative Frobenius of X for m + n is that of X for m followed by that of X^{(p^m)} for n. In particular F^{n+1}_{X/S} is F^n_{X/S} followed by the relative Frobenius of the n-th twist. As in the case n = 1, the iterated relative Frobenius is natural in X over S, commutes with every base change T ⟶ S, and lifts to a homomorphism of group schemes G ⟶ G^{(p^n)} for every group scheme G over S.

Main definitions

• AlgebraicGeometry.Scheme.Hom.iterateRelativeFrobenius π p hS n: the iterated relative Frobenius F^n_{X/S} : X ⟶ X ×_{S, F_S^n} S.
• AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistZeroIso: the zeroth twist is X.
• AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistSuccIso: the Frobenius twist of the n-th twist is the (n + 1)-th twist.
• AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistAddIso: the n-th twist of the m-th twist is the (m + n)-th twist.
• AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistMap π p hS n f: the projection from the n-th twist of the base change of X along f : T ⟶ S to the n-th twist of X.
• AlgebraicGeometry.Scheme.iterateRelativeFrobeniusNatTrans S p hS n: the iterated relative Frobenius as a natural transformation 𝟭 (Over S) ⟶ Over.pullback F_S^n, and AlgebraicGeometry.Scheme.iterateRelativeFrobeniusGrpHom its value on group schemes.

Main results

• AlgebraicGeometry.Scheme.Hom.iterateRelativeFrobenius_zero, AlgebraicGeometry.Scheme.Hom.iterateRelativeFrobenius_one, AlgebraicGeometry.Scheme.Hom.iterateRelativeFrobenius_succ and AlgebraicGeometry.Scheme.Hom.iterateRelativeFrobenius_add: the iteration laws.
• AlgebraicGeometry.Scheme.Hom.iterateRelativeFrobenius_naturality: F^n_{X/S} is natural in X over S.
• AlgebraicGeometry.Scheme.Hom.isPullback_iterateFrobeniusTwistMap and AlgebraicGeometry.Scheme.Hom.isPullback_iterateRelativeFrobenius: the n-th twist and the iterated relative Frobenius commute with base change.

References

• The Stacks Project, chapter Varieties, section Frobenii, Remark 33.36.11, for the iterated relative Frobenius.

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

The iterated relative Frobenius is a morphism over S.

@[simp]

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

The iterated relative Frobenius is a morphism over S.

@[simp]

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

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

@[simp]

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

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

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

The zeroth Frobenius twist X ×_{S, F_S^0} S of X is X, through the first projection.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistZeroIso_hom {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) : (iterateFrobeniusTwistZeroIso π p hS).hom = CategoryTheory.Limits.pullback.fst π (S.iterateFrobenius p hS 0)

noncomputable def AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistSuccIso {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (n : ℕ) : CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS n)) (S.frobenius p hS) ≅ CategoryTheory.Limits.pullback π (S.iterateFrobenius p hS (n + 1))

The Frobenius twist X^{(p^n)} ×_{S, F_S} S of the n-th Frobenius twist of X, a scheme over S through its second projection, is the (n + 1)-th Frobenius twist of X.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistSuccIso_hom_fst {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (n : ℕ) : CategoryTheory.CategoryStruct.comp (iterateFrobeniusTwistSuccIso π p hS n).hom (CategoryTheory.Limits.pullback.fst π (S.iterateFrobenius p hS (n + 1))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS n)) (S.frobenius p hS)) (CategoryTheory.Limits.pullback.fst π (S.iterateFrobenius p hS n))

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistSuccIso_hom_fst_assoc {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (n : ℕ) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (iterateFrobeniusTwistSuccIso π p hS n).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π (S.iterateFrobenius p hS (n + 1))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS n)) (S.frobenius p hS)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π (S.iterateFrobenius p hS n)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistSuccIso_hom_snd {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (n : ℕ) : CategoryTheory.CategoryStruct.comp (iterateFrobeniusTwistSuccIso π p hS n).hom (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS (n + 1))) = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS n)) (S.frobenius p hS)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistSuccIso_hom_snd_assoc {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (n : ℕ) {Z : Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (iterateFrobeniusTwistSuccIso π p hS n).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS (n + 1))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS n)) (S.frobenius p hS)) h

noncomputable def AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistAddIso {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (m n : ℕ) : CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS m)) (S.iterateFrobenius p hS n) ≅ CategoryTheory.Limits.pullback π (S.iterateFrobenius p hS (m + n))

The n-th Frobenius twist X^{(p^m)} ×_{S, F_S^n} S of the m-th Frobenius twist of X, a scheme over S through its second projection, is the (m + n)-th Frobenius twist of X.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistAddIso_hom_fst {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (m n : ℕ) : CategoryTheory.CategoryStruct.comp (iterateFrobeniusTwistAddIso π p hS m n).hom (CategoryTheory.Limits.pullback.fst π (S.iterateFrobenius p hS (m + n))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS m)) (S.iterateFrobenius p hS n)) (CategoryTheory.Limits.pullback.fst π (S.iterateFrobenius p hS m))

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistAddIso_hom_fst_assoc {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (m n : ℕ) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (iterateFrobeniusTwistAddIso π p hS m n).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π (S.iterateFrobenius p hS (m + n))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS m)) (S.iterateFrobenius p hS n)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π (S.iterateFrobenius p hS m)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistAddIso_hom_snd {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (m n : ℕ) : CategoryTheory.CategoryStruct.comp (iterateFrobeniusTwistAddIso π p hS m n).hom (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS (m + n))) = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS m)) (S.iterateFrobenius p hS n)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.iterateFrobeniusTwistAddIso_hom_snd_assoc {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (m n : ℕ) {Z : Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (iterateFrobeniusTwistAddIso π p hS m n).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS (m + n))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS m)) (S.iterateFrobenius p hS n)) h

theorem AlgebraicGeometry.Scheme.Hom.iterateRelativeFrobenius_zero {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) : CategoryTheory.CategoryStruct.comp (iterateRelativeFrobenius π p hS 0) (iterateFrobeniusTwistZeroIso π p hS).hom = CategoryTheory.CategoryStruct.id X

The zeroth iterated relative Frobenius is the identity, under the identification of the zeroth Frobenius twist of X with X.

theorem AlgebraicGeometry.Scheme.Hom.iterateRelativeFrobenius_zero_assoc {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (iterateRelativeFrobenius π p hS 0) (CategoryTheory.CategoryStruct.comp (iterateFrobeniusTwistZeroIso π p hS).hom h) = h

The zeroth iterated relative Frobenius is the identity, under the identification of the zeroth Frobenius twist of X with X.

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

The first iterated relative Frobenius is the relative Frobenius, under the identification of X ×_{S, F_S^1} S with the Frobenius twist X ×_{S, F_S} S.

theorem AlgebraicGeometry.Scheme.Hom.iterateRelativeFrobenius_one_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 (iterateRelativeFrobenius π p hS 1) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.congrHom ⋯ ⋯).hom h) = CategoryTheory.CategoryStruct.comp (relativeFrobenius π p hS) h

The first iterated relative Frobenius is the relative Frobenius, under the identification of X ×_{S, F_S^1} S with the Frobenius twist X ×_{S, F_S} S.

theorem AlgebraicGeometry.Scheme.Hom.iterateRelativeFrobenius_succ {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (n : ℕ) : iterateRelativeFrobenius π p hS (n + 1) = CategoryTheory.CategoryStruct.comp (iterateRelativeFrobenius π p hS n) (CategoryTheory.CategoryStruct.comp (relativeFrobenius (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS n)) p hS) (iterateFrobeniusTwistSuccIso π p hS n).hom)

The (n + 1)-th iterated relative Frobenius of X is the n-th iterated relative Frobenius X ⟶ X^{(p^n)} followed by the relative Frobenius of the n-th Frobenius twist X^{(p^n)} over S.

theorem AlgebraicGeometry.Scheme.Hom.iterateRelativeFrobenius_add {X S : Scheme} (π : X ⟶ S) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (m n : ℕ) : iterateRelativeFrobenius π p hS (m + n) = CategoryTheory.CategoryStruct.comp (iterateRelativeFrobenius π p hS m) (CategoryTheory.CategoryStruct.comp (iterateRelativeFrobenius (CategoryTheory.Limits.pullback.snd π (S.iterateFrobenius p hS m)) p hS n) (iterateFrobeniusTwistAddIso π p hS m n).hom)

The (m + n)-th iterated relative Frobenius of X is the m-th iterated relative Frobenius X ⟶ X^{(p^m)} followed by the n-th iterated relative Frobenius of the m-th Frobenius twist X^{(p^m)} over S.

theorem AlgebraicGeometry.Scheme.Hom.iterateRelativeFrobenius_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 = π) (n : ℕ) : CategoryTheory.CategoryStruct.comp (iterateRelativeFrobenius π p hS n) (CategoryTheory.Limits.pullback.map π (S.iterateFrobenius p hS n) πY (S.iterateFrobenius p hS n) g (CategoryTheory.CategoryStruct.id S) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) = CategoryTheory.CategoryStruct.comp g (iterateRelativeFrobenius πY p hS n)

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

theorem AlgebraicGeometry.Scheme.Hom.iterateRelativeFrobenius_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 = π) (n : ℕ) {Z : Scheme} (h : CategoryTheory.Limits.pullback πY (S.iterateFrobenius p hS n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (iterateRelativeFrobenius π p hS n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map π (S.iterateFrobenius p hS n) πY (S.iterateFrobenius p hS n) g (CategoryTheory.CategoryStruct.id S) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (iterateRelativeFrobenius πY p hS n) h)

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

@[simp]

theorem AlgebraicGeometry.Scheme.iterateRelativeFrobeniusNatTrans_app_left (S : Scheme) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (n : ℕ) (X : CategoryTheory.Over S) : CategoryTheory.Over.Hom.left ((S.iterateRelativeFrobeniusNatTrans p hS n).app X) = Hom.iterateRelativeFrobenius X.hom p hS n

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

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

@[simp]

theorem AlgebraicGeometry.Scheme.iterateRelativeFrobeniusGrpHom_hom_hom_left (S : Scheme) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (n : ℕ) (G : CategoryTheory.Grp (CategoryTheory.Over S)) : CategoryTheory.Over.Hom.left (S.iterateRelativeFrobeniusGrpHom p hS n G).hom.hom = Hom.iterateRelativeFrobenius G.X.hom p hS n

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

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

@[simp]

theorem AlgebraicGeometry.Scheme.iterateRelativeFrobeniusCommGrpHom_hom_hom_hom_left (S : Scheme) (p : ℕ) [Fact (Nat.Prime p)] (hS : ↑p = 0) (n : ℕ) (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) : CategoryTheory.Over.Hom.left (S.iterateRelativeFrobeniusCommGrpHom p hS n G).hom.hom.hom = Hom.iterateRelativeFrobenius G.X.hom p hS n