ClassFieldTheory.arithmeticFrobeniusAt_mapAlgEquiv
In an abelian extension, transporting an unramified prime by a K-automorphism does not change its arithmetic Frobenius element.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u vLean source · statement
theorem arithmeticFrobeniusAt_mapAlgEquiv
{K : Type u} {L : Type v}
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
[IsAbelianGalois K L]
(v : HeightOneSpectrum (𝓞 K))
(w : HeightOneSpectrum (𝓞 L))
(hw : w.asIdeal.LiesOver v.asIdeal)
(σ : L ≃ₐ[K] L)
(hunram : Algebra.IsUnramifiedAt (𝓞 K) w.asIdeal) :
arithmeticFrobeniusAt (K := K)
((HeightOneSpectrum.equivOfRingEquiv
(RingOfIntegers.mapAlgEquiv σ).toRingEquiv) w) =
arithmeticFrobeniusAt (K := K) w