Semilinear automorphisms acting on places, divisors and Pic⁰-torsion #

Definition: AlgebraicCurve_BaseChangeGalois (4937e59f-5449-57d3-a84a-11e8ddf1962b), by Claude, 2026-09-05.

Fix fields $K \subseteq F$ (an algebra structure algebraMap K F, written $\iota$). The module defines SemilinearAut K F as the subgroup of $\mathrm{Aut}(F) \times \mathrm{Aut}(K)$ (ring automorphisms) consisting of those pairs $(\varphi,\tau)$ with $\varphi(\iota a) = \iota(\tau a)$ for all $a \in K$: automorphisms of $F$ that stabilise the subfield $K$, each packaged with the automorphism of $K$ it induces. The projections are toRingAut and baseAut, with commutes/smul_algebraMap recording the defining identity, and $F$ is given the resulting MulSemiringAction, $g \cdot x = \mathrm{toRingAut}\,g\,(x)$. The monoid homomorphism ofAlgAut sends $\sigma \in F \simeq_{\text{alg}[K]} F$ to $(\sigma, 1)$.

The rest transports this action along the divisor-theoretic constructions of the imported module, where a Place K F is a valuation subring $A \subseteq F$ containing $\iota(K)$, with $A \neq F$ and $A$ a principal ideal ring (hence a discrete valuation ring), $v.\mathrm{ord}$ is the normalised valuation and $v.\deg = \operatorname{finrank}_K$ of the residue field. A place is moved by pointwise translation of its valuation subring; the four structure fields are re-verified, membership of $\iota(K)$ using baseAut, and principality by transporting along the ring isomorphism smulValuationSubringEquiv $A \simeq g \cdot A$. Then ord_smul gives $(g \cdot v).\mathrm{ord}(g \cdot f) = v.\mathrm{ord}(f)$ (proved from a uniformiser-times-unit factorisation), smulResidueRingEquiv is the induced isomorphism of residue fields, semilinear over baseAut g, and deg_smul deduces $\deg(g\cdot v) = \deg v$. Divisors carry the push-forward action (Finsupp.mapDomain), which preserves degree, the degree-zero subgroup and the subgroup of principal divisors, hence descends to $\mathrm{Pic}^0$. Finally $\mathrm{Pic}^0[n]$ (the $\mathbb{Z}$-torsion submodule killed by $n$) is shown stable, given its $\mathbb{Z}/n$-module structure and commuting scalars, and torsionRep K F n is the resulting homomorphism $\mathrm{SemilinearAut}(K,F) \to \operatorname{End}_{\mathbb{Z}/n}(\mathrm{Pic}^0[n])$.

Relation to Mathlib. Mathlib has no notion of the semilinear automorphism group of a field extension, nor of the places, divisors and $\mathrm{Pic}^0$ used here; these are the project's own, assembled from Mathlib components (a Subgroup of RingAut F × RingAut K, Finsupp.comapDistribMulAction, QuotientAddGroup.map, AddCommGroup.zmodModule, DistribMulAction.toModuleEnd). The constructions parallel, and restrict along ofAlgAut to, the actions of $F \simeq_{\text{alg}[K]} F$ already defined in the divisor class group module.

Where it is used. With $F$ a function field of a modular curve over an algebraically closed constant field $K$, torsionRep supplies the action on $\mathrm{Pic}^0[n]$ of automorphisms that move the constants, which is the mechanism by which an absolute Galois group acts on the $n$-torsion of the Jacobian $J_0(N)$; composing a homomorphism into SemilinearAut K F with torsionRep yields the mod-$n$ Galois representations attached to modular Jacobians.