Relative Frobenius on affine coordinate rings

For a Weierstrass curve W over a commutative ring of exponential characteristic p, this file constructs the relative Frobenius map from the coordinate ring of the Frobenius twist W.map (frobenius R p) to W.CoordinateRing. It sends the two coordinates to their p-th powers and factors the absolute Frobenius through Mathlib's base-change map.

Main definitions

• WeierstrassCurve.Affine.CoordinateRing.relativeFrobenius: the relative Frobenius on coordinate rings.
• WeierstrassCurve.Affine.CoordinateRing.iterateRelativeFrobenius: its n-fold iterate, from the coordinate ring of W.map (iterateFrobenius R p n) to that of W.

Main results

• WeierstrassCurve.Affine.expChar_coordinateRing: a coordinate ring has the same exponential characteristic as its base ring, so the absolute Frobenius of the coordinate ring is available.
• relativeFrobenius_comp_map: composing relative Frobenius with the base-change map recovers absolute Frobenius.
• relativeFrobenius_map: the pointwise form of that identity.
• iterateRelativeFrobenius_comp_map: the iterated coefficient Frobenius followed by the iterated relative Frobenius is the p ^ n-power map.

Roadmap

TauCetiRoadmap/EllipticCurves/README.md, Layer 1, the relative Frobenius milestone. This is the coordinate-ring construction underlying the function-field pullback and isogeny.

Provenance

Not a port. The pinned sources build only the absolute finite-field Frobenius; the relative Frobenius over an arbitrary commutative base appears in none of them. The exponential-characteristic instance is the direct transport along Mathlib's injective coordinate-ring algebra map.

instance WeierstrassCurve.Affine.expChar_coordinateRing {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (W : Affine R) : ExpChar W.CoordinateRing p

The coordinate ring of a Weierstrass curve has the same exponential characteristic as its base ring.

noncomputable def WeierstrassCurve.Affine.CoordinateRing.relativeFrobenius {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (W : Affine R) : (W.map (frobenius R p)).CoordinateRing →ₐ[R] W.CoordinateRing

The relative Frobenius on coordinate rings: the R-algebra map out of the coordinate ring of the Frobenius twist W⁽ᵖ⁾ that sends its two coordinates to the p-th powers of the coordinates of W.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.relativeFrobenius_of {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (W : Affine R) (g : Polynomial R) : (relativeFrobenius p W) ((AdjoinRoot.of (W.map (frobenius R p)).polynomial) g) = (AdjoinRoot.of W.polynomial) ((Polynomial.expand R p) g)

The relative Frobenius substitutes X ^ p into a polynomial in the affine coordinate.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.relativeFrobenius_root {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (W : Affine R) : (relativeFrobenius p W) (AdjoinRoot.root (W.map (frobenius R p)).polynomial) = AdjoinRoot.root W.polynomial ^ p

The relative Frobenius sends the second coordinate of the twist to y ^ p.

theorem WeierstrassCurve.Affine.CoordinateRing.relativeFrobenius_comp_map {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (W : Affine R) : (relativeFrobenius p W).comp (map W (frobenius R p)) = frobenius W.CoordinateRing p

The absolute Frobenius factors through the twist. Mathlib's base-change map W.CoordinateRing →+* (W.map (frobenius R p)).CoordinateRing is semilinear over the coefficient Frobenius; composing the relative Frobenius with it recovers the p-power map of W.CoordinateRing.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.relativeFrobenius_map {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (W : Affine R) (z : W.CoordinateRing) : (relativeFrobenius p W) ((map W (frobenius R p)) z) = z ^ p

The pointwise form of relativeFrobenius_comp_map.

Iterated relative Frobenius

noncomputable def WeierstrassCurve.Affine.CoordinateRing.iterateRelativeFrobenius {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (W : Affine R) (n : ℕ) : (W.map (iterateFrobenius R p n)).CoordinateRing →ₐ[R] W.CoordinateRing

The iterated relative Frobenius on coordinate rings. It maps the coordinate ring of the n-th Frobenius twist W.map (iterateFrobenius R p n) to W.CoordinateRing, sending the two coordinates to their p ^ n-th powers.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.iterateRelativeFrobenius_of {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (W : Affine R) (n : ℕ) (g : Polynomial R) : (iterateRelativeFrobenius p W n) ((AdjoinRoot.of (W.map (iterateFrobenius R p n)).polynomial) g) = (AdjoinRoot.of W.polynomial) ((Polynomial.expand R (p ^ n)) g)

The iterated relative Frobenius substitutes X ^ (p ^ n) into a polynomial in the affine coordinate.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.iterateRelativeFrobenius_root {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (W : Affine R) (n : ℕ) : (iterateRelativeFrobenius p W n) (AdjoinRoot.root (W.map (iterateFrobenius R p n)).polynomial) = AdjoinRoot.root W.polynomial ^ p ^ n

The iterated relative Frobenius sends the second coordinate of the twist to its p ^ n-th power.

theorem WeierstrassCurve.Affine.CoordinateRing.iterateRelativeFrobenius_comp_map {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (W : Affine R) (n : ℕ) : (iterateRelativeFrobenius p W n).comp (map W (iterateFrobenius R p n)) = iterateFrobenius W.CoordinateRing p n

The iterated absolute Frobenius factors through the n-th twist. Composing the coefficient map with the iterated relative Frobenius is the p ^ n-power map on W.CoordinateRing.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.iterateRelativeFrobenius_map {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p] (W : Affine R) (n : ℕ) (z : W.CoordinateRing) : (iterateRelativeFrobenius p W n) ((map W (iterateFrobenius R p n)) z) = z ^ p ^ n

Pointwise form of iterateRelativeFrobenius_comp_map.