Automorphisms acting on the ring of integers

A ring automorphism of a field restricts to its ring of integers, because it preserves integrality. This file records how that restricted action relates to the ambient one: the structure map 𝓞 K → K is equivariant, carrying σ • z to σ applied to the image of z. It also records that restriction to a normal subfield commutes with the map between the two rings of integers.

For a tower F / K of fields it also records that the Gal(F/K)-action on 𝓞 F commutes with the 𝓞 K-scalar action: a K-algebra automorphism fixes K pointwise, hence fixes the image of 𝓞 K. Mathlib supplies the corresponding SMulCommClass only over the base ℤ (integralClosure's own instance, with ℤ the ring 𝓞 F is integral over), which is what a Frobenius over ℚ needs; a relative Frobenius over a general base K needs this one.

𝓞 K is the integral closure of ℤ, and any ring automorphism of K preserves ℤ-integrality, so the base ring R over which σ is linear is irrelevant to both statement and proof; it is a free parameter, specialized to ℚ by the callers. Nothing here needs K to be finite-dimensional either, so [NumberField K] is not assumed.

This is the AlgEquiv specialization of Mathlib's integralClosure.coe_smul, which is stated for an arbitrary [Group G] [MulSemiringAction G K] and therefore cannot phrase the right-hand side as function application. Callers want exactly that applied form, so the specialization is recorded once here rather than reconstructed at each use site.

Main results

• NumberField.algebraMap_smul_eq_apply: algebraMap (𝓞 K) K (σ • z) = σ (algebraMap (𝓞 K) K z).
• NumberField.algebraMap_restrictNormal_smul: mapping the action of a restricted automorphism into the top ring of integers gives the action of the original automorphism.
• NumberField.RingOfIntegers.smulCommClass: Gal(F/K) acting on 𝓞 F commutes with the 𝓞 K-action.
• AlgEquiv.mapAlgEquiv_symm_autCongr_smul: restriction to rings of integers intertwines conjugation of automorphisms along an algebra equivalence.

@[simp]

theorem NumberField.algebraMap_smul_eq_apply {R : Type u_1} {K : Type u_2} [CommSemiring R] [Field K] [Algebra R K] (σ : K ≃ₐ[R] K) (z : RingOfIntegers K) : (algebraMap (RingOfIntegers K) K) (σ • z) = σ ((algebraMap (RingOfIntegers K) K) z)

algebraMap intertwines the automorphism actions on 𝓞 K and on K. The action on the ring of integers is the restriction of the action on K (integralClosure.coe_smul), so the structure map sends σ • z to σ applied to the image of z.

Not named algebraMap_smul: that is Mathlib's unrelated algebraMap R A r • m = r • m.

@[simp]

theorem NumberField.algebraMap_restrictNormal_smul {K : Type u_2} [Field K] {M : Type u_3} {L : Type u_4} [Field M] [Field L] [Algebra K M] [Algebra M L] [Algebra K L] [IsScalarTower K M L] [Normal K M] (σ : Gal(L/K)) (x : RingOfIntegers M) : (algebraMap (RingOfIntegers M) (RingOfIntegers L)) (σ.restrictNormal M • x) = σ • (algebraMap (RingOfIntegers M) (RingOfIntegers L)) x

Restriction of automorphisms commutes with the map between rings of integers. If M/K is normal inside L, then acting on 𝓞 M by the restriction of σ ∈ Gal(L/K) and mapping to 𝓞 L agrees with first mapping and then acting by σ.

instance NumberField.RingOfIntegers.smulCommClass {K : Type u_2} [Field K] {F : Type u_5} [Field F] [Algebra K F] : SMulCommClass Gal(F/K) (RingOfIntegers K) (RingOfIntegers F)

The Galois action on 𝓞 F commutes with the 𝓞 K-action. A K-algebra automorphism of F fixes K pointwise, so it fixes the image of 𝓞 K in F and therefore commutes with multiplication by it.

This is the relative form of Mathlib's SMulCommClass G R (integralClosure R K), which for 𝓞 F = integralClosure ℤ F gives only the base ring ℤ. Neither field has to be a number field.

theorem AlgEquiv.mapAlgEquiv_symm_autCongr_smul {R : Type u_1} {K : Type u_2} {L : Type u_3} [Field R] [Field K] [Field L] [Algebra R K] [Algebra R L] (e : K ≃ₐ[R] L) (σ : Gal(K/R)) (x : NumberField.RingOfIntegers L) : (NumberField.RingOfIntegers.mapAlgEquiv e).symm (e.autCongr σ • x) = σ • (NumberField.RingOfIntegers.mapAlgEquiv e).symm x

Restriction to rings of integers intertwines conjugation of automorphisms along an algebra equivalence.