Local Galois groups of p-adic fields

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe generator rank of a local absolute Galois group (NSW (7.4.1))#

For a finite extension K of ℚ_p, the absolute Galois group G_K needs exactly [K : ℚ_p] + 2 topological generators. A witness of topological finite generation is TauCeti.isTopologicallyFinitelyGenerated_fieldAbsoluteGaloisGroup.

TauCeti.topologicalGeneratorRankNat_absoluteGaloisGroup (p : ℕ) [Fact (Nat.Prime p)] (K : Type)
  [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K]
  [Module.Finite ℚ_[p] K] [ValuativeExtension ℚ_[p] K]
  (hG : TauCeti.IsTopologicallyFinitelyGenerated (Field.absoluteGaloisGroup K)) :
  TauCeti.topologicalGeneratorRankNat (Field.absoluteGaloisGroup K) hG = Module.finrank ℚ_[p] K + 2

Lean

Formalized in Tau Ceti as TauCeti.topologicalGeneratorRankNat_absoluteGaloisGroup.

Sources

• Tau Ceti documentation: TauCeti.topologicalGeneratorRankNat_absoluteGaloisGroup
• Source of TauCeti.topologicalGeneratorRankNat_absoluteGaloisGroup in TauCeti/NumberTheory/LocalField/Generation/AbsoluteGaloisGroup.lean
• Tau Ceti roadmap status: Local Galois groups of p-adic fields

LeanTauCeti.topologicalGeneratorRankNat_absoluteGaloisGroup

Uses 7

Proof usesBurnside's basis theorem, cardinal form · The finite level of the generator theorem (NSW, proof of (7.4.1)) · The Kummer isomorphism · The Schreier bound · Shapiro's lemma in degree one · TauCeti.algebraicExtensionNormedField · The wild inertia subgroup

TheoremDemushkin's theorem#

the maximal pro-p quotient G_K(p) of the absolute Galois group of a nonarchimedean local field K containing a primitive pth root of unity is a Demushkin group.

TauCeti.isDemushkin_absoluteGaloisGroupProP_of_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  (hmu : ∃ ζ, IsPrimitiveRoot ζ p) : TauCeti.IsDemushkin p (TauCeti.absoluteGaloisGroupProP p K)

Lean

Formalized in Tau Ceti as TauCeti.isDemushkin_absoluteGaloisGroupProP_of_mu.

Sources

• Tau Ceti documentation: TauCeti.isDemushkin_absoluteGaloisGroupProP_of_mu
• Source of TauCeti.isDemushkin_absoluteGaloisGroupProP_of_mu in TauCeti/NumberTheory/LocalField/ProP/Demushkin.lean
• Tau Ceti roadmap status: Local Galois groups of p-adic fields

LeanTauCeti.isDemushkin_absoluteGaloisGroupProP_of_mu

Uses 5 · Used by 2

Statement usesThe Demushkin predicate

Proof usesThe Kummer isomorphism · The local invariant · Shapiro's lemma in degree one · TauCeti.algebraicExtensionNormedField

Used byThe marked presentation of G_{ℚ₂}(2) · The marked presentation of G_{ℚ₂(√-2)}(2)

TheoremThe marked presentation of G_{ℚ₂}(2)#

There is an isomorphism e : G_{ℚ₂}(2) ≃ D₀ = ⟨A, S, Y ∣ A²S⁴(S,Y)⟩ along which the standard orientation of D₀ pulls back to the cyclotomic orientation of G_{ℚ₂}(2), and the cyclotomic orientation is surjective.

TauCeti.absoluteGaloisGroupProP_two_ratPadic_marked :
  ∃ e,
    TauCeti.standardD0Orientation.comp ↑e =
        TauCeti.cyclotomicOrientation 2 ℚ_[2] TauCeti.ratPadicTwo_hasPrimitiveRoot ∧
      Function.Surjective
        ⇑(TauCeti.cyclotomicOrientation 2 ℚ_[2] TauCeti.ratPadicTwo_hasPrimitiveRoot)

Lean

Formalized in Tau Ceti as TauCeti.absoluteGaloisGroupProP_two_ratPadic_marked.

Sources

• Tau Ceti documentation: TauCeti.absoluteGaloisGroupProP_two_ratPadic_marked
• Source of TauCeti.absoluteGaloisGroupProP_two_ratPadic_marked in TauCeti/NumberTheory/LocalField/ProP/RatPadic.lean
• Tau Ceti roadmap status: Local Galois groups of p-adic fields

LeanTauCeti.absoluteGaloisGroupProP_two_ratPadic_marked

Uses 12

Proof usesThe abelianization structure theorem for one-relator pro-p groups · Burnside's basis theorem, cardinal form · The Demushkin predicate · Demushkin's theorem · The first isomorphism theorem for a surjective strict homomorphism of topological groups · The Kummer isomorphism · Labute's criterion · Labute's Theorem 4: a Demushkin group has exactly one continuous character with the prescription property · The relative successive-approximation theorem · Shapiro's lemma in degree one · The successive-approximation theorem with tails · TauCeti.algebraicExtensionNormedField

TheoremThe marked presentation of G_{ℚ₂(√-2)}(2)#

The maximal pro-2 Galois group of ℚ₂(√-2) is isomorphic to ⟨x₁, x₂, x₃, x₄ ∣ x₁⁶ (x₁, x₂) x₃⁸ (x₃, x₄)⟩, the even dyadic Demushkin group with α = 4 and f = 3, and under this isomorphism the cyclotomic orientation satisfies χ(x₂) · (1 + 4) = -1 and χ(x₄) · (1 - 8) = 1 and is trivial on x₁ and x₃.

This is absoluteGaloisGroupProP_two_marked_of_degree_even_principal at N = 2, with k = 2 read off the cyclotomic image closure⟨-1 + 2²⟩ (range_localCyclotomicCharacter_ratPadicSqrtNegTwo).

TauCeti.absoluteGaloisGroupProP_two_ratPadicSqrtNegTwo_marked :
  ∃ e,
    ↑((TauCeti.cyclotomicOrientation 2 TauCeti.RatPadicSqrtNegTwo
                TauCeti.ratPadicSqrtNegTwo_hasPrimitiveRoot)
              (e.symm
                (TauCeti.presentedProPGen 2 4
                  {TauCeti.demushkinWordTwoEven 4 3 4 (TauCeti.freeProPGen 2 4)} 1))) *
          (1 + 4) =
        -1 ∧
      ↑((TauCeti.cyclotomicOrientation 2 TauCeti.RatPadicSqrtNegTwo
                  TauCeti.ratPadicSqrtNegTwo_hasPrimitiveRoot)
                (e.symm
                  (TauCeti.presentedProPGen 2 4
                    {TauCeti.demushkinWordTwoEven 4 3 4 (TauCeti.freeProPGen 2 4)} 3))) *
            (1 - 8) =
          1 ∧
        (TauCeti.cyclotomicOrientation 2 TauCeti.RatPadicSqrtNegTwo
                TauCeti.ratPadicSqrtNegTwo_hasPrimitiveRoot)
              (e.symm
                (TauCeti.presentedProPGen 2 4
                  {TauCeti.demushkinWordTwoEven 4 3 4 (TauCeti.freeProPGen 2 4)} 0)) =
            1 ∧
          (TauCeti.cyclotomicOrientation 2 TauCeti.RatPadicSqrtNegTwo
                TauCeti.ratPadicSqrtNegTwo_hasPrimitiveRoot)
              (e.symm
                (TauCeti.presentedProPGen 2 4
                  {TauCeti.demushkinWordTwoEven 4 3 4 (TauCeti.freeProPGen 2 4)} 2)) =
            1

Lean

Formalized in Tau Ceti as TauCeti.absoluteGaloisGroupProP_two_ratPadicSqrtNegTwo_marked.

Sources

• Tau Ceti documentation: TauCeti.absoluteGaloisGroupProP_two_ratPadicSqrtNegTwo_marked
• Source of TauCeti.absoluteGaloisGroupProP_two_ratPadicSqrtNegTwo_marked in TauCeti/NumberTheory/LocalField/ProP/SqrtNegTwo.lean
• Tau Ceti roadmap status: Local Galois groups of p-adic fields

LeanTauCeti.absoluteGaloisGroupProP_two_ratPadicSqrtNegTwo_marked

Uses 13

Proof usesBurnside's basis theorem, cardinal form · Burnside's criterion modulo λ_1 · The constrained successive-approximation theorem · Dedekind's modular law · The Demushkin predicate · Demushkin's theorem · The first isomorphism theorem for a surjective strict homomorphism of topological groups · The Kummer isomorphism · Labute's classification of the closed subgroups of ℤ_2ˣ · Labute's criterion · Labute's Theorem 4: a Demushkin group has exactly one continuous character with the prescription property · Shapiro's lemma in degree one · TauCeti.algebraicExtensionNormedField

TheoremFunctoriality of the marked presentation when q(K) ≠ 2#

Let e : K ≃+* K' be an isomorphism of fields, and let m be a marked presentation of G_K(p) with the relator word and the values that TauCeti.absoluteGaloisGroupProP_marked_of_q_ne_two records for K. Then (absoluteGaloisGroupProPCongr e).trans m presents G_{K'}(p) by the same relator word and takes the same values of the cyclotomic orientation on the generators.

Only the transport of the recorded values is claimed, and it uses no property of e beyond being an isomorphism of fields: it is the naturality of the cyclotomic orientation along the induced isomorphism of the absolute Galois groups (TauCeti.cyclotomicOrientation_trans_absoluteGaloisGroupProPCongr). For the transported presentation to be the marked presentation of G_{K'}(p) in the sense of TauCeti.absoluteGaloisGroupProP_marked_of_q_ne_two, the target must have the same degree over ℚ_p and the same number of p-power roots of unity as the source; an isomorphism of local fields over ℚ_p provides that (TauCeti.isQNeTwoCase_iff_of_algEquiv).

TauCeti.absoluteGaloisGroupProP_marked_of_q_ne_two_congr.{u_1, u_2} (p : ℕ) [Fact (Nat.Prime p)]
  {K : Type u_1} {K' : Type u_2} [Field K] [Algebra ℚ_[p] K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] [Field K'] (e : K ≃+* K') (hmu : ∃ ζ, IsPrimitiveRoot ζ p)
  (hmu' : ∃ ζ, IsPrimitiveRoot ζ p)
  (m :
    TauCeti.absoluteGaloisGroupProP p K ≃ₜ*
      TauCeti.presentedProP p (Fin (Module.finrank ℚ_[p] K + 2))
        {TauCeti.demushkinWordNeTwo (TauCeti.localRootOfUnityOrder p K ⋯)
            (Module.finrank ℚ_[p] K + 2) (TauCeti.freeProPGen p (Module.finrank ℚ_[p] K + 2))})
  (hm₁ :
    ↑((TauCeti.cyclotomicOrientation p K hmu)
            (m.symm
              (TauCeti.presentedProPGen p (Module.finrank ℚ_[p] K + 2)
                {TauCeti.demushkinWordNeTwo (TauCeti.localRootOfUnityOrder p K ⋯)
                    (Module.finrank ℚ_[p] K + 2)
                    (TauCeti.freeProPGen p (Module.finrank ℚ_[p] K + 2))}
                1))) *
        (1 - ↑(TauCeti.localRootOfUnityOrder p K ⋯)) =
      1)
  (hm₂ :
    ∀ (i : ℕ),
      i ≠ 1 →
        i < Module.finrank ℚ_[p] K + 2 →
          (TauCeti.cyclotomicOrientation p K hmu)
              (m.symm
                (TauCeti.presentedProPGen p (Module.finrank ℚ_[p] K + 2)
                  {TauCeti.demushkinWordNeTwo (TauCeti.localRootOfUnityOrder p K ⋯)
                      (Module.finrank ℚ_[p] K + 2)
                      (TauCeti.freeProPGen p (Module.finrank ℚ_[p] K + 2))}
                  i)) =
            1) :
  ↑((TauCeti.cyclotomicOrientation p K' hmu')
            (((TauCeti.absoluteGaloisGroupProPCongr p K K' e).trans m).symm
              (TauCeti.presentedProPGen p (Module.finrank ℚ_[p] K + 2)
                {TauCeti.demushkinWordNeTwo (TauCeti.localRootOfUnityOrder p K ⋯)
                    (Module.finrank ℚ_[p] K + 2)
                    (TauCeti.freeProPGen p (Module.finrank ℚ_[p] K + 2))}
                1))) *
        (1 - ↑(TauCeti.localRootOfUnityOrder p K ⋯)) =
      1 ∧
    ∀ (i : ℕ),
      i ≠ 1 →
        i < Module.finrank ℚ_[p] K + 2 →
          (TauCeti.cyclotomicOrientation p K' hmu')
              (((TauCeti.absoluteGaloisGroupProPCongr p K K' e).trans m).symm
                (TauCeti.presentedProPGen p (Module.finrank ℚ_[p] K + 2)
                  {TauCeti.demushkinWordNeTwo (TauCeti.localRootOfUnityOrder p K ⋯)
                      (Module.finrank ℚ_[p] K + 2)
                      (TauCeti.freeProPGen p (Module.finrank ℚ_[p] K + 2))}
                  i)) =
            1

Lean

Formalized in Tau Ceti as TauCeti.absoluteGaloisGroupProP_marked_of_q_ne_two_congr.

Sources

• Tau Ceti documentation: TauCeti.absoluteGaloisGroupProP_marked_of_q_ne_two_congr
• Source of TauCeti.absoluteGaloisGroupProP_marked_of_q_ne_two_congr in TauCeti/NumberTheory/LocalField/ProP/Marked/Functoriality.lean
• Tau Ceti roadmap status: Local Galois groups of p-adic fields

LeanTauCeti.absoluteGaloisGroupProP_marked_of_q_ne_two_congr

TheoremFunctoriality of the marked presentation in odd degree#

Let e : K ≃+* K' be an isomorphism of fields, and let m be a marked presentation of G_K(2) with the relator word and the values that TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_odd records for K. Then (absoluteGaloisGroupProPCongr e).trans m presents G_{K'}(2) by the same relator word demushkinWordTwoOdd and takes the same values on the generators 0, 2 and the remaining ones.

Only the transport of the recorded values is claimed, and it uses no property of e beyond being an isomorphism of fields; the transport is the naturality of the cyclotomic orientation along the induced isomorphism of the absolute Galois groups (TauCeti.cyclotomicOrientation_trans_absoluteGaloisGroupProPCongr). For the transported presentation to be the marked presentation of G_{K'}(2) in the sense of TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_odd, the target must have the same odd degree over ℚ₂ as the source; an isomorphism of local fields over ℚ₂ provides that (TauCeti.isDyadicOddCase_iff_of_algEquiv).

TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_odd_congr.{u_1, u_2} {K : Type u_1}
  {K' : Type u_2} [Field K] [Algebra ℚ_[2] K] [Field K'] (e : K ≃+* K')
  (hmu : ∃ ζ, IsPrimitiveRoot ζ 2) (hmu' : ∃ ζ, IsPrimitiveRoot ζ 2)
  (m :
    TauCeti.absoluteGaloisGroupProP 2 K ≃ₜ*
      TauCeti.presentedProP 2 (Fin (Module.finrank ℚ_[2] K + 2))
        {TauCeti.demushkinWordTwoOdd 2 (Module.finrank ℚ_[2] K + 2)
            (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))})
  (hm₀ :
    (TauCeti.cyclotomicOrientation 2 K hmu)
        (m.symm
          (TauCeti.presentedProPGen 2 (Module.finrank ℚ_[2] K + 2)
            {TauCeti.demushkinWordTwoOdd 2 (Module.finrank ℚ_[2] K + 2)
                (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))}
            0)) =
      -1)
  (hm₂ :
    ↑((TauCeti.cyclotomicOrientation 2 K hmu)
            (m.symm
              (TauCeti.presentedProPGen 2 (Module.finrank ℚ_[2] K + 2)
                {TauCeti.demushkinWordTwoOdd 2 (Module.finrank ℚ_[2] K + 2)
                    (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))}
                2))) *
        (1 - 2 ^ 2) =
      1)
  (hm :
    ∀ (i : ℕ),
      i ≠ 0 →
        i ≠ 2 →
          i < Module.finrank ℚ_[2] K + 2 →
            (TauCeti.cyclotomicOrientation 2 K hmu)
                (m.symm
                  (TauCeti.presentedProPGen 2 (Module.finrank ℚ_[2] K + 2)
                    {TauCeti.demushkinWordTwoOdd 2 (Module.finrank ℚ_[2] K + 2)
                        (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))}
                    i)) =
              1) :
  (TauCeti.cyclotomicOrientation 2 K' hmu')
        (((TauCeti.absoluteGaloisGroupProPCongr 2 K K' e).trans m).symm
          (TauCeti.presentedProPGen 2 (Module.finrank ℚ_[2] K + 2)
            {TauCeti.demushkinWordTwoOdd 2 (Module.finrank ℚ_[2] K + 2)
                (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))}
            0)) =
      -1 ∧
    ↑((TauCeti.cyclotomicOrientation 2 K' hmu')
              (((TauCeti.absoluteGaloisGroupProPCongr 2 K K' e).trans m).symm
                (TauCeti.presentedProPGen 2 (Module.finrank ℚ_[2] K + 2)
                  {TauCeti.demushkinWordTwoOdd 2 (Module.finrank ℚ_[2] K + 2)
                      (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))}
                  2))) *
          (1 - 2 ^ 2) =
        1 ∧
      ∀ (i : ℕ),
        i ≠ 0 →
          i ≠ 2 →
            i < Module.finrank ℚ_[2] K + 2 →
              (TauCeti.cyclotomicOrientation 2 K' hmu')
                  (((TauCeti.absoluteGaloisGroupProPCongr 2 K K' e).trans m).symm
                    (TauCeti.presentedProPGen 2 (Module.finrank ℚ_[2] K + 2)
                      {TauCeti.demushkinWordTwoOdd 2 (Module.finrank ℚ_[2] K + 2)
                          (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))}
                      i)) =
                1

Lean

Formalized in Tau Ceti as TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_odd_congr.

Sources

• Tau Ceti documentation: TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_odd_congr
• Source of TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_odd_congr in TauCeti/NumberTheory/LocalField/ProP/Marked/Functoriality.lean
• Tau Ceti roadmap status: Local Galois groups of p-adic fields

LeanTauCeti.absoluteGaloisGroupProP_two_marked_of_degree_odd_congr

TheoremFunctoriality of the marked presentation in even degree#

The two even dyadic marked theorems TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_even_plusMinus and TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_even_principal present G_K(2) by the same word demushkinWordTwoEven a f (N + 2) on N + 2 generators and record the same values on the second and fourth marked generators, the value -(1 + a)⁻¹ and the value (1 - 2^f)⁻¹; they differ only in the hypotheses that select the parameters a and f. Hence the transport of their marking is a single statement. For e : K ≃+* K' an isomorphism of fields, the transported isomorphism (absoluteGaloisGroupProPCongr e).trans m of a marked presentation of G_K(2) of the even form presents G_{K'}(2) by the same relator word and takes the same values.

Only the transport of the recorded values is claimed, and it uses no property of e beyond being an isomorphism of fields; the transport is the naturality of the cyclotomic orientation along the induced isomorphism of the absolute Galois groups (TauCeti.cyclotomicOrientation_trans_absoluteGaloisGroupProPCongr). For the transported presentation to be the marked presentation of G_{K'}(2) in the sense of TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_even_plusMinus or TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_even_principal, the target must have the same even degree over ℚ₂ and the same cyclotomic image as the source; an isomorphism of local fields over ℚ₂ provides that (TauCeti.isDyadicEvenPlusMinusCase_iff_of_algEquiv and TauCeti.isDyadicEvenPrincipalCase_iff_of_algEquiv).

TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_even_congr.{u_1, u_2} {K : Type u_1}
  {K' : Type u_2} [Field K] [Algebra ℚ_[2] K] [Field K'] (e : K ≃+* K')
  (hmu : ∃ ζ, IsPrimitiveRoot ζ 2) (hmu' : ∃ ζ, IsPrimitiveRoot ζ 2) {a f : ℕ}
  (m :
    TauCeti.absoluteGaloisGroupProP 2 K ≃ₜ*
      TauCeti.presentedProP 2 (Fin (Module.finrank ℚ_[2] K + 2))
        {TauCeti.demushkinWordTwoEven a f (Module.finrank ℚ_[2] K + 2)
            (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))})
  (hm₁ :
    ↑((TauCeti.cyclotomicOrientation 2 K hmu)
            (m.symm
              (TauCeti.presentedProPGen 2 (Module.finrank ℚ_[2] K + 2)
                {TauCeti.demushkinWordTwoEven a f (Module.finrank ℚ_[2] K + 2)
                    (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))}
                1))) *
        (1 + ↑a) =
      -1)
  (hm₃ :
    ↑((TauCeti.cyclotomicOrientation 2 K hmu)
            (m.symm
              (TauCeti.presentedProPGen 2 (Module.finrank ℚ_[2] K + 2)
                {TauCeti.demushkinWordTwoEven a f (Module.finrank ℚ_[2] K + 2)
                    (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))}
                3))) *
        (1 - 2 ^ f) =
      1)
  (hm :
    ∀ (i : ℕ),
      i ≠ 1 →
        i ≠ 3 →
          i < Module.finrank ℚ_[2] K + 2 →
            (TauCeti.cyclotomicOrientation 2 K hmu)
                (m.symm
                  (TauCeti.presentedProPGen 2 (Module.finrank ℚ_[2] K + 2)
                    {TauCeti.demushkinWordTwoEven a f (Module.finrank ℚ_[2] K + 2)
                        (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))}
                    i)) =
              1) :
  ↑((TauCeti.cyclotomicOrientation 2 K' hmu')
            (((TauCeti.absoluteGaloisGroupProPCongr 2 K K' e).trans m).symm
              (TauCeti.presentedProPGen 2 (Module.finrank ℚ_[2] K + 2)
                {TauCeti.demushkinWordTwoEven a f (Module.finrank ℚ_[2] K + 2)
                    (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))}
                1))) *
        (1 + ↑a) =
      -1 ∧
    ↑((TauCeti.cyclotomicOrientation 2 K' hmu')
              (((TauCeti.absoluteGaloisGroupProPCongr 2 K K' e).trans m).symm
                (TauCeti.presentedProPGen 2 (Module.finrank ℚ_[2] K + 2)
                  {TauCeti.demushkinWordTwoEven a f (Module.finrank ℚ_[2] K + 2)
                      (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))}
                  3))) *
          (1 - 2 ^ f) =
        1 ∧
      ∀ (i : ℕ),
        i ≠ 1 →
          i ≠ 3 →
            i < Module.finrank ℚ_[2] K + 2 →
              (TauCeti.cyclotomicOrientation 2 K' hmu')
                  (((TauCeti.absoluteGaloisGroupProPCongr 2 K K' e).trans m).symm
                    (TauCeti.presentedProPGen 2 (Module.finrank ℚ_[2] K + 2)
                      {TauCeti.demushkinWordTwoEven a f (Module.finrank ℚ_[2] K + 2)
                          (TauCeti.freeProPGen 2 (Module.finrank ℚ_[2] K + 2))}
                      i)) =
                1

Lean

Formalized in Tau Ceti as TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_even_congr.

Sources

• Tau Ceti documentation: TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_even_congr
• Source of TauCeti.absoluteGaloisGroupProP_two_marked_of_degree_even_congr in TauCeti/NumberTheory/LocalField/ProP/Marked/Functoriality.lean
• Tau Ceti roadmap status: Local Galois groups of p-adic fields

LeanTauCeti.absoluteGaloisGroupProP_two_marked_of_degree_even_congr

TheoremThe image of the cyclotomic character is an invariant of the field#

An isomorphism of fields induces an isomorphism of absolute Galois groups, and the cyclotomic character of the target is the character of the source read through it (TauCeti.localCyclotomicCharacter_map); hence the two characters have the same image in ℤ_pˣ.

TauCeti.range_localCyclotomicCharacter_eq_of_ringEquiv.{u_1, u_2} (p : ℕ) [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] {K' : Type u_2} [Field K'] (e : K ≃+* K') :
  (TauCeti.localCyclotomicCharacter p K).range = (TauCeti.localCyclotomicCharacter p K').range

Lean

Formalized in Tau Ceti as TauCeti.range_localCyclotomicCharacter_eq_of_ringEquiv.

Sources

• Tau Ceti documentation: TauCeti.range_localCyclotomicCharacter_eq_of_ringEquiv
• Source of TauCeti.range_localCyclotomicCharacter_eq_of_ringEquiv in TauCeti/NumberTheory/LocalField/ProP/Marked/Functoriality.lean
• Tau Ceti roadmap status: Local Galois groups of p-adic fields

LeanTauCeti.range_localCyclotomicCharacter_eq_of_ringEquiv

TheoremThe cyclotomic normalization of the local Artin map of a finite extension of ℚ_p#

Let F/ℚ_p be finite. If σ ∈ G_F represents the absolute Artin symbol of a unit u of the valuation ring of F (v(u) = 1), then the p-adic cyclotomic character of σ is the inverse of the norm of u:

χ_cyc (Art_F u) = N_{F/ℚ_p}(u)⁻¹.

TauCeti.ClassFieldTheory.localCyclotomicCharacter_artinMap_unit (p : ℕ) [Fact (Nat.Prime p)]
  (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F]
  [Algebra ℚ_[p] F] [FiniteDimensional ℚ_[p] F] [ValuativeExtension ℚ_[p] F] (u : Fˣ)
  (hu : (ValuativeRel.valuation F) ↑u = 1) (σ : Field.absoluteGaloisGroup F)
  (hσ : ↑σ = (TauCeti.ClassFieldTheory.artinMap F) u) :
  (Units.map ↑(algebraMap ℤ_[p] ℚ_[p])) ((TauCeti.localCyclotomicCharacter p F) σ) =
    ((Units.map (Algebra.norm ℚ_[p])) u)⁻¹

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.localCyclotomicCharacter_artinMap_unit.

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.localCyclotomicCharacter_artinMap_unit
• Source of TauCeti.ClassFieldTheory.localCyclotomicCharacter_artinMap_unit in TauCeti/NumberTheory/ClassFieldTheory/Local/ExplicitCyclotomicSymbol/ArtinMap.lean
• Tau Ceti roadmap status: Local Galois groups of p-adic fields

LeanTauCeti.ClassFieldTheory.localCyclotomicCharacter_artinMap_unit

Uses 14

Statement usesThe local class formation · Tate's theorem for a class formation, in every integer degree

Proof usesArtin's theorem · Artin's theorem for a finite group of automorphisms · Corestriction through Shapiro's lemma · Dedekind's different theorem, the tame case · The first half of Dedekind's different theorem · The Galois group of the maximal unramified extension is the profinite integers · Hensel's lemma for the norm · The local invariant · Restriction through Shapiro's lemma · Tate's theorem · TauCeti.algebraicExtensionNormedField · TauCeti.ClassFieldTheory.tateTheorem

DefinitionLocal reciprocity for A(L)#

If V ≤ G_K is the subgroup fixing the image of a finite extension L/K under ι : L →ₐ[K] Kˢ, then the multiplicative p-adic completion A(L) of Lˣ is canonically isomorphic to V^ab(p), the maximal pro-p quotient of the topological abelianization of V.

TauCeti.padicCompletionUnitsEquivAbelianizationProP (p : ℕ) [Fact (Nat.Prime p)] (K L : Type)
  [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L]
  [IsNonarchimedeanLocalField L] [CharZero L] (ι : L →ₐ[K] SeparableClosure K) :
  ↥(TauCeti.padicCompletionUnits p L) ≃ₜ*
    TauCeti.abelianizationProP p (TauCeti.AbsoluteGaloisGroup K) ↑(TauCeti.galoisSubgroup K L ι)

Lean

Formalized in Tau Ceti as TauCeti.padicCompletionUnitsEquivAbelianizationProP.

Sources

• Tau Ceti documentation: TauCeti.padicCompletionUnitsEquivAbelianizationProP
• Source of TauCeti.padicCompletionUnitsEquivAbelianizationProP in TauCeti/NumberTheory/Padics/MultiplicativeCompletion/Reciprocity.lean
• Tau Ceti roadmap status: Local Galois groups of p-adic fields

LeanTauCeti.padicCompletionUnitsEquivAbelianizationProP

Uses 10 · Used by 2

Statement usesThe local class formation · Tate's theorem for a class formation, in every integer degree

Proof usesCorestriction through Shapiro's lemma · The Kummer isomorphism · The local invariant · Restriction through Shapiro's lemma · Tate's theorem · TauCeti.algebraicExtensionNormedField · TauCeti.ClassFieldTheory.tateTheorem · The third isomorphism theorem for coset spaces

Used byExistence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · The finite level of the generator theorem (NSW, proof of (7.4.1))

DefinitionThe cokernel of the completed norm#

The cokernel of the completed norm A(L) → A(K) is Gal(L/K)^ab / (Gal(L/K)^ab)^(p^m), the maximal p-quotient of Gal(L/K)^ab, once p ^ m contains the full power of p dividing #Gal(L/K)^ab. The isomorphism is induced by the completed norm residue map (TauCeti.padicCompletionUnitsNormCokernelEquiv_mk).

TauCeti.padicCompletionUnitsNormCokernelEquiv.{u_1} (p : ℕ) (K : Type) [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [Fact (Nat.Prime p)] (hpK : ↑p ≠ 0) {m : ℕ}
  (hm : (Nat.card (Abelianization Gal(L/K))).factorization p ≤ m) :
  Additive ↥(TauCeti.padicCompletionUnits p K) ⧸
      (TauCeti.padicCompletionUnitsNorm p K L).range.toAddSubgroup ≃+
    Additive (TauCeti.powerClassQuotient (Abelianization Gal(L/K)) (p ^ m))

Lean

Formalized in Tau Ceti as TauCeti.padicCompletionUnitsNormCokernelEquiv.

Sources

• Tau Ceti documentation: TauCeti.padicCompletionUnitsNormCokernelEquiv
• Source of TauCeti.padicCompletionUnitsNormCokernelEquiv in TauCeti/NumberTheory/Padics/MultiplicativeCompletion/Norm/Cokernel.lean
• Tau Ceti roadmap status: Local Galois groups of p-adic fields

LeanTauCeti.padicCompletionUnitsNormCokernelEquiv

Uses 2

Statement usesThe local class formation · Tate's theorem for a class formation, in every integer degree

TheoremExistence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1))#

For a finite Galois extension L/K of p-adic fields there is a finitely generated ℤ_p[Gal(L/K)]-module of projective dimension at most one which is an extension of the augmentation ideal by A(L).

TauCeti.nonempty_layerTateModule.{u} (p : ℕ) [Fact (Nat.Prime p)] (K L : Type u) [Field L] [Field K]
  [Algebra K L] [Algebra ℚ_[p] L] [Module.Finite ℚ_[p] L] [Algebra ℚ_[p] K]
  [IsScalarTower ℚ_[p] K L] [IsGalois K L] : Nonempty (TauCeti.LayerTateModule p L K)

Lean

Formalized in Tau Ceti as TauCeti.nonempty_layerTateModule.

Sources

• Tau Ceti documentation: TauCeti.nonempty_layerTateModule
• Source of TauCeti.nonempty_layerTateModule in TauCeti/NumberTheory/Padics/MultiplicativeCompletion/LayerTateModule/Cohomology.lean
• Tau Ceti roadmap status: Local Galois groups of p-adic fields

LeanTauCeti.nonempty_layerTateModule

Uses 22 · Used by 1

Proof usesArtin's theorem · Artin's theorem for a finite group of automorphisms · Corestriction through Shapiro's lemma · Dedekind's different theorem, the tame case · Dimension shifting in every positive degree · The first half of Dedekind's different theorem · Hensel's lemma for the norm · The Kummer isomorphism · The local class formation · The local invariant · Local reciprocity for A(L) · Local Tate duality in degree one · Nakayama–Rim, Sylow form · Restriction through Shapiro's lemma · Shapiro's lemma in degree one · The strict cohomological dimension through integral coefficients (NSW (3.3.4)), as vanishing predicates · Tate's cohomological triviality criterion (Milne II 3.10) · Tate's theorem · Tate's theorem for a class formation, in every integer degree · TauCeti.algebraicExtensionNormedField · TauCeti.ClassFieldTheory.tateTheorem · The third isomorphism theorem for coset spaces

Used byThe finite level of the generator theorem (NSW, proof of (7.4.1))

TheoremSwan's theorem for ℤ_p[G] (NSW (5.6.10)(ii))#

Two finitely generated projective ℤ_p[G]-modules with isomorphic rationalizations are isomorphic.

TauCeti.nonempty_linearEquiv_of_projective_of_tensorRat.{u, v, w} (p : ℕ) [Fact (Nat.Prime p)]
  {G : Type u} [Group G] [Finite G] (M : Type v) (N : Type w) [AddCommGroup M]
  [_root_.Module ℤ_[p] M] [_root_.Module (MonoidAlgebra ℤ_[p] G) M]
  [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) M] [Module.Finite (MonoidAlgebra ℤ_[p] G) M]
  [Module.Projective (MonoidAlgebra ℤ_[p] G) M] [AddCommGroup N] [_root_.Module ℤ_[p] N]
  [_root_.Module (MonoidAlgebra ℤ_[p] G) N] [IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] G) N]
  [Module.Finite (MonoidAlgebra ℤ_[p] G) N] [Module.Projective (MonoidAlgebra ℤ_[p] G) N]
  (h :
    Nonempty (TensorProduct ℤ_[p] M ℚ_[p] ≃ₗ[MonoidAlgebra ℤ_[p] G] TensorProduct ℤ_[p] N ℚ_[p])) :
  Nonempty (M ≃ₗ[MonoidAlgebra ℤ_[p] G] N)

Lean

Formalized in Tau Ceti as TauCeti.nonempty_linearEquiv_of_projective_of_tensorRat.

Sources

• Tau Ceti documentation: TauCeti.nonempty_linearEquiv_of_projective_of_tensorRat
• Source of TauCeti.nonempty_linearEquiv_of_projective_of_tensorRat in TauCeti/NumberTheory/Padics/GroupAlgebra/Swan.lean
• Tau Ceti roadmap status: Local Galois groups of p-adic fields

LeanTauCeti.nonempty_linearEquiv_of_projective_of_tensorRat

Uses 1 · Used by 1

Proof usesSchur's lemma, vanishing form

Used byThe finite level of the generator theorem (NSW, proof of (7.4.1))

TheoremShafarevich's theorem#

If a finite compatible extension K of ℚ_[p] contains no primitive pth root of unity, its maximal pro-p Galois group G_K(p) is the free pro-p group on [K : ℚ_[p]] + 1 generators.

TauCeti.nonempty_continuousMulEquiv_freeProP_of_not_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type)
  [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K]
  [ValuativeExtension ℚ_[p] K] (hmu : ¬∃ ζ, IsPrimitiveRoot ζ p) :
  Nonempty
    (TauCeti.absoluteGaloisGroupProP p K ≃ₜ* TauCeti.freeProP p (Fin (Module.finrank ℚ_[p] K + 1)))

Lean

Formalized in Tau Ceti as TauCeti.nonempty_continuousMulEquiv_freeProP_of_not_mu.

Sources

• Tau Ceti documentation: TauCeti.nonempty_continuousMulEquiv_freeProP_of_not_mu
• Source of TauCeti.nonempty_continuousMulEquiv_freeProP_of_not_mu in TauCeti/NumberTheory/LocalField/ProP/Free.lean

LeanTauCeti.nonempty_continuousMulEquiv_freeProP_of_not_mu

Uses 8

Proof usesBurnside's basis theorem, cardinal form · Dimension shifting in every positive degree · The Kummer isomorphism · The local invariant · Local Tate duality in degree one · Serre's theorem at arbitrary rank, as an equivalence · Shapiro's lemma in degree one · TauCeti.algebraicExtensionNormedField

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.