The ideal-theoretic Artin map away from a finite set of primes #
Let L/K be a finite abelian extension of number fields and let S be a finite set of finite
places of K outside which L/K is unramified. At a prime v ∉ S the Artin symbol is a
conjugacy class in an abelian group, hence a single automorphism, and extending that assignment
multiplicatively over the unique factorization of fractional ideals gives the Artin map
artinHomAway : idealsAway S →* (L ≃ₐ[K] L)
on the group idealsAway S of invertible fractional ideals of multiplicity zero along S.
The excluded set S is a parameter: no relation between S and the ramified primes is assumed
beyond the hypothesis hur that every prime outside S is unramified. Specializing S to the
support of the relative discriminant, or to the support of a modulus, is a separate matter.
Commutativity of Gal(L/K) enters as an explicit hypothesis hab rather than as an instance,
because the ambient group is a Galois group of a general extension. Where the construction needs
a bundled commutative structure — for the bijection between the group and its conjugacy classes,
and for the finitely supported product over all primes — the scoped Group plus
IsMulCommutative instance supplies it.
Nothing about the kernel, the image, or a factorization through ray class groups is proved here.
The construction follows Jürgen Neukirch, Algebraic Number Theory, Chapter VI, §7.
Main definitions #
TauCeti.NumberFieldArithmetic.artinElement: the Artin automorphism at an unramified prime.TauCeti.NumberFieldArithmetic.artinElementAway: the local Artin automorphism, extended by1onS.TauCeti.NumberFieldArithmetic.artinHomAway: the Artin map onidealsAway S.TauCeti.NumberFieldArithmetic.artinHomAwayIntegral: its restriction to the integral ideals prime toS.
Main results #
TauCeti.NumberFieldArithmetic.artinHomAway_apply: the value at an ideal is the product of the local Artin automorphisms with the multiplicities of the ideal as exponents.TauCeti.NumberFieldArithmetic.artinHomAway_apply_prime: the value at a prime outsideSis the Frobenius there.TauCeti.NumberFieldArithmetic.artinHomAway_eq_of_apply_prime: those values determine the map.TauCeti.NumberFieldArithmetic.artinHomAway_mono: enlargingSrestricts the map.TauCeti.NumberFieldArithmetic.artinHomAway_restrict: restriction of automorphisms to an intermediate field carries the Artin map ofL/Kto the Artin map ofM/K.
The Artin automorphism at an unramified prime of K in an abelian extension L/K.
This is the unique element of the Artin symbol, taken through the bijection
ConjClasses.mkEquiv between an abelian group and its conjugacy classes.
Equations
Instances For
At an unramified prime, the Artin automorphism represents the Artin symbol.
The Artin automorphism at an unramified prime is an arithmetic Frobenius at every prime above it.
Any arithmetic Frobenius at an unramified prime equals its Artin automorphism.
The Artin automorphism at a finite place of K, extended by 1 inside the excluded set S.
At v ∉ S this is the unique element of the Artin symbol of v, taken through the bijection
ConjClasses.mkEquiv between an abelian group and its conjugacy classes. The commutativity
hypothesis hab is what makes that bijection available, so without it there is no automorphism
here to name and only the class artinSymbol is defined.
Equations
- TauCeti.NumberFieldArithmetic.artinElementAway hab S hur v = if hv : v ∈ S then 1 else TauCeti.NumberFieldArithmetic.artinElement hab v.asIdeal ⋯
Instances For
Inside the excluded set the Artin automorphism is trivial by definition.
Outside the excluded set the Artin automorphism represents the Artin symbol.
The Artin automorphism at v ∉ S is an arithmetic Frobenius at every prime above v.
For a general Galois extension only the conjugacy class of a Frobenius is attached to v; here
the class is a single element, so it is a Frobenius at each prime above v at once.
The Artin automorphism at v ∉ S is the Frobenius there. Any arithmetic Frobenius at any
prime above v equals it, which is what makes the assignment v ↦ artinElementAway hab S hur v
well defined without a choice of prime above v.
The ideal-theoretic Artin map. The multiplicative extension of artinElementAway along
the unique factorization of an invertible fractional ideal, on the group of fractional ideals
with multiplicity zero at every prime of S.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Artin map is the product of the local Artin automorphisms, with the multiplicities of
the ideal as exponents. The product is over all finite places of K, all but finitely many
factors being trivial. It is taken in the commutative structure that hab itself supplies, so
no bundled commutativity is asked of the caller.
The value of the Artin map at a prime outside S is its local Artin automorphism.
The value of the Artin map at a prime outside S is the Frobenius there.
The values on the primes outside S determine the Artin map. The carrier is generated by
those primes, so a homomorphism taking the Frobenius value at each of them is the Artin map.
Enlarging the excluded set restricts the Artin map. For S ⊆ S' the Artin map for S'
is the Artin map for S composed with the inclusion of carriers.
The Artin map is functorial in the top field. Restriction of automorphisms to a normal
intermediate field M carries the Artin map of L/K to the Artin map of M/K, over the same
excluded set and with both the commutativity and the unramifiedness hypothesis for M/K derived
from the ones for L/K.
The integral Artin homomorphism. The Artin map read on the monoid of nonzero integral
ideals divisible by no prime of S; this is the shape the classical statements take.
Equations
Instances For
The integral Artin homomorphism is the Artin map read through the inclusion of the integral
ideals prime to S into idealsAway S.
The value of the integral Artin homomorphism at a prime outside S is the Frobenius
there.