The unramified ideal Artin map

This file develops the part of the ideal-theoretic Artin map that follows from Dedekind factorization and local Frobenius theory. For a finite Galois extension of number fields it chooses a prime above every finite prime and defines the corresponding arithmetic Frobenius. In an abelian extension the choice disappears, since Frobenius elements above the same prime are conjugate. The local symbols then extend uniquely to a homomorphism from the group of nonzero fractional ideals.

The construction here is deliberately separate from global reciprocity. The two global assertions needed later are that principal ideals lie in the kernel, and that the resulting Artin map is onto. Neither assertion is used in this file.

The divisor equivalence below is the scheme-free Dedekind-domain core of the construction in Tau Ceti's AlgebraicGeometry/WeilDivisor/FractionalIdealDivisor/Basic.lean; it is reproved here directly from Mathlib's fractional-ideal factorization API so this number-theory module does not depend on Picard or Weil-divisor theory.

@[reducible, inline]

abbrev NumberTheory.UnramifiedArtin.FinitePrime (K : Type u_1) [Field K] : Type u_1

A finite prime of a number field, represented by a nonzero prime ideal in its ring of integers.

Equations

• NumberTheory.UnramifiedArtin.FinitePrime K = IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)

theorem NumberTheory.UnramifiedArtin.stabilizer_eq_zpowers_of_isArithFrobAt {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Group G] [Finite G] [MulSemiringAction G S] [SMulCommClass G R S] [IsGaloisGroup G R S] [IsDomain R] [IsDomain S] [Module.Finite R S] [Module.Flat R S] (p : Ideal R) (Q : Ideal S) [p.IsPrime] [Q.IsPrime] [Q.LiesOver p] [Finite (S ⧸ Q)] [PerfectField p.ResidueField] [Algebra.IsUnramifiedAt R Q] {σ : G} (hσ : IsArithFrobAt R σ Q) : Subgroup.zpowers σ = MulAction.stabilizer G Q

At an unramified prime, an arithmetic Frobenius generates the full decomposition group.

noncomputable def NumberTheory.UnramifiedArtin.primeAbove {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] (v : FinitePrime K) : ↑(v.asIdeal.primesOver (NumberField.RingOfIntegers L))

An arbitrary prime of L above the finite prime v of K.

Equations

• NumberTheory.UnramifiedArtin.primeAbove v = Classical.choice ⋯

noncomputable def NumberTheory.UnramifiedArtin.frobeniusAt {K : Type u} {L : Type v} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (v : FinitePrime K) : Gal(L/K)

The chosen arithmetic Frobenius at a finite prime of the base number field.

Equations

• NumberTheory.UnramifiedArtin.frobeniusAt v = arithFrobAt (NumberField.RingOfIntegers K) Gal(L/K) ↑(NumberTheory.UnramifiedArtin.primeAbove v)

theorem NumberTheory.UnramifiedArtin.frobeniusAt_isArithFrobAt {K : Type u} {L : Type v} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (v : FinitePrime K) : IsArithFrobAt (NumberField.RingOfIntegers K) (frobeniusAt v) ↑(primeAbove v)

The chosen element really is an arithmetic Frobenius at the chosen prime above v.

theorem NumberTheory.UnramifiedArtin.frobeniusAt_eq_arithFrobAt {K : Type u} {L : Type v} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsMulCommutative Gal(L/K)] (v : FinitePrime K) (Q : ↑(v.asIdeal.primesOver (NumberField.RingOfIntegers L))) : frobeniusAt v = arithFrobAt (NumberField.RingOfIntegers K) Gal(L/K) ↑Q

In an abelian extension, the Frobenius at v is independent of the prime of L chosen above v.

theorem NumberTheory.UnramifiedArtin.arithFrobAt_unique_of_unramified {K : Type u} {L : Type v} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (v : FinitePrime K) (hunramified : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers L) v.asIdeal) (Q : ↑(v.asIdeal.primesOver (NumberField.RingOfIntegers L))) (τ : Gal(L/K)) (hτ : IsArithFrobAt (NumberField.RingOfIntegers K) τ ↑Q) : τ = arithFrobAt (NumberField.RingOfIntegers K) Gal(L/K) ↑Q

At an unramified finite prime, an arithmetic Frobenius at a fixed prime above it is unique. This is the strongest local uniqueness statement needed by the ideal Artin construction.

def NumberTheory.UnramifiedArtin.semilinearConjugate {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (eR : R ≃+* R) (eS : S ≃+* S) (hsemilinear : ∀ (r : R), eS ((algebraMap R S) r) = (algebraMap R S) (eR r)) (f : S →ₐ[R] S) : S →ₐ[R] S

Conjugate an R-algebra endomorphism by a ring equivalence of S that is semilinear for a ring equivalence of R. The two semilinear twists cancel, so the conjugate is again R-linear.

Equations

• NumberTheory.UnramifiedArtin.semilinearConjugate eR eS hsemilinear f = { toRingHom := eS.toRingHom.comp (f.comp eS.symm.toRingHom), commutes' := ⋯ }

@[simp]

theorem NumberTheory.UnramifiedArtin.semilinearConjugate_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (eR : R ≃+* R) (eS : S ≃+* S) (hsemilinear : ∀ (r : R), eS ((algebraMap R S) r) = (algebraMap R S) (eR r)) (f : S →ₐ[R] S) (x : S) : (semilinearConjugate eR eS hsemilinear f) x = eS (f (eS.symm x))

Pointwise formula for semilinear conjugation.

theorem NumberTheory.UnramifiedArtin.under_map_semilinear {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (eR : R ≃+* R) (eS : S ≃+* S) (hsemilinear : ∀ (r : R), eS ((algebraMap R S) r) = (algebraMap R S) (eR r)) (Q : Ideal S) : Ideal.under R (Ideal.map eS Q) = Ideal.map eR (Ideal.under R Q)

Under a semilinear equivalence of an algebra, transporting a prime of the extension transports its underlying base prime by the base equivalence.

theorem NumberTheory.UnramifiedArtin.card_quotient_under_map_semilinear {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (eR : R ≃+* R) (eS : S ≃+* S) (hsemilinear : ∀ (r : R), eS ((algebraMap R S) r) = (algebraMap R S) (eR r)) (Q : Ideal S) : Nat.card (R ⧸ Ideal.under R (Ideal.map eS Q)) = Nat.card (R ⧸ Ideal.under R Q)

A semilinear transport preserves the cardinality of the base residue field below a prime.

theorem NumberTheory.UnramifiedArtin.isArithFrobAt_semilinearConjugate {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (eR : R ≃+* R) (eS : S ≃+* S) (hsemilinear : ∀ (r : R), eS ((algebraMap R S) r) = (algebraMap R S) (eR r)) {f : S →ₐ[R] S} {Q : Ideal S} (hf : f.IsArithFrobAt Q) : (semilinearConjugate eR eS hsemilinear f).IsArithFrobAt (Ideal.map eS Q)

Arithmetic Frobenius congruences are preserved by compatible semilinear transport of the base and extension rings.

theorem NumberTheory.UnramifiedArtin.asIdeal_equivOfRingEquiv {R : Type u} [CommRing R] (e : R ≃+* R) (v : IsDedekindDomain.HeightOneSpectrum R) : ((IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv e) v).asIdeal = Ideal.map e v.asIdeal

Transporting a height-one prime along a ring equivalence maps its ideal to the image ideal.

theorem NumberTheory.UnramifiedArtin.ringEquivOfRingEquiv_coeIdeal (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (g : R ≃+* R) (I : Ideal R) : (FractionalIdeal.ringEquivOfRingEquiv K K g) ↑I = ↑(Ideal.map g I)

The semilinear fractional-ideal equivalence induced by a ring automorphism sends an integral ideal to its ordinary image ideal.

noncomputable def NumberTheory.UnramifiedArtin.fractionalIdealDivisor (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : Additive (FractionalIdeal (nonZeroDivisors R) K)ˣ →+ IsDedekindDomain.HeightOneSpectrum R →₀ ℤ

The finitely supported multiplicity divisor of an invertible fractional ideal.

Equations

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

@[simp]

theorem NumberTheory.UnramifiedArtin.fractionalIdealDivisor_apply (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (I : Additive (FractionalIdeal (nonZeroDivisors R) K)ˣ) (x : IsDedekindDomain.HeightOneSpectrum R) : ((fractionalIdealDivisor R K) I) x = FractionalIdeal.count K x ↑(Additive.toMul I)

The coefficient of the fractional-ideal divisor is Mathlib's local multiplicity.

theorem NumberTheory.UnramifiedArtin.fractionalIdealDivisor_injective (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : Function.Injective ⇑(fractionalIdealDivisor R K)

A nonzero fractional ideal is recovered from all of its finite-prime multiplicities.

theorem NumberTheory.UnramifiedArtin.prod_asIdeal_zpow_ne_zero (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (D : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ) : (D.prod fun (x : IsDedekindDomain.HeightOneSpectrum R) (e : ℤ) => ↑x.asIdeal ^ e) ≠ 0

The fractional ideal attached to a finitely supported integer divisor is nonzero.

theorem NumberTheory.UnramifiedArtin.fractionalIdealDivisor_surjective (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : Function.Surjective ⇑(fractionalIdealDivisor R K)

Every finitely supported integer divisor is the divisor of a nonzero fractional ideal.

noncomputable def NumberTheory.UnramifiedArtin.fractionalIdealDivisorAddEquiv (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : Additive (FractionalIdeal (nonZeroDivisors R) K)ˣ ≃+ (IsDedekindDomain.HeightOneSpectrum R →₀ ℤ)

Nonzero fractional ideals form the free abelian group on the finite primes of a Dedekind domain.

Equations

• NumberTheory.UnramifiedArtin.fractionalIdealDivisorAddEquiv R K = AddEquiv.ofBijective (NumberTheory.UnramifiedArtin.fractionalIdealDivisor R K) ⋯

@[simp]

theorem NumberTheory.UnramifiedArtin.fractionalIdealDivisor_prime {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] (x : IsDedekindDomain.HeightOneSpectrum R) : (fractionalIdealDivisor R K) (Additive.ofMul (Units.mk0 ↑x.asIdeal ⋯)) = Finsupp.single x 1

The divisor of a prime fractional ideal is the corresponding standard basis divisor.

noncomputable def NumberTheory.UnramifiedArtin.fractionalIdealDivisorMulEquiv {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] : (FractionalIdeal (nonZeroDivisors R) K)ˣ ≃* Multiplicative (IsDedekindDomain.HeightOneSpectrum R →₀ ℤ)

The multiplicative form of the divisor equivalence for nonzero fractional ideals.

Equations

• NumberTheory.UnramifiedArtin.fractionalIdealDivisorMulEquiv = AddEquiv.toMultiplicativeRight (NumberTheory.UnramifiedArtin.fractionalIdealDivisorAddEquiv R K)

noncomputable def NumberTheory.UnramifiedArtin.primeFractionalIdealUnit {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] (x : IsDedekindDomain.HeightOneSpectrum R) : (FractionalIdeal (nonZeroDivisors R) K)ˣ

The unit of the fractional-ideal monoid represented by a finite prime.

Equations

• NumberTheory.UnramifiedArtin.primeFractionalIdealUnit x = Units.mk0 ↑x.asIdeal ⋯

@[simp]

theorem NumberTheory.UnramifiedArtin.fractionalIdealDivisorMulEquiv_prime {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] (x : IsDedekindDomain.HeightOneSpectrum R) : fractionalIdealDivisorMulEquiv (primeFractionalIdealUnit x) = Multiplicative.ofAdd (Finsupp.single x 1)

Under the multiplicative divisor equivalence, a finite prime is its standard basis divisor.

theorem NumberTheory.UnramifiedArtin.fractionalIdealMonoidHom_ext {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] {f g : (FractionalIdeal (nonZeroDivisors R) K)ˣ →* M} (h : ∀ (x : IsDedekindDomain.HeightOneSpectrum R), f (primeFractionalIdealUnit x) = g (primeFractionalIdealUnit x)) : f = g

Homomorphisms out of the fractional-ideal group are determined by their values on finite prime ideals.

noncomputable def NumberTheory.UnramifiedArtin.freeAbelianHom {R : Type u} [CommRing R] {M : Type w} [CommGroup M] (c : IsDedekindDomain.HeightOneSpectrum R → M) : Multiplicative (IsDedekindDomain.HeightOneSpectrum R →₀ ℤ) →* M

Extend a family of values on the generators of a free abelian group to a homomorphism.

Equations

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

@[simp]

theorem NumberTheory.UnramifiedArtin.freeAbelianHom_single {R : Type u} [CommRing R] {M : Type w} [CommGroup M] (c : IsDedekindDomain.HeightOneSpectrum R → M) (x : IsDedekindDomain.HeightOneSpectrum R) : (freeAbelianHom c) (Multiplicative.ofAdd (Finsupp.single x 1)) = c x

The free extension takes a standard basis divisor to its prescribed value.

theorem NumberTheory.UnramifiedArtin.freeAbelianHom_apply {R : Type u} [CommRing R] {M : Type w} [CommGroup M] (c : IsDedekindDomain.HeightOneSpectrum R → M) (D : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ) : (freeAbelianHom c) (Multiplicative.ofAdd D) = D.prod fun (x : IsDedekindDomain.HeightOneSpectrum R) (n : ℤ) => c x ^ n

The free extension is the finite product of the prescribed generator values raised to their integer multiplicities.

theorem NumberTheory.UnramifiedArtin.freeAbelianHom_comp {R : Type u} [CommRing R] {M : Type w} [CommGroup M] {N : Type w'} [CommGroup N] (f : M →* N) (c : IsDedekindDomain.HeightOneSpectrum R → M) : f.comp (freeAbelianHom c) = freeAbelianHom fun (x : IsDedekindDomain.HeightOneSpectrum R) => f (c x)

Extending values on generators commutes with a homomorphism of target groups.

noncomputable def NumberTheory.UnramifiedArtin.fractionalIdealHom {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] (c : IsDedekindDomain.HeightOneSpectrum R → M) : (FractionalIdeal (nonZeroDivisors R) K)ˣ →* M

The homomorphism from nonzero fractional ideals obtained by prescribing a value at every finite prime.

Equations

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

@[simp]

theorem NumberTheory.UnramifiedArtin.fractionalIdealHom_prime {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] (c : IsDedekindDomain.HeightOneSpectrum R → M) (x : IsDedekindDomain.HeightOneSpectrum R) : (fractionalIdealHom c) (Units.mk0 ↑x.asIdeal ⋯) = c x

The fractional-ideal homomorphism has the prescribed value on each prime ideal.

theorem NumberTheory.UnramifiedArtin.fractionalIdealHom_apply {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] (c : IsDedekindDomain.HeightOneSpectrum R → M) (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : (fractionalIdealHom c) I = ((fractionalIdealDivisor R K) (Additive.ofMul I)).prod fun (x : IsDedekindDomain.HeightOneSpectrum R) (n : ℤ) => c x ^ n

The fractional-ideal homomorphism is the finite Artin product over the prime factorization of the ideal.

theorem NumberTheory.UnramifiedArtin.fractionalIdealHom_comp {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] {N : Type w'} [CommGroup N] (f : M →* N) (c : IsDedekindDomain.HeightOneSpectrum R → M) : f.comp (fractionalIdealHom c) = fractionalIdealHom fun (x : IsDedekindDomain.HeightOneSpectrum R) => f (c x)

Postcomposition of a fractional-ideal homomorphism is computed locally on its prime symbols.

theorem NumberTheory.UnramifiedArtin.fractionalIdealHom_range {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] (c : IsDedekindDomain.HeightOneSpectrum R → M) : (fractionalIdealHom c).range = Subgroup.closure (Set.range c)

The image of a fractional-ideal homomorphism is exactly the subgroup generated by its finite-prime symbols.

theorem NumberTheory.UnramifiedArtin.fractionalIdealHom_surjective_iff {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] (c : IsDedekindDomain.HeightOneSpectrum R → M) : Function.Surjective ⇑(fractionalIdealHom c) ↔ Subgroup.closure (Set.range c) = ⊤

Surjectivity of the fractional-ideal homomorphism is equivalent to generation of the target by its finite-prime symbols.

noncomputable def NumberTheory.UnramifiedArtin.classGroupEquiv (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (g : R ≃+* R) : ClassGroup R ≃* ClassGroup R

The class-group automorphism induced by a ring automorphism, expressed in the chosen fraction field K. This computational form agrees with the canonical construction but has a direct formula on ClassGroup.mk K.

Equations

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

theorem NumberTheory.UnramifiedArtin.classGroupEquiv_mk (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (g : R ≃+* R) (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : (classGroupEquiv R K g) ((ClassGroup.mk K) I) = (ClassGroup.mk K) ((Units.mapEquiv (FractionalIdeal.ringEquivOfRingEquiv K K g).toMulEquiv) I)

Formula for the induced class-group automorphism on a represented fractional ideal.

def NumberTheory.UnramifiedArtin.KillsPrincipalIdeals (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] (φ : (FractionalIdeal (nonZeroDivisors R) K)ˣ →* M) : Prop

The exact conductor-one reciprocity condition needed for an ideal homomorphism to descend to the ordinary ideal class group.

Equations

• NumberTheory.UnramifiedArtin.KillsPrincipalIdeals R K φ = ∀ (x : Kˣ), φ ((toPrincipalIdeal R K) x) = 1

theorem NumberTheory.UnramifiedArtin.principalIdeals_le_ker (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] (φ : (FractionalIdeal (nonZeroDivisors R) K)ˣ →* M) (hprincipal : KillsPrincipalIdeals R K φ) : (toPrincipalIdeal R K).range ≤ φ.ker

The principal fractional-ideal subgroup lies in the kernel of an ideal homomorphism satisfying conductor-one reciprocity.

noncomputable def NumberTheory.UnramifiedArtin.classGroupHom (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] (φ : (FractionalIdeal (nonZeroDivisors R) K)ˣ →* M) (hprincipal : KillsPrincipalIdeals R K φ) : ClassGroup R →* M

Descend an ideal homomorphism that kills principal ideals to the ordinary ideal class group.

Equations

• NumberTheory.UnramifiedArtin.classGroupHom R K φ hprincipal = (QuotientGroup.lift (toPrincipalIdeal R K).range φ ⋯).comp (ClassGroup.equiv K).toMonoidHom

theorem NumberTheory.UnramifiedArtin.classGroupHom_mk (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] (φ : (FractionalIdeal (nonZeroDivisors R) K)ˣ →* M) (hprincipal : KillsPrincipalIdeals R K φ) (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : (classGroupHom R K φ hprincipal) ((ClassGroup.mk K) I) = φ I

The descended class-group map agrees with the original ideal map on the canonical class of a fractional ideal.

theorem NumberTheory.UnramifiedArtin.classGroupHom_surjective (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] (φ : (FractionalIdeal (nonZeroDivisors R) K)ˣ →* M) (hprincipal : KillsPrincipalIdeals R K φ) (hsurjective : Function.Surjective ⇑φ) : Function.Surjective ⇑(classGroupHom R K φ hprincipal)

Surjectivity of an ideal homomorphism passes to its class-group descent.

theorem NumberTheory.UnramifiedArtin.classGroupHom_surjective_iff (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] (φ : (FractionalIdeal (nonZeroDivisors R) K)ˣ →* M) (hprincipal : KillsPrincipalIdeals R K φ) : Function.Surjective ⇑(classGroupHom R K φ hprincipal) ↔ Function.Surjective ⇑φ

The class-group descent is onto exactly when the original fractional-ideal homomorphism is onto.

theorem NumberTheory.UnramifiedArtin.classGroupHom_surjective_iff_generators (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] {M : Type w} [CommGroup M] (c : IsDedekindDomain.HeightOneSpectrum R → M) (hprincipal : KillsPrincipalIdeals R K (fractionalIdealHom c)) : Function.Surjective ⇑(classGroupHom R K (fractionalIdealHom c) hprincipal) ↔ Subgroup.closure (Set.range c) = ⊤

After principal reciprocity, the class-group map is onto exactly when its finite-prime symbols generate the target. This identifies the precise Frobenius-generation input supplied classically by Chebotarev or the global Artin existence theorem.

noncomputable def NumberTheory.UnramifiedArtin.fractionalArtin {K : Type u} {L : Type v} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsMulCommutative Gal(L/K)] : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ →* Gal(L/K)

The ideal-theoretic arithmetic Frobenius homomorphism of an abelian extension, before applying global reciprocity to principal ideals.

Equations

• NumberTheory.UnramifiedArtin.fractionalArtin = NumberTheory.UnramifiedArtin.fractionalIdealHom NumberTheory.UnramifiedArtin.frobeniusAt

@[simp]

theorem NumberTheory.UnramifiedArtin.fractionalArtin_prime {K : Type u} {L : Type v} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsMulCommutative Gal(L/K)] (x : FinitePrime K) : fractionalArtin (Units.mk0 ↑x.asIdeal ⋯) = frobeniusAt x

The fractional Artin map sends a prime ideal to its arithmetic Frobenius.