Artin map

DefinitionA prime as an invertible fractional ideal#✓fully proved

For a number field \(K\) with ring of integers \(\mathcal O_K\) and a height-one prime \(\mathfrak p\) of \(\mathcal O_K\), this is \(\mathfrak p\) regarded as a fractional ideal of \(K\); it is nonzero, hence a unit in the group of nonzero fractional ideals of \(K\).

noncomputable def primeUnitFractionalIdeal
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) :
    (FractionalIdeal (𝓞 K)⁰ K)ˣ :=
  Units.mk0 (v.asIdeal : FractionalIdeal (𝓞 K)⁰ K)
    (FractionalIdeal.coeIdeal_ne_zero.mpr v.ne_bot)

Used by 5

Used byThe coprime primes generate the coprime ideals · Factorization of a prime of a number field · The kernel of the free-group map lies in the commutator subgroup · Primes not dividing the modulus are coprime to it · The prime as a coprime fractional ideal

TheoremFactorization of a prime of a number field#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal O_K\) and let \(\mathfrak p\) be a height-one prime of \(\mathcal O_K\). The factorization isomorphism sends \(\mathfrak p\), regarded as an invertible fractional ideal of \(K\), to the function on height-one primes of \(\mathcal O_K\) that is \(1\) at \(\mathfrak p\) and \(0\) elsewhere.

theorem _root_.FractionalIdeal.factorizationMulEquiv_primeUnitFractionalIdeal
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) :
    Multiplicative.toAdd (FractionalIdeal.factorizationMulEquiv K
      (primeUnitFractionalIdeal v)) = Finsupp.single v 1

Uses 3 · Used by 2

Statement usesPrime factorization isomorphism for fractional ideals · A prime as an invertible fractional ideal

Proof usesExponent function of a prime ideal

Used byThe kernel of the free-group map lies in the commutator subgroup · Primes not dividing the modulus are coprime to it

TheoremPrimes not dividing the modulus are coprime to it#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\) and let \(\mathfrak p\) be a height-one prime of the ring of integers \(\mathcal O_K\) that does not contain the finite part of \(\mathfrak m\). Then \(\mathfrak p\), viewed as an invertible fractional ideal of \(K\), lies in the group of fractional ideals coprime to \(\mathfrak m\): its exponent at every height-one prime containing the finite part of \(\mathfrak m\) is zero.

theorem mem_coprimeFractionalIdeals_primeUnit (hvm : ¬ m.finiteSupported v) :
    primeUnitFractionalIdeal v ∈ m.coprimeFractionalIdeals

Uses 5 · Used by 1

Statement usesFractional ideals coprime to a modulus · Primes dividing a modulus · A prime as an invertible fractional ideal

Proof usesPrime factorization isomorphism for fractional ideals · Factorization of a prime of a number field

Used byThe prime as a coprime fractional ideal

DefinitionThe prime as a coprime fractional ideal#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\) and let \(\mathfrak p\) be a height-one prime of the ring of integers \(\mathcal O_K\) that does not contain the finite part of \(\mathfrak m\). This is \(\mathfrak p\), viewed as an invertible fractional ideal of \(K\), regarded as an element of the group of fractional ideals coprime to \(\mathfrak m\).

noncomputable def primeCoprimeUnit (hvm : ¬ m.finiteSupported v) :
    m.coprimeFractionalIdeals :=
  ⟨primeUnitFractionalIdeal v, mem_coprimeFractionalIdeals_primeUnit m v hvm⟩

Uses 4 · Used by 11

Statement usesFractional ideals coprime to a modulus · Primes dividing a modulus · Primes not dividing the modulus are coprime to it · A prime as an invertible fractional ideal

Used byThe Artin map at a prime · The coprime primes generate the coprime ideals · Prime coprime units · The prime coprime units are the image of the coprime primes · The free group on the coprime primes maps to the coprime ideals · The kernel of the free-group map lies in the commutator subgroup · The free-group map on generators · The free group on the coprime primes surjects onto the coprime ideals · Membership in the prime coprime units · Restriction of the Artin map at a prime · The Artin map commutes with restriction

AbbreviationPrimes coprime to a modulus#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\). The primes coprime to \(\mathfrak m\) are the nonzero prime ideals \(\mathfrak p\) of the ring of integers \(\mathcal O_K\) that do not contain the finite part of \(\mathfrak m\), that is, that do not divide it. They index the generators of a free group that maps to the group of fractional ideals coprime to the finite part of \(\mathfrak m\).

abbrev CoprimePrimes :=
  { v : IsDedekindDomain.HeightOneSpectrum (𝓞 K) // ¬ m.finiteSupported v }

Uses 1 · Used by 17

Statement usesPrimes dividing a modulus

Used byArtin map · The Artin map factors the free-group Frobenius map · The Artin map at a prime · Unramified outside a modulus implies unramified at coprime primes · The prime coprime units are the image of the coprime primes · The free group on the coprime primes maps to the coprime ideals · The kernel of the free-group map is the commutator subgroup · The kernel of the free-group map lies in the commutator subgroup · Kernel containment for the free-group Frobenius map · The free-group map on generators · The free group on the coprime primes surjects onto the coprime ideals · Frobenius homomorphism on the free group of coprime primes · The Frobenius homomorphism on generators · Chosen Frobenius element at a coprime prime · The chosen Frobenius is an arithmetic Frobenius at an unramified prime · The Artin map commutes with restriction · Restriction of Frobenius elements in a tower

DefinitionPrime coprime units#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), and let \(I_K^{\mathfrak m}\) be the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\). The prime coprime units of \(\mathfrak m\) are the elements of \(I_K^{\mathfrak m}\) of the form \(\mathfrak p\), where \(\mathfrak p\) is a nonzero prime ideal of the ring of integers \(\mathcal O_K\) that does not divide the finite part of \(\mathfrak m\).

def coprimePrimeUnits : Set m.coprimeFractionalIdeals :=
  { I | ∃ (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
    (hvm : ¬ m.finiteSupported v), I = m.primeCoprimeUnit v hvm }

Uses 3 · Used by 4

Statement usesFractional ideals coprime to a modulus · Primes dividing a modulus · The prime as a coprime fractional ideal

Used byThe coprime primes generate the coprime ideals · The prime coprime units are the image of the coprime primes · The free group on the coprime primes surjects onto the coprime ideals · Membership in the prime coprime units

TheoremMembership in the prime coprime units#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), and let \(I_K^{\mathfrak m}\) be the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\). An element \(I\) of \(I_K^{\mathfrak m}\) is a prime coprime unit of \(\mathfrak m\) if and only if \(I = \mathfrak p\) for some nonzero prime ideal \(\mathfrak p\) of the ring of integers \(\mathcal O_K\) that does not divide the finite part of \(\mathfrak m\).

theorem mem_coprimePrimeUnits (I : m.coprimeFractionalIdeals) :
    I ∈ m.coprimePrimeUnits ↔
      ∃ (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
        (hvm : ¬ m.finiteSupported v), I = m.primeCoprimeUnit v hvm

Uses 4 · Used by 2

Statement usesFractional ideals coprime to a modulus · Prime coprime units · Primes dividing a modulus · The prime as a coprime fractional ideal

Used byThe coprime primes generate the coprime ideals · The prime coprime units are the image of the coprime primes

TheoremThe prime coprime units are the image of the coprime primes#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), let \(I_K^{\mathfrak m}\) be the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\), and let \(P\) be the set of nonzero prime ideals of the ring of integers \(\mathcal O_K\) that do not divide the finite part of \(\mathfrak m\). Then the set of prime coprime units of \(\mathfrak m\) equals the range of the map \(P \to I_K^{\mathfrak m}\) sending each \(\mathfrak p \in P\) to \(\mathfrak p\) viewed as an element of \(I_K^{\mathfrak m}\).

theorem coprimePrimeUnits_eq_range :
    m.coprimePrimeUnits =
      Set.range (fun p : m.CoprimePrimes => m.primeCoprimeUnit p.val p.property)

Sources

• direct native counterpart of ATLAS primesCoprime_eq_range.

Uses 6 · Used by 1

Statement usesPrimes coprime to a modulus · Fractional ideals coprime to a modulus · Prime coprime units · Primes dividing a modulus · The prime as a coprime fractional ideal

Proof usesMembership in the prime coprime units

Used byThe free group on the coprime primes surjects onto the coprime ideals

TheoremThe coprime primes generate the coprime ideals#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), and let \(I_K^{\mathfrak m}\) be the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\). Then \(I_K^{\mathfrak m}\) is generated, as a group, by the nonzero prime ideals \(\mathfrak p\) of the ring of integers \(\mathcal O_K\) that do not divide the finite part of \(\mathfrak m\).

theorem closure_coprimePrimeUnits_eq_top :
    Subgroup.closure m.coprimePrimeUnits = ⊤

Uses 9 · Used by 1

Statement usesFractional ideals coprime to a modulus · Prime coprime units

Proof usesFractional ideal with prescribed prime exponents · Reconstructing a fractional ideal from its prime exponents · Prime exponents of an invertible fractional ideal · Primes dividing a modulus · Membership in the prime coprime units · The prime as a coprime fractional ideal · A prime as an invertible fractional ideal

Used byThe free group on the coprime primes surjects onto the coprime ideals

DefinitionThe free group on the coprime primes maps to the coprime ideals#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), let \(P\) be the set of nonzero prime ideals of the ring of integers \(\mathcal O_K\) that do not divide the finite part of \(\mathfrak m\), and let \(I_K^{\mathfrak m}\) be the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\). This is the group homomorphism \(F(P) \to I_K^{\mathfrak m}\) from the free group on \(P\) that sends each generator \(\mathfrak p\) to \(\mathfrak p\), viewed as an element of \(I_K^{\mathfrak m}\).

noncomputable def freeGroupToCoprime :
    FreeGroup m.CoprimePrimes →* m.coprimeFractionalIdeals :=
  FreeGroup.lift (fun p => m.primeCoprimeUnit p.val p.property)

Uses 4 · Used by 9

Statement usesPrimes coprime to a modulus · Fractional ideals coprime to a modulus · Primes dividing a modulus · The prime as a coprime fractional ideal

Used byArtin map · The Artin map factors the free-group Frobenius map · The Artin map at a prime · The kernel of the free-group map is the commutator subgroup · The kernel of the free-group map lies in the commutator subgroup · Kernel containment for the free-group Frobenius map · The free-group map on generators · The free group on the coprime primes surjects onto the coprime ideals · The Artin map commutes with restriction

TheoremThe free-group map on generators#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), let \(P\) be the set of nonzero prime ideals of the ring of integers \(\mathcal O_K\) that do not divide the finite part of \(\mathfrak m\), and let \(I_K^{\mathfrak m}\) be the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\). For every \(\mathfrak p \in P\), the homomorphism \(F(P) \to I_K^{\mathfrak m}\) from the free group on \(P\) sends the generator attached to \(\mathfrak p\) to \(\mathfrak p\), viewed as an element of \(I_K^{\mathfrak m}\).

@[simp]
theorem freeGroupToCoprime_of (p : m.CoprimePrimes) :
    m.freeGroupToCoprime (FreeGroup.of p) = m.primeCoprimeUnit p.val p.property

Uses 5 · Used by 3

Statement usesPrimes coprime to a modulus · Fractional ideals coprime to a modulus · Primes dividing a modulus · The free group on the coprime primes maps to the coprime ideals · The prime as a coprime fractional ideal

Used byThe Artin map at a prime · The kernel of the free-group map lies in the commutator subgroup · The Artin map commutes with restriction

TheoremThe free group on the coprime primes surjects onto the coprime ideals#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), let \(P\) be the set of nonzero prime ideals of the ring of integers \(\mathcal O_K\) that do not divide the finite part of \(\mathfrak m\), and let \(I_K^{\mathfrak m}\) be the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\). The homomorphism \(F(P) \to I_K^{\mathfrak m}\) from the free group on \(P\) sending each generator \(\mathfrak p\) to \(\mathfrak p\) is surjective.

theorem freeGroupToCoprime_surjective :
    Function.Surjective m.freeGroupToCoprime

Uses 8 · Used by 3

Statement usesPrimes coprime to a modulus · Fractional ideals coprime to a modulus · The free group on the coprime primes maps to the coprime ideals

Proof usesThe coprime primes generate the coprime ideals · Prime coprime units · The prime coprime units are the image of the coprime primes · Primes dividing a modulus · The prime as a coprime fractional ideal

Used byArtin map · The Artin map factors the free-group Frobenius map · The Artin map commutes with restriction

TheoremThe kernel of the free-group map lies in the commutator subgroup#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), let \(P\) be the set of nonzero prime ideals of the ring of integers \(\mathcal O_K\) that do not divide the finite part of \(\mathfrak m\), and let \(I_K^{\mathfrak m}\) be the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\). The kernel of the homomorphism \(F(P) \to I_K^{\mathfrak m}\) from the free group on \(P\) sending each generator \(\mathfrak p\) to \(\mathfrak p\) is contained in the commutator subgroup \([F(P), F(P)]\).

theorem freeGroupToCoprime_ker_le_commutator :
    MonoidHom.ker m.freeGroupToCoprime ≤
      commutator (FreeGroup m.CoprimePrimes)

Sources

• direct native counterpart of ATLAS freeGroupToCoprime_ker_le_commutator (source lines 429--487). The prime basis-vector computation at source lines 416--427 is replaced by FractionalIdeal.factorizationMulEquiv_primeUnitFractionalIdeal. The proof builds the ATLAS retraction to the abelianization through FractionalIdeal.factorizationMulEquiv, Finsupp.comapDomain.addMonoidHom, Finsupp.toFreeAbelianGroup, and Abelianization.of; the retraction itself stays private to this proof.

Uses 9 · Used by 2

Statement usesPrimes coprime to a modulus · Fractional ideals coprime to a modulus · The free group on the coprime primes maps to the coprime ideals

Proof usesPrime factorization isomorphism for fractional ideals · Factorization of a prime of a number field · Primes dividing a modulus · The free-group map on generators · The prime as a coprime fractional ideal · A prime as an invertible fractional ideal

Used byThe kernel of the free-group map is the commutator subgroup · Kernel containment for the free-group Frobenius map

TheoremThe kernel of the free-group map is the commutator subgroup#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), let \(P\) be the set of nonzero prime ideals of the ring of integers \(\mathcal O_K\) that do not divide the finite part of \(\mathfrak m\), and let \(I_K^{\mathfrak m}\) be the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\). The kernel of the homomorphism \(F(P) \to I_K^{\mathfrak m}\) from the free group on \(P\) sending each generator \(\mathfrak p\) to \(\mathfrak p\) equals the commutator subgroup \([F(P), F(P)]\).

The commutator subgroup lies in the kernel because \(I_K^{\mathfrak m}\) is abelian.

@[simp]
theorem freeGroupToCoprime_ker :
    MonoidHom.ker m.freeGroupToCoprime =
      commutator (FreeGroup m.CoprimePrimes)

Uses 4

Statement usesPrimes coprime to a modulus · Fractional ideals coprime to a modulus · The free group on the coprime primes maps to the coprime ideals

Proof usesThe kernel of the free-group map lies in the commutator subgroup

DefinitionExtensions unramified outside a modulus#✓fully proved

Let \(m\) be a modulus of a number field \(K\). An extension of number fields \(L / K\) is unramified outside \(m\) when every finite prime \(\mathfrak p\) of \(K\) not dividing the finite part of \(m\) is unramified in \(\mathcal O_L\), that is, every prime of \(\mathcal O_L\) lying over \(\mathfrak p\) is unramified over \(\mathcal O_K\).

def IsUnramifiedOutside (L : Type*) [Field L] [NumberField L] [Algebra K L] :
    Prop :=
  ∀ v : IsDedekindDomain.HeightOneSpectrum (𝓞 K), ¬ m.finiteSupported v →
    Algebra.IsUnramifiedIn (𝓞 L) v.asIdeal

Uses 1 · Used by 12

Statement usesPrimes dividing a modulus

Used byArtin map · The Artin map factors the free-group Frobenius map · The Artin map at a prime · Unramified outside a modulus implies unramified at coprime primes · Kernel containment for the free-group Frobenius map · Frobenius homomorphism on the free group of coprime primes · The Frobenius homomorphism on generators · Chosen Frobenius element at a coprime prime · The chosen Frobenius is an arithmetic Frobenius at an unramified prime · Restriction of the Artin map at a prime · The Artin map commutes with restriction · Restriction of Frobenius elements in a tower

TheoremUnramified outside a modulus implies unramified at coprime primes#✓fully proved

Let \(m\) be a modulus of a number field \(K\) and let \(L / K\) be an extension of number fields that is unramified outside \(m\). Then every finite prime \(\mathfrak p\) of \(K\) not dividing the finite part of \(m\) is unramified in \(\mathcal O_L\).

theorem IsUnramifiedOutside.at_coprimePrime {L : Type*} [Field L] [NumberField L]
    [Algebra K L] (h : m.IsUnramifiedOutside L) (p : m.CoprimePrimes) :
    Algebra.IsUnramifiedIn (𝓞 L) p.val.asIdeal

Uses 3

Statement usesPrimes coprime to a modulus · Extensions unramified outside a modulus · Primes dividing a modulus

DefinitionChosen Frobenius element at a coprime prime#✓fully proved

Let \(m\) be a modulus of a number field \(K\), let \(L / K\) be a Galois extension of number fields that is unramified outside \(m\), and let \(\mathfrak p\) be a finite prime of \(K\) not dividing the finite part of \(m\). Fix a prime \(\mathfrak P\) of \(\mathcal O_L\) lying over \(\mathfrak p\). The chosen Frobenius element at \(\mathfrak p\) is a fixed element \(\sigma \in \mathrm{Gal}(L/K)\) that is an arithmetic Frobenius at \(\mathfrak P\), that is, \(\sigma(x) \equiv x^q \pmod{\mathfrak P}\) for all \(x \in \mathcal O_L\), where \(q\) is the number of elements of \(\mathcal O_K / \mathfrak p\).

The value may depend on the choice of \(\mathfrak P\).

noncomputable def frobeniusAtCoprimePrime (_h : m.IsUnramifiedOutside L)
    (p : m.CoprimePrimes) : (L ≃ₐ[K] L) :=
  haveI := (m.chosenPrime (L := L) p).property.1
  haveI := m.chosenFinite (L := L) p
  arithFrobAt (𝓞 K) (L ≃ₐ[K] L) (m.chosenPrime (L := L) p).1

Uses 3 · Used by 6

Statement usesPrimes coprime to a modulus · Extensions unramified outside a modulus · Primes dividing a modulus

Used byThe Artin map at a prime · Frobenius homomorphism on the free group of coprime primes · The Frobenius homomorphism on generators · The chosen Frobenius is an arithmetic Frobenius at an unramified prime · Restriction of the Artin map at a prime · Restriction of Frobenius elements in a tower

TheoremThe chosen Frobenius is an arithmetic Frobenius at an unramified prime#✓fully proved

Let \(m\) be a modulus of a number field \(K\), let \(L / K\) be a Galois extension of number fields that is unramified outside \(m\), and let \(\mathfrak p\) be a finite prime of \(K\) not dividing the finite part of \(m\), with chosen Frobenius element \(\sigma \in \mathrm{Gal}(L/K)\). Then there is a prime \(\mathfrak P\) of \(\mathcal O_L\) lying over \(\mathfrak p\) such that \(\mathcal O_L / \mathfrak P\) is finite, \(\mathfrak P\) is unramified over \(\mathcal O_K\), and \(\sigma(x) \equiv x^q \pmod{\mathfrak P}\) for all \(x \in \mathcal O_L\), where \(q\) is the number of elements of \(\mathcal O_K / \mathfrak p\).

theorem frobeniusAtCoprimePrime_spec (h : m.IsUnramifiedOutside L)
    (p : m.CoprimePrimes) :
    ∃ Q : Ideal.primesOver p.val.asIdeal (𝓞 L),
      Finite (𝓞 L ⧸ Q.1) ∧ Q.1.LiesOver p.val.asIdeal ∧
        Algebra.IsUnramifiedAt (𝓞 K) Q.1 ∧
        IsArithFrobAt (𝓞 K) (m.frobeniusAtCoprimePrime (L := L) h p) Q.1

Uses 4 · Used by 1

Statement usesPrimes coprime to a modulus · Extensions unramified outside a modulus · Primes dividing a modulus · Chosen Frobenius element at a coprime prime

Used byRestriction of Frobenius elements in a tower

DefinitionFrobenius homomorphism on the free group of coprime primes#✓fully proved

Let \(m\) be a modulus of a number field \(K\) and let \(L / K\) be a Galois extension of number fields that is unramified outside \(m\). The Frobenius homomorphism is the group homomorphism from the free group on the finite primes of \(K\) not dividing the finite part of \(m\) to \(\mathrm{Gal}(L/K)\) that sends each such prime \(\mathfrak p\) to the chosen Frobenius element at \(\mathfrak p\).

noncomputable def freeGroupToGal (h : m.IsUnramifiedOutside L) :
    FreeGroup m.CoprimePrimes →* (L ≃ₐ[K] L) :=
  FreeGroup.lift (fun p => m.frobeniusAtCoprimePrime (L := L) h p)

Uses 3 · Used by 5

Statement usesPrimes coprime to a modulus · Extensions unramified outside a modulus · Chosen Frobenius element at a coprime prime

Used byArtin map · The Artin map factors the free-group Frobenius map · The Artin map at a prime · Kernel containment for the free-group Frobenius map · The Frobenius homomorphism on generators

TheoremThe Frobenius homomorphism on generators#✓fully proved

Let \(m\) be a modulus of a number field \(K\) and let \(L / K\) be a Galois extension of number fields that is unramified outside \(m\). For every finite prime \(\mathfrak p\) of \(K\) not dividing the finite part of \(m\), the Frobenius homomorphism from the free group on these primes to \(\mathrm{Gal}(L/K)\) sends the generator \(\mathfrak p\) to the chosen Frobenius element at \(\mathfrak p\).

@[simp]
theorem freeGroupToGal_of (h : m.IsUnramifiedOutside L) (p : m.CoprimePrimes) :
    m.freeGroupToGal (L := L) h (FreeGroup.of p) =
      m.frobeniusAtCoprimePrime (L := L) h p

Uses 4 · Used by 1

Statement usesPrimes coprime to a modulus · Extensions unramified outside a modulus · Frobenius homomorphism on the free group of coprime primes · Chosen Frobenius element at a coprime prime

Used byThe Artin map at a prime

TheoremKernel containment for the free-group Frobenius map#✓fully proved

Let \(L/K\) be an abelian Galois extension of number fields and \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\), such that every prime of \(\mathcal O_K\) not dividing \(\mathfrak m_0\) is unramified in \(L\). Let \(F\) be the free group on the primes \(\mathfrak p\) of \(\mathcal O_K\) not dividing \(\mathfrak m_0\). Then the kernel of the homomorphism from \(F\) to the group of fractional ideals of \(K\) coprime to \(\mathfrak m_0\) sending each generator \(\mathfrak p\) to the ideal \(\mathfrak p\) is contained in the kernel of the homomorphism \(F \to \mathrm{Gal}(L/K)\) sending each generator \(\mathfrak p\) to the arithmetic Frobenius at a chosen prime of \(\mathcal O_L\) above \(\mathfrak p\).

The first kernel lies in the commutator subgroup of \(F\), which the second map kills because \(\mathrm{Gal}(L/K)\) is abelian.

theorem freeGroupToCoprime_ker_le_freeGroupToGal_ker (h : m.IsUnramifiedOutside L) :
    MonoidHom.ker m.freeGroupToCoprime ≤
      MonoidHom.ker (m.freeGroupToGal (L := L) h)

Uses 6 · Used by 2

Statement usesPrimes coprime to a modulus · Extensions unramified outside a modulus · Fractional ideals coprime to a modulus · The free group on the coprime primes maps to the coprime ideals · Frobenius homomorphism on the free group of coprime primes

Proof usesThe kernel of the free-group map lies in the commutator subgroup

Used byArtin map · The Artin map factors the free-group Frobenius map

DefinitionArtin map#✓fully proved

Let \(L/K\) be an abelian Galois extension of number fields and \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\), such that every prime of \(\mathcal O_K\) not dividing \(\mathfrak m_0\) is unramified in \(L\). Let \(I^{\mathfrak m}\) be the group of fractional ideals of \(K\) coprime to \(\mathfrak m_0\) and \(F\) the free group on the primes \(\mathfrak p\) of \(\mathcal O_K\) not dividing \(\mathfrak m_0\). The homomorphism \(F \to I^{\mathfrak m}\) sending each generator \(\mathfrak p\) to the ideal \(\mathfrak p\) is surjective, and its kernel lies in the kernel of the homomorphism \(F \to \mathrm{Gal}(L/K)\) sending each generator \(\mathfrak p\) to the arithmetic Frobenius at a chosen prime of \(\mathcal O_L\) above \(\mathfrak p\). The Artin map is the homomorphism \(I^{\mathfrak m} \to \mathrm{Gal}(L/K)\) induced by the second map through the first.

noncomputable def artinMap (h : m.IsUnramifiedOutside L) :
    m.coprimeFractionalIdeals →* (L ≃ₐ[K] L) :=
  (m.freeGroupToCoprime.liftOfSurjective m.freeGroupToCoprime_surjective)
    ⟨m.freeGroupToGal (L := L) h,
      m.freeGroupToCoprime_ker_le_freeGroupToGal_ker (L := L) h⟩

Uses 7 · Used by 4

Statement usesPrimes coprime to a modulus · Extensions unramified outside a modulus · Fractional ideals coprime to a modulus · The free group on the coprime primes maps to the coprime ideals · Kernel containment for the free-group Frobenius map · The free group on the coprime primes surjects onto the coprime ideals · Frobenius homomorphism on the free group of coprime primes

Used byThe Artin map factors the free-group Frobenius map · The Artin map at a prime · Restriction of the Artin map at a prime · The Artin map commutes with restriction

TheoremThe Artin map factors the free-group Frobenius map#✓fully proved

Let \(L/K\) be an abelian Galois extension of number fields and \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\), such that every prime of \(\mathcal O_K\) not dividing \(\mathfrak m_0\) is unramified in \(L\). Let \(F\) be the free group on the primes \(\mathfrak p\) of \(\mathcal O_K\) not dividing \(\mathfrak m_0\), and let \(I^{\mathfrak m}\) be the group of fractional ideals of \(K\) coprime to \(\mathfrak m_0\). Then the Artin map \(I^{\mathfrak m} \to \mathrm{Gal}(L/K)\) composed with the homomorphism \(F \to I^{\mathfrak m}\) sending each generator \(\mathfrak p\) to the ideal \(\mathfrak p\) equals the homomorphism \(F \to \mathrm{Gal}(L/K)\) sending each generator \(\mathfrak p\) to the arithmetic Frobenius at a chosen prime of \(\mathcal O_L\) above \(\mathfrak p\).

@[simp]
theorem artinMap_comp_freeGroupToCoprime (h : m.IsUnramifiedOutside L) :
    (m.artinMap (L := L) h).comp m.freeGroupToCoprime =
      m.freeGroupToGal (L := L) h

Uses 8 · Used by 1

Statement usesPrimes coprime to a modulus · Extensions unramified outside a modulus · Artin map · Fractional ideals coprime to a modulus · The free group on the coprime primes maps to the coprime ideals · Frobenius homomorphism on the free group of coprime primes

Proof usesKernel containment for the free-group Frobenius map · The free group on the coprime primes surjects onto the coprime ideals

Used byThe Artin map at a prime

TheoremThe Artin map at a prime#✓fully proved

Let \(L/K\) be an abelian Galois extension of number fields and \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\), such that every prime of \(\mathcal O_K\) not dividing \(\mathfrak m_0\) is unramified in \(L\). For every prime \(\mathfrak p\) of \(\mathcal O_K\) not dividing \(\mathfrak m_0\), the Artin map sends \(\mathfrak p\), viewed as a fractional ideal coprime to \(\mathfrak m_0\), to the arithmetic Frobenius in \(\mathrm{Gal}(L/K)\) at a chosen prime of \(\mathcal O_L\) above \(\mathfrak p\).

@[simp]
theorem artinMap_primeCoprimeUnit (h : m.IsUnramifiedOutside L)
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) (hvm : ¬ m.finiteSupported v) :
    m.artinMap (L := L) h (m.primeCoprimeUnit v hvm) =
      m.frobeniusAtCoprimePrime (L := L) h ⟨v, hvm⟩

Uses 12 · Used by 1

Statement usesExtensions unramified outside a modulus · Artin map · Fractional ideals coprime to a modulus · Primes dividing a modulus · Chosen Frobenius element at a coprime prime · The prime as a coprime fractional ideal

Proof usesPrimes coprime to a modulus · The Artin map factors the free-group Frobenius map · The free group on the coprime primes maps to the coprime ideals · The free-group map on generators · Frobenius homomorphism on the free group of coprime primes · The Frobenius homomorphism on generators

Used byRestriction of the Artin map at a prime

TheoremRestriction of Frobenius elements in a tower#✓fully proved

Let \(K \subseteq L \subseteq M\) be a tower of number fields with \(L/K\) abelian Galois and \(M/K\) Galois, and let \(\mathfrak m\) be a modulus of \(K\) such that \(L\) and \(M\) are both unramified outside \(\mathfrak m\). For every finite prime \(\mathfrak p\) of \(K\) not dividing the finite part of \(\mathfrak m\), the restriction to \(L\) of the chosen Frobenius element of \(\mathfrak p\) in \(\mathrm{Gal}(M/K)\) equals the chosen Frobenius element of \(\mathfrak p\) in \(\mathrm{Gal}(L/K)\).

The abelianity of \(L/K\) is used only to make conjugation of the Frobenius element in \(\mathrm{Gal}(L/K)\) trivial.

theorem restrictNormalHom_frobeniusAtCoprimePrime
    (m : Modulus K) (hL : m.IsUnramifiedOutside L)
    (hM : m.IsUnramifiedOutside M) (p : m.CoprimePrimes) :
    AlgEquiv.restrictNormalHom L
        (m.frobeniusAtCoprimePrime (L := M) hM p) =
      m.frobeniusAtCoprimePrime (L := L) hL p

Uses 6 · Used by 1

Statement usesPrimes coprime to a modulus · Extensions unramified outside a modulus · Chosen Frobenius element at a coprime prime

Proof usesPrimes dividing a modulus · The chosen Frobenius is an arithmetic Frobenius at an unramified prime · Restricting a Frobenius element to an intermediate field

Used byRestriction of the Artin map at a prime

TheoremRestriction of the Artin map at a prime#✓fully proved

Let \(K \subseteq L \subseteq M\) be a tower of number fields with \(L/K\) and \(M/K\) abelian Galois, and let \(\mathfrak m\) be a modulus of \(K\) with finite part \(\mathfrak m_0\) such that every prime of \(\mathcal O_K\) not dividing \(\mathfrak m_0\) is unramified in \(L\) and in \(M\). For every prime \(\mathfrak p\) of \(\mathcal O_K\) not dividing \(\mathfrak m_0\), restricting to \(L\) the image of \(\mathfrak p\) under the Artin map of \(M/K\) gives the image of \(\mathfrak p\) under the Artin map of \(L/K\).

theorem restrictNormalHom_artinMap_primeCoprimeUnit
    (m : Modulus K) (hL : m.IsUnramifiedOutside L)
    (hM : m.IsUnramifiedOutside M)
    (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))
    (hvm : ¬ m.finiteSupported v) :
    AlgEquiv.restrictNormalHom L
        (m.artinMap (L := M) hM (m.primeCoprimeUnit v hvm)) =
      m.artinMap (L := L) hL (m.primeCoprimeUnit v hvm)

Uses 8 · Used by 1

Statement usesExtensions unramified outside a modulus · Artin map · Fractional ideals coprime to a modulus · Primes dividing a modulus · The prime as a coprime fractional ideal

Proof usesThe Artin map at a prime · Chosen Frobenius element at a coprime prime · Restriction of Frobenius elements in a tower

Used byThe Artin map commutes with restriction

TheoremThe Artin map commutes with restriction#✓fully proved

Let \(K \subseteq L \subseteq M\) be a tower of number fields with \(L/K\) and \(M/K\) abelian Galois, and let \(\mathfrak m\) be a modulus of \(K\) with finite part \(\mathfrak m_0\) such that every prime of \(\mathcal O_K\) not dividing \(\mathfrak m_0\) is unramified in \(L\) and in \(M\). Then the Artin map of \(M/K\) followed by restriction \(\mathrm{Gal}(M/K) \to \mathrm{Gal}(L/K)\) equals the Artin map of \(L/K\), as homomorphisms from the group of fractional ideals of \(K\) coprime to \(\mathfrak m_0\) to \(\mathrm{Gal}(L/K)\).

theorem restrictNormalHom_comp_artinMap
    (m : Modulus K) (hL : m.IsUnramifiedOutside L)
    (hM : m.IsUnramifiedOutside M) :
    (AlgEquiv.restrictNormalHom L).comp (m.artinMap (L := M) hM) =
      m.artinMap (L := L) hL

Uses 10

Statement usesExtensions unramified outside a modulus · Artin map · Fractional ideals coprime to a modulus

Proof usesPrimes coprime to a modulus · Primes dividing a modulus · The free group on the coprime primes maps to the coprime ideals · The free-group map on generators · The free group on the coprime primes surjects onto the coprime ideals · The prime as a coprime fractional ideal · Restriction of the Artin map at a prime

27 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.