Class Field Theory: other results

Results named in Tau Ceti's TauCeti.NumberTheory.ClassFieldTheory modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe cyclic Hasse norm theorem#

For a cyclic extension L/K of number fields, an element a ∈ Kˣ lies in N_{L/K}(Lˣ) exactly when its principal idele is the norm of an idele of L.

TauCeti.ClassFieldTheory.cyclicHasseNorm (K : Type) [Field K] [NumberField K] (L : Type) [Field L]
  [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] (a : Kˣ) :
  a ∈ TauCeti.normGroup K L ↔
    (NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) a ∈
      (TauCeti.GlobalNumberFields.ideleNormMap K L).range

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.cyclicHasseNorm.

Other forms

The cyclic Hasse norm theorem, placewise. Formalized in Tau Ceti as TauCeti.ClassFieldTheory.isGlobalNorm_iff_isLocalNormEverywhere.

TauCeti.ClassFieldTheory.isGlobalNorm_iff_isLocalNormEverywhere (K : Type) [Field K] [NumberField K]
  (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] (a : Kˣ) :
  a ∈ TauCeti.normGroup K L ↔ TauCeti.GlobalNumberFields.IsLocalNormEverywhere K L a

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.cyclicHasseNorm
• Source of TauCeti.ClassFieldTheory.cyclicHasseNorm in TauCeti/NumberTheory/ClassFieldTheory/Global/HasseNorm/Basic.lean

LeanTauCeti.ClassFieldTheory.cyclicHasseNorm · TauCeti.ClassFieldTheory.isGlobalNorm_iff_isLocalNormEverywhere

Uses 13

Proof usesCorestriction through Shapiro's lemma · The Galois action on the semi-local decomposition · Hensel's lemma for the norm · The Kummer case of the second fundamental inequality · Restriction through Shapiro's lemma · The semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w · Shapiro's lemma for the normalized order · Shapiro's lemma in degree one · The Sylow reduction of Tate's triviality criterion (Milne II 3.10, last paragraph) · Tate's cohomological triviality criterion (Milne II 3.10) · Tate's lattice lemma · TauCeti.algebraicExtensionNormedField · TauCeti.relDiscr

TheoremThe equivariant Kummer isomorphism on Kummer classes (TauCeti.ClassFieldTheory.dualTensorHom_kummerH1ConjRepresentationEquiv)#

Under kummerH1ConjRepresentationEquiv, the Kummer class of a power class x, read on V through restrictSubgroupH1Equiv, corresponds to the homomorphism M → Lˣ ⧸ (Lˣ)ⁿ sending m to log(m) • x, where log : M ≃ μₙ ≃ ℤ/n is e followed by kummerCoeffAddEquivZMod.

TauCeti.ClassFieldTheory.dualTensorHom_kummerH1ConjRepresentationEquiv.{u_1} {F : Type} [Field F]
  {L : Type u_1} [Field L] [Algebra F L] [FiniteDimensional F L] (σ : L →ₐ[F] SeparableClosure F)
  {V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)} {n : ℕ} [Normal F L] (hn : IsUnit ↑n)
  (hV : (TauCeti.absoluteGaloisGroupExtend F L σ).range = ↑V.toOpenSubgroup)
  {M : FDRep (ZMod n) (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)}
  (e :
    (TauCeti.ClassFieldTheory.fdGalRepOfQuotient n F V).obj M ≅ TauCeti.ClassFieldTheory.muNRep n F)
  (x : Additive (TauCeti.powerClassQuotient Lˣ n)) (m : ↑M.V) :
  ((dualTensorHom (ZMod n) (↑M.V) (Additive (TauCeti.powerClassQuotient Lˣ n)))
        ((TauCeti.ClassFieldTheory.kummerH1ConjRepresentationEquiv σ hn hV e)
          ((TauCeti.ClassFieldTheory.restrictSubgroupH1Equiv σ n hV)
            ((TauCeti.fixingSubgroupKummerEquivOfTrivial σ hn (TauCeti.kummerCoeffAddEquivZMod hn) ⋯
                ⋯)
              x))))
      m =
    (TauCeti.kummerCoeffAddEquivZMod hn)
        ((TauCeti.ClassFieldTheory.kummerCoeffEquivMuNRep n F).symm
          ((TopRep.Hom.hom (CategoryTheory.eqToIso ⋯ ≪≫ e).hom) m)) •
      x

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.dualTensorHom_kummerH1ConjRepresentationEquiv.

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.dualTensorHom_kummerH1ConjRepresentationEquiv
• Source of TauCeti.ClassFieldTheory.dualTensorHom_kummerH1ConjRepresentationEquiv in TauCeti/NumberTheory/ClassFieldTheory/Local/EulerCharacteristic/Kummer/Basic.lean

LeanTauCeti.ClassFieldTheory.dualTensorHom_kummerH1ConjRepresentationEquiv

Uses 1

Statement usesThe Kummer isomorphism

TheoremThe Euler characteristic formula and G₀#

Tate's local Euler characteristic formula χ_F(X) = φ_F(X) holds for every finite smooth discrete Galois representation X exactly when, for every open normal subgroup V of G_F, the descended Euler characteristic and the descended normalized absolute value of the order agree on the Grothendieck group of (ZMod n)[G_F ⧸ V].

TauCeti.ClassFieldTheory.forall_localEulerCharacteristic_eq_localCardNorm_iff {n : ℕ} {F : Type}
  [Field F] [NeZero n] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (p : ℕ)
  [Fact (Nat.Prime p)] [TauCeti.FinitePadicExtension F p] (hn : IsUnit ↑n) :
  (∀ (X : TauCeti.ClassFieldTheory.GalRep n F) [inst : Finite ↑X] [DiscreteTopology ↑X]
      [inst_2 : Fact (TauCeti.IsSmoothDiscrete (ZMod n) X)],
      TauCeti.ClassFieldTheory.localEulerCharacteristic ⋯ X =
        TauCeti.ClassFieldTheory.localCardNorm p X) ↔
    ∀ (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)),
      TauCeti.ClassFieldTheory.localEulerCharacteristicK0 V hn =
        TauCeti.ClassFieldTheory.localCardNormK0 n V p

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.forall_localEulerCharacteristic_eq_localCardNorm_iff.

Other forms

The Euler characteristic formula for V on G₀. Formalized in Tau Ceti as TauCeti.ClassFieldTheory.localEulerCharacteristicK0_eq_localCardNormK0_iff.

TauCeti.ClassFieldTheory.localEulerCharacteristicK0_eq_localCardNormK0_iff {n : ℕ} {F : Type}
  [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) [NeZero n] [ValuativeRel F]
  [TopologicalSpace F] [IsNonarchimedeanLocalField F] (p : ℕ) [Fact (Nat.Prime p)]
  [TauCeti.FinitePadicExtension F p] (hn : IsUnit ↑n) :
  TauCeti.ClassFieldTheory.localEulerCharacteristicK0 V hn =
      TauCeti.ClassFieldTheory.localCardNormK0 n V p ↔
    ∀ (X : TauCeti.ClassFieldTheory.GalRep n F) [inst : Finite ↑X] [DiscreteTopology ↑X]
      [inst_2 : Fact (TauCeti.IsSmoothDiscrete (ZMod n) X)],
      (∀ g ∈ V, ∀ (x : ↑X), (X.ρ g) x = x) →
        TauCeti.ClassFieldTheory.localEulerCharacteristic ⋯ X =
          TauCeti.ClassFieldTheory.localCardNorm p X

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.forall_localEulerCharacteristic_eq_localCardNorm_iff
• Source of TauCeti.ClassFieldTheory.forall_localEulerCharacteristic_eq_localCardNorm_iff in TauCeti/NumberTheory/ClassFieldTheory/Local/EulerCharacteristic/GrothendieckGroup.lean

LeanTauCeti.ClassFieldTheory.forall_localEulerCharacteristic_eq_localCardNorm_iff · TauCeti.ClassFieldTheory.localEulerCharacteristicK0_eq_localCardNormK0_iff

Uses 7 · Used by 1

Proof usesThe dual Noether isomorphism · The Kummer isomorphism · The local invariant · Local Tate duality in degree one · The Noether isomorphism for exact categories · Shapiro's lemma in degree one · TauCeti.algebraicExtensionNormedField

Used byModular-Artin reduction of the local Euler characteristic formula

TheoremGlobal existence (Milne VII, Theorem 9.5)#

For a number field K, every open subgroup of finite index of the idele class group C_K is the norm subgroup of a finite abelian extension of K.

TauCeti.ClassFieldTheory.globalAbelianExistence {K : Type} [Field K] [NumberField K]
  {N : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)} (hN : IsOpen ↑N)
  [N.FiniteIndex] :
  ∃ V, V.IsAbelianClassFieldLayer ∧ TauCeti.ClassFieldTheory.globalNormSubgroup K V = N

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.globalAbelianExistence.

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.globalAbelianExistence
• Source of TauCeti.ClassFieldTheory.globalAbelianExistence in TauCeti/NumberTheory/ClassFieldTheory/GlobalExistence/Existence.lean

LeanTauCeti.ClassFieldTheory.globalAbelianExistence

Uses 10

Proof usesCorestriction through Shapiro's lemma · The global class formation · The Kummer case of global existence (Milne VII, Lemma 9.3) · Restriction through Shapiro's lemma · The semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w · 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

TheoremThe Hasse principle for Brauer classes, from idele-class H¹#

If H¹(Gal(L/K), C_L) vanishes for every finite Galois extension L/K, then a Brauer class of K whose localizations at all places vanish is zero: Br K → ⨁_v Br K_v is injective.

TauCeti.ClassFieldTheory.brLocalization_injective_of_subsingleton_groupCohomology_one (K : Type)
  [Field K] [NumberField K]
  (h :
    ∀ (L : Type) [inst : Field L] [inst_1 : NumberField L] [inst_2 : Algebra K L] [IsGalois K L],
      Subsingleton ↑(groupCohomology (TauCeti.ClassFieldTheory.ideleClassRep K L) 1)) :
  Function.Injective ⇑(TauCeti.ClassFieldTheory.brLocalization K)

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.brLocalization_injective_of_subsingleton_groupCohomology_one.

Other forms

The Hasse principle for the Brauer group (Albert–Brauer–Hasse–Noether). Formalized in Tau Ceti as TauCeti.ClassFieldTheory.brLocalization_injective.

TauCeti.ClassFieldTheory.brLocalization_injective (K : Type) [Field K] [NumberField K] :
  Function.Injective ⇑(TauCeti.ClassFieldTheory.brLocalization K)

The Hasse principle from the vanishing of H¹ on the idele-class formation. Formalized in Tau Ceti as TauCeti.ClassFieldTheory.brLocalization_injective_of_subsingleton_h1_globalFormation.

TauCeti.ClassFieldTheory.brLocalization_injective_of_subsingleton_h1_globalFormation (K : Type)
  [Field K] [NumberField K]
  (h :
    ∀ (V : OpenNormalSubgroup (TauCeti.AbsoluteGaloisGroup K)),
      Subsingleton
        ↑((TauCeti.ClassFieldTheory.NormalLayer.ofOpenNormal V).H
            (TauCeti.ClassFieldTheory.globalFormation K) 1)) :
  Function.Injective ⇑(TauCeti.ClassFieldTheory.brLocalization K)

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.brLocalization_injective_of_subsingleton_groupCohomology_one
• Source of TauCeti.ClassFieldTheory.brLocalization_injective_of_subsingleton_groupCohomology_one in TauCeti/NumberTheory/ClassFieldTheory/Global/Brauer/LocalizationKernel.lean

LeanTauCeti.ClassFieldTheory.brLocalization_injective_of_subsingleton_groupCohomology_one · TauCeti.ClassFieldTheory.brLocalization_injective · TauCeti.ClassFieldTheory.brLocalization_injective_of_subsingleton_h1_globalFormation

Uses 14 · Used by 5

Proof usesCorestriction through Shapiro's lemma · The Galois action on the semi-local decomposition · Hensel's lemma for the norm · The Kummer case of the second fundamental inequality · The local invariant · Restriction through Shapiro's lemma · The semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w · Shapiro's lemma for the normalized order · Shapiro's lemma in degree one · The Sylow reduction of Tate's triviality criterion (Milne II 3.10, last paragraph) · Tate's cohomological triviality criterion (Milne II 3.10) · Tate's lattice lemma · TauCeti.algebraicExtensionNormedField · TauCeti.relDiscr

Used byHilbert reciprocity · The global class formation · The global invariant · The global invariant is injective · The Kronecker–Weber theorem

TheoremThe Kronecker–Weber theorem#

every finite abelian extension of ℚ embeds in a cyclotomic field ℚ(ζ_n).

TauCeti.ClassFieldTheory.kroneckerWeber (E : Type) [Field E] [NumberField E] [IsAbelianGalois ℚ E] :
  ∃ n, n ≠ 0 ∧ Nonempty (E →ₐ[ℚ] CyclotomicField n ℚ)

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.kroneckerWeber.

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.kroneckerWeber
• Source of TauCeti.ClassFieldTheory.kroneckerWeber in TauCeti/NumberTheory/ClassFieldTheory/ClassFields/KroneckerWeber.lean

LeanTauCeti.ClassFieldTheory.kroneckerWeber

Uses 32

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 · Euler's theorem on an n-th root of unity · Finite global reciprocity · The first half of Dedekind's different theorem · The Galois action on the semi-local decomposition · The Galois group of the maximal unramified extension is the profinite integers · The global class formation · The global invariant · The Hasse principle for Brauer classes, from idele-class H¹ · Hensel's lemma for the norm · The ideal-theoretic Artin map · IsDedekindDomain.FiniteAdeleRing.sIntegralAdeles · The Kummer case of the second fundamental inequality · The local class formation · The local invariant · The Mackey formula for the degree-one corestriction cochain · The ray class group of ℚ modulo (n)·∞ is the Galois group of ℚ(ζ_n) · Restriction through Shapiro's lemma · The semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w · Shapiro's lemma in degree one · The Sylow reduction of Tate's triviality criterion (Milne II 3.10, last paragraph) · Tate's cohomological triviality criterion (Milne II 3.10) · Tate's lattice lemma · Tate's theorem · Tate's theorem for a class formation, in every integer degree · TauCeti.algebraicExtensionNormedField · TauCeti.ClassFieldTheory.tateTheorem · TauCeti.relDiscr · The third isomorphism theorem for coset spaces

TheoremThe Kummer case of the second fundamental inequality#

Let L/K be a Galois extension of number fields of prime degree p, and suppose that K contains the p-th roots of unity. Then the idele-class norm group has index at most p: [C_K : N_{L/K}(C_L)] ≤ p.

TauCeti.ClassFieldTheory.index_range_ideleClassNormMap_le_of_finrank_prime (K L : Type) [Field K]
  [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (p : ℕ)
  [Fact (Nat.Prime p)] [HasEnoughRootsOfUnity K p] (hfin : Module.finrank K L = p) :
  (TauCeti.GlobalNumberFields.ideleClassNormMap K L).range.index ≤ p

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.index_range_ideleClassNormMap_le_of_finrank_prime.

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.index_range_ideleClassNormMap_le_of_finrank_prime
• Source of TauCeti.ClassFieldTheory.index_range_ideleClassNormMap_le_of_finrank_prime in TauCeti/NumberTheory/ClassFieldTheory/Global/Kummer/Index.lean

LeanTauCeti.ClassFieldTheory.index_range_ideleClassNormMap_le_of_finrank_prime

Uses 15 · Used by 7

Proof usesArtin's theorem · Corestriction through Shapiro's lemma · Dedekind's bound · Euler's criterion in a finite residue domain · The Galois action on the semi-local decomposition · Hensel's lemma for the norm · The local class formation · Restriction through Shapiro's lemma · The semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w · Shapiro's lemma in degree one · Tate's cohomological triviality criterion (Milne II 3.10) · Tate's lattice lemma · Tate's theorem for a class formation, in every integer degree · TauCeti.algebraicExtensionNormedField · TauCeti.relDiscr

Used byThe global class formation · The global invariant · The global invariant is injective · Hilbert sign prescription (O'Meara 71:19a) · The cyclic Hasse norm theorem · The Hasse principle for Brauer classes, from idele-class H¹ · The Kronecker–Weber theorem

TheoremLocal Tate duality in degree one#

Let K be a nonarchimedean local field and n a natural number invertible in K. For every finite discrete G_K-module A killed by n, Tate's duality map H¹(G_K, A) → Hom(H¹(G_K, Hom(A, μₙ)), H²(G_K, μₙ)) is bijective.

TauCeti.ClassFieldTheory.dualityMap1_kummerCoeff_bijective {K : Type} [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (A : Type)
  [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A]
  [DistribMulAction (TauCeti.AbsoluteGaloisGroup K) A]
  [ContinuousSMul (TauCeti.AbsoluteGaloisGroup K) A] [Finite A] (hA : ∀ (a : A), n • a = 0) :
  Function.Bijective
    ⇑(TauCeti.ContCohomology.dualityMap1 (TauCeti.AbsoluteGaloisGroup K) A
        (TauCeti.KummerCoeff K n))

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.dualityMap1_kummerCoeff_bijective.

Other forms

Local Tate duality for the named evaluation pairing. Formalized in Tau Ceti as TauCeti.ClassFieldTheory.tateDualityPairing_flip_perfect.

TauCeti.ClassFieldTheory.tateDualityPairing_flip_perfect {n : ℕ} {F : Type} [Field F]
  [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (hn : IsUnit ↑n)
  (A : TauCeti.ClassFieldTheory.GalRep n F) [DiscreteTopology ↑A] [Finite ↑A]
  [Fact (TauCeti.IsSmoothDiscrete (ZMod n) A)]
  (tr : ↑(continuousCohomology 2 (TauCeti.ClassFieldTheory.muNRep n F)).toModuleCat ≃+ ZMod n)
  (i j : ℕ) (hij : i + j = 2) :
  (∀ (y : ↑(continuousCohomology j A).toModuleCat),
      (∀ (x : ↑(continuousCohomology i (TauCeti.ClassFieldTheory.tateDual A)).toModuleCat),
          TauCeti.ClassFieldTheory.tateDualityPairing A tr i j hij x y = 0) →
        y = 0) ∧
    ∀ (ψ : ↑(continuousCohomology i (TauCeti.ClassFieldTheory.tateDual A)).toModuleCat →+ ZMod n),
      ∃ y,
        ∀ (x : ↑(continuousCohomology i (TauCeti.ClassFieldTheory.tateDual A)).toModuleCat),
          TauCeti.ClassFieldTheory.tateDualityPairing A tr i j hij x y = ψ x

Local Tate duality in degree two. Formalized in Tau Ceti as TauCeti.ClassFieldTheory.dualityMap2_kummerCoeff_bijective.

TauCeti.ClassFieldTheory.dualityMap2_kummerCoeff_bijective {K : Type} [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (A : Type)
  [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A]
  [DistribMulAction (TauCeti.AbsoluteGaloisGroup K) A]
  [ContinuousSMul (TauCeti.AbsoluteGaloisGroup K) A] [Finite A] (hA : ∀ (a : A), n • a = 0) :
  Function.Bijective
    ⇑(TauCeti.ContCohomology.dualityMap2 (TauCeti.AbsoluteGaloisGroup K) A
        (TauCeti.KummerCoeff K n))

Local Tate duality in degree zero. Formalized in Tau Ceti as TauCeti.ClassFieldTheory.dualityMap0_kummerCoeff_bijective.

TauCeti.ClassFieldTheory.dualityMap0_kummerCoeff_bijective {K : Type} [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (A : Type)
  [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A]
  [DistribMulAction (TauCeti.AbsoluteGaloisGroup K) A]
  [ContinuousSMul (TauCeti.AbsoluteGaloisGroup K) A] [Finite A] (hA : ∀ (a : A), n • a = 0) :
  Function.Bijective
    ⇑(TauCeti.ContCohomology.dualityMap0 (TauCeti.AbsoluteGaloisGroup K) A
        (TauCeti.KummerCoeff K n))

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.dualityMap1_kummerCoeff_bijective
• Source of TauCeti.ClassFieldTheory.dualityMap1_kummerCoeff_bijective in TauCeti/NumberTheory/ClassFieldTheory/Local/Duality/FiniteModule.lean

LeanTauCeti.ClassFieldTheory.dualityMap1_kummerCoeff_bijective · TauCeti.ClassFieldTheory.tateDualityPairing_flip_perfect · TauCeti.ClassFieldTheory.dualityMap2_kummerCoeff_bijective · TauCeti.ClassFieldTheory.dualityMap0_kummerCoeff_bijective

Uses 5 · Used by 8

Proof usesThe Kummer isomorphism · The local invariant · Shapiro's lemma in degree one · Tate's duality on an open subgroup acting trivially on μₙ · TauCeti.algebraicExtensionNormedField

Used byPerfect local Tate duality for E[m] · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · Shafarevich's theorem · Modular-Artin reduction of the local Euler characteristic formula · Perfect local Tate duality in mixed characteristic · Tate's local Euler characteristic formula · The Euler characteristic formula and G₀ · The finite level of the generator theorem (NSW, proof of (7.4.1))

TheoremModular-Artin reduction of the local Euler characteristic formula#

If χ_F = φ_F holds for the inflation to G_F of every representation of a finite Galois quotient G_F ⧸ V induced from a cyclic subgroup of order prime to ℓ, then it holds for every finite smooth discrete ZMod ℓ-representation of G_F.

TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm_of_indFDRep (p : ℕ)
  [Fact (Nat.Prime p)] (F : Type) [Field F] [CharZero F] [ValuativeRel F] [TopologicalSpace F]
  [IsNonarchimedeanLocalField F] [TauCeti.FinitePadicExtension F p] (ℓ : ℕ) [Fact (Nat.Prime ℓ)]
  (h :
    ∀ (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F))
      (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)),
      IsCyclic ↥C ∧ ¬ℓ ∣ Nat.card ↥C →
        ∀ (B : FDRep (ZMod ℓ) ↥C),
          TauCeti.ClassFieldTheory.localEulerCharacteristic ⋯
              ((TauCeti.ClassFieldTheory.fdGalRepOfQuotient ℓ F V).obj (TauCeti.indFDRep B)) =
            TauCeti.ClassFieldTheory.localCardNorm p
              ((TauCeti.ClassFieldTheory.fdGalRepOfQuotient ℓ F V).obj (TauCeti.indFDRep B)))
  (A : TauCeti.ClassFieldTheory.GalRep ℓ F) [Finite ↑A] [DiscreteTopology ↑A]
  [Fact (TauCeti.IsSmoothDiscrete (ZMod ℓ) A)] :
  TauCeti.ClassFieldTheory.localEulerCharacteristic ⋯ A = TauCeti.ClassFieldTheory.localCardNorm p A

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm_of_indFDRep.

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm_of_indFDRep
• Source of TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm_of_indFDRep in TauCeti/NumberTheory/ClassFieldTheory/Local/EulerCharacteristic/ModularInduction.lean

LeanTauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm_of_indFDRep

Uses 10 · Used by 1

Proof usesArtin's induction identity for every virtual class over every field · The dual Noether isomorphism · The Euler characteristic formula and G₀ · Kolchin's common fixed vector theorem · The Kummer isomorphism · The local invariant · Local Tate duality in degree one · The Noether isomorphism for exact categories · Shapiro's lemma in degree one · TauCeti.algebraicExtensionNormedField

Used byTate's local Euler characteristic formula

TheoremPerfect local Tate duality in mixed characteristic#

For a characteristic-zero nonarchimedean local field F, every finite smooth discrete ZMod n-representation has a perfect local Tate-duality pairing in complementary degrees.

TauCeti.ClassFieldTheory.tateDualityPairing_perfect_mixed (F : Type) [Field F] [CharZero F]
  [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (n : ℕ) (hn : n ≠ 0)
  (A : TauCeti.ClassFieldTheory.GalRep n F)
  (tr : ↑(continuousCohomology 2 (TauCeti.ClassFieldTheory.muNRep n F)).toModuleCat ≃+ ZMod n)
  (hA : Finite ↑A) [DiscreteTopology ↑A] [Fact (TauCeti.IsSmoothDiscrete (ZMod n) A)] (i j : ℕ)
  (hij : i + j = 2) :
  (∀ (x : ↑(continuousCohomology i (TauCeti.ClassFieldTheory.tateDual A)).toModuleCat),
      (∀ (y : ↑(continuousCohomology j A).toModuleCat),
          TauCeti.ClassFieldTheory.tateDualityPairing A tr i j hij x y = 0) →
        x = 0) ∧
    ∀ (φ : ↑(continuousCohomology j A).toModuleCat →+ ZMod n),
      ∃ x,
        ∀ (y : ↑(continuousCohomology j A).toModuleCat),
          TauCeti.ClassFieldTheory.tateDualityPairing A tr i j hij x y = φ y

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.tateDualityPairing_perfect_mixed.

Other forms

Perfect local Tate duality for the named evaluation pairing. Formalized in Tau Ceti as TauCeti.ClassFieldTheory.tateDualityPairing_perfect.

TauCeti.ClassFieldTheory.tateDualityPairing_perfect {n : ℕ} {F : Type} [Field F] [ValuativeRel F]
  [TopologicalSpace F] [IsNonarchimedeanLocalField F] (hn : IsUnit ↑n)
  (A : TauCeti.ClassFieldTheory.GalRep n F) [DiscreteTopology ↑A] [Finite ↑A]
  [Fact (TauCeti.IsSmoothDiscrete (ZMod n) A)]
  (tr : ↑(continuousCohomology 2 (TauCeti.ClassFieldTheory.muNRep n F)).toModuleCat ≃+ ZMod n)
  (i j : ℕ) (hij : i + j = 2) :
  (∀ (x : ↑(continuousCohomology i (TauCeti.ClassFieldTheory.tateDual A)).toModuleCat),
      (∀ (y : ↑(continuousCohomology j A).toModuleCat),
          TauCeti.ClassFieldTheory.tateDualityPairing A tr i j hij x y = 0) →
        x = 0) ∧
    ∀ (φ : ↑(continuousCohomology j A).toModuleCat →+ ZMod n),
      ∃ x,
        ∀ (y : ↑(continuousCohomology j A).toModuleCat),
          TauCeti.ClassFieldTheory.tateDualityPairing A tr i j hij x y = φ y

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.tateDualityPairing_perfect_mixed
• Source of TauCeti.ClassFieldTheory.tateDualityPairing_perfect_mixed in TauCeti/NumberTheory/ClassFieldTheory/Local/Duality/Perfect.lean

LeanTauCeti.ClassFieldTheory.tateDualityPairing_perfect_mixed · TauCeti.ClassFieldTheory.tateDualityPairing_perfect

Uses 5 · Used by 1

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

Used byTate's local Euler characteristic formula

TheoremThe principal ideal theorem for a class formation#

Let V ◁ U be a layer, K/F in field notation, and restrict it to the ground subgroup U' whose image U'/V is the commutator subgroup of U/V, the layer K/E over the maximal abelian subextension E. Then every element of the ground level A^U is, in A^{U'}, a norm from A^V.

TauCeti.ClassFieldTheory.ClassFormation.groundInclusion_mem_normSubgroup_of_range_eq_commutator
  {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] {F : TauCeti.ClassFieldTheory.Formation G}
  (cf : TauCeti.ClassFieldTheory.ClassFormation F)
  {small big : TauCeti.ClassFieldTheory.NormalLayer G}
  (T : TauCeti.ClassFieldTheory.LayerRestriction small big)
  (hT : T.galHom.range = commutator big.Gal) (a : ↥(F.level big.ground)) :
  (T.groundInclusion F) a ∈ small.normSubgroup F

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.ClassFormation.groundInclusion_mem_normSubgroup_of_range_eq_commutator.

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.ClassFormation.groundInclusion_mem_normSubgroup_of_range_eq_commutator
• Source of TauCeti.ClassFieldTheory.ClassFormation.groundInclusion_mem_normSubgroup_of_range_eq_commutator in TauCeti/NumberTheory/ClassFieldTheory/Formation/PrincipalIdeal.lean

LeanTauCeti.ClassFieldTheory.ClassFormation.groundInclusion_mem_normSubgroup_of_range_eq_commutator

Uses 6 · Used by 1

Proof usesCorestriction through Shapiro's lemma · Furtwängler's theorem, the group-theoretic principal ideal theorem · Restriction through Shapiro's lemma · Tate's theorem · Tate's theorem for a class formation, in every integer degree · TauCeti.ClassFieldTheory.tateTheorem

Used byThe idelic consequence of Furtwängler's theorem

TheoremShapiro's lemma for the normalized order#

For L the fixed field of C ≤ G_K ⧸ V, the invariant φ_K(A) = ‖#A‖_K = |#A|_p ^ [K : ℚ_p] of the inflation of Ind_C^{G_K ⧸ V} B is that of B over L: #Ind B = #B ^ [L : K] and [L : ℚ_p] = [K : ℚ_p] [L : K].

TauCeti.ClassFieldTheory.localCardNorm_galRepOfQuotient_ind {K : Type} [Field K] {L : Type}
  [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (n : ℕ)
  {V : OpenNormalSubgroup (Field.absoluteGaloisGroup K)}
  {C : Subgroup (Field.absoluteGaloisGroup K ⧸ ↑V.toOpenSubgroup)}
  (hσ :
    (TauCeti.absoluteGaloisGroupExtend K L σ).range =
      Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C)
  (B : Rep.{0, 0, 0} (ZMod n) ↥C) (p : ℕ) [Fact (Nat.Prime p)] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] [TauCeti.FinitePadicExtension K p] [ValuativeRel L]
  [TopologicalSpace L] [IsNonarchimedeanLocalField L] [TauCeti.FinitePadicExtension L p]
  [IsScalarTower ℚ_[p] K L] [Finite ↑B] :
  TauCeti.ClassFieldTheory.localCardNorm p
      ((TauCeti.ClassFieldTheory.galRepOfQuotient n K V).obj (Rep.ind C.subtype B)) =
    TauCeti.ClassFieldTheory.localCardNorm p (TauCeti.ClassFieldTheory.shapiroGalRep σ n hσ B)

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.localCardNorm_galRepOfQuotient_ind.

Other forms

Shapiro's lemma for infinite semi-local units in positive degrees. Formalized in Tau Ceti as NumberField.InfinitePlace.infiniteSemilocalUnitsTateCohomologyIsoPos.

NumberField.InfinitePlace.infiniteSemilocalUnitsTateCohomologyIsoPos {K L : Type} [Field K]
  [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L]
  (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) [w.LiesOver v] (n : ℕ)
  [NeZero n] :
  tateCohomology (TauCeti.GlobalNumberFields.infiniteSemilocalUnitsRep L v) ↑n ≅
    tateCohomology (Rep.ofAlgebraAutOnUnits v.Completion w.Completion) ↑n

Shapiro's lemma for semi-local units in positive degrees. Formalized in Tau Ceti as IsDedekindDomain.HeightOneSpectrum.semilocalUnitsTateCohomologyIsoPos.

IsDedekindDomain.HeightOneSpectrum.semilocalUnitsTateCohomologyIsoPos {K L : Type} [Field K]
  [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))
  (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L))
  [w.asIdeal.LiesOver v.asIdeal] (n : ℕ) [NeZero n] :
  tateCohomology (TauCeti.semilocalUnitsRep L v) ↑n ≅
    tateCohomology
      (Rep.ofAlgebraAutOnUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
        (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w))
      ↑n

Shapiro's lemma for the local Euler characteristic. Formalized in Tau Ceti as TauCeti.ClassFieldTheory.localEulerCharacteristic_galRepOfQuotient_ind.

TauCeti.ClassFieldTheory.localEulerCharacteristic_galRepOfQuotient_ind {K : Type} [Field K]
  {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K)
  (n : ℕ) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup K)}
  {C : Subgroup (Field.absoluteGaloisGroup K ⧸ ↑V.toOpenSubgroup)}
  (hσ :
    (TauCeti.absoluteGaloisGroupExtend K L σ).range =
      Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C)
  (B : Rep.{0, 0, 0} (ZMod n) ↥C) [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] [ValuativeRel L] [TopologicalSpace L]
  [IsNonarchimedeanLocalField L] (hn : ↑n ≠ 0) [Finite ↑B] :
  TauCeti.ClassFieldTheory.localEulerCharacteristic hn
      ((TauCeti.ClassFieldTheory.galRepOfQuotient n K V).obj (Rep.ind C.subtype B)) =
    TauCeti.ClassFieldTheory.localEulerCharacteristic ⋯
      (TauCeti.ClassFieldTheory.shapiroGalRep σ n hσ B)

Shapiro's lemma for the semi-local units. Formalized in Tau Ceti as TauCeti.ClassFieldTheory.semilocalUnitsTateCohomologyIso.

TauCeti.ClassFieldTheory.semilocalUnitsTateCohomologyIso {K : Type} [Field K] [NumberField K]
  {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))
  (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L))
  [w.asIdeal.LiesOver v.asIdeal] (n : ℤ) :
  tateCohomology (TauCeti.semilocalUnitsRep L v) n ≅
    tateCohomology
      (Rep.ofAlgebraAutOnUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
        (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w))
      n

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.localCardNorm_galRepOfQuotient_ind
• Source of TauCeti.ClassFieldTheory.localCardNorm_galRepOfQuotient_ind in TauCeti/NumberTheory/ClassFieldTheory/Local/EulerCharacteristic/Induced.lean

LeanTauCeti.ClassFieldTheory.localCardNorm_galRepOfQuotient_ind · NumberField.InfinitePlace.infiniteSemilocalUnitsTateCohomologyIsoPos · IsDedekindDomain.HeightOneSpectrum.semilocalUnitsTateCohomologyIsoPos · TauCeti.ClassFieldTheory.localEulerCharacteristic_galRepOfQuotient_ind · TauCeti.ClassFieldTheory.semilocalUnitsTateCohomologyIso

Uses 5 · Used by 3

Statement usesThe semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w · Shapiro's lemma in degree one

Proof usesThe Kummer isomorphism · The local invariant · TauCeti.algebraicExtensionNormedField

Used byTate's local Euler characteristic formula · The cyclic Hasse norm theorem · The Hasse principle for Brauer classes, from idele-class H¹

TheoremTate's duality on an open subgroup acting trivially on μₙ#

Let V be an open subgroup of G_K acting trivially on μₙ, for n invertible in the local field K. For every finite discrete V-module A killed by n on which V acts trivially, the three duality maps Hⁱ(V, A) → Hom(H²⁻ⁱ(V, Hom(A, μₙ)), H²(V, μₙ)) are bijective.

TauCeti.ClassFieldTheory.dualityMap_bijective_of_smul_kummerCoeff_eq_self {K : Type} [Field K]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n)
  (V : Subgroup (TauCeti.AbsoluteGaloisGroup K)) (hV : IsOpen ↑V)
  (hVN : ∀ v ∈ V, ∀ (y : TauCeti.KummerCoeff K n), v • y = y) (A : Type) [AddCommGroup A]
  [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (↥V) A] [ContinuousSMul (↥V) A]
  [Finite A] (hA : ∀ (a : A), n • a = 0) (hAV : ∀ (v : ↥V) (a : A), v • a = a) :
  Function.Bijective ⇑(TauCeti.ContCohomology.dualityMap0 (↥V) A (TauCeti.KummerCoeff K n)) ∧
    Function.Bijective ⇑(TauCeti.ContCohomology.dualityMap1 (↥V) A (TauCeti.KummerCoeff K n)) ∧
      Function.Bijective ⇑(TauCeti.ContCohomology.dualityMap2 (↥V) A (TauCeti.KummerCoeff K n))

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.dualityMap_bijective_of_smul_kummerCoeff_eq_self.

Other forms

Tate's duality on a module coinduced from an open subgroup acting trivially on μₙ. Formalized in Tau Ceti as TauCeti.ClassFieldTheory.dualityMap_bijective_discreteCoind_kummerCoeff.

TauCeti.ClassFieldTheory.dualityMap_bijective_discreteCoind_kummerCoeff {K : Type} [Field K]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n)
  (V : Subgroup (TauCeti.AbsoluteGaloisGroup K)) (hV : IsOpen ↑V)
  (hVN : ∀ v ∈ V, ∀ (y : TauCeti.KummerCoeff K n), v • y = y) (A : Type) [AddCommGroup A]
  [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (↥V) A] [ContinuousSMul (↥V) A]
  [Finite A] (hA : ∀ (a : A), n • a = 0) (hAV : ∀ (v : ↥V) (a : A), v • a = a) [V.FiniteIndex] :
  Function.Bijective
      ⇑(TauCeti.ContCohomology.dualityMap0 (TauCeti.AbsoluteGaloisGroup K)
          (TauCeti.DiscreteCoind (TauCeti.AbsoluteGaloisGroup K) V A) (TauCeti.KummerCoeff K n)) ∧
    Function.Bijective
        ⇑(TauCeti.ContCohomology.dualityMap1 (TauCeti.AbsoluteGaloisGroup K)
            (TauCeti.DiscreteCoind (TauCeti.AbsoluteGaloisGroup K) V A) (TauCeti.KummerCoeff K n)) ∧
      Function.Bijective
        ⇑(TauCeti.ContCohomology.dualityMap2 (TauCeti.AbsoluteGaloisGroup K)
            (TauCeti.DiscreteCoind (TauCeti.AbsoluteGaloisGroup K) V A) (TauCeti.KummerCoeff K n))

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.dualityMap_bijective_of_smul_kummerCoeff_eq_self
• Source of TauCeti.ClassFieldTheory.dualityMap_bijective_of_smul_kummerCoeff_eq_self in TauCeti/NumberTheory/ClassFieldTheory/Local/Duality/FiniteModule.lean

LeanTauCeti.ClassFieldTheory.dualityMap_bijective_of_smul_kummerCoeff_eq_self · TauCeti.ClassFieldTheory.dualityMap_bijective_discreteCoind_kummerCoeff

Uses 9 · Used by 1

Proof usesArtin's theorem · Artin's theorem for a finite group of automorphisms · Dedekind's different theorem, the tame case · The first half of Dedekind's different theorem · Hensel's lemma for the norm · The Kummer isomorphism · The local invariant · Shapiro's lemma in degree one · TauCeti.algebraicExtensionNormedField

Used byLocal Tate duality in degree one

TheoremTate's local Euler characteristic formula#

The Euler characteristic of a finite smooth discrete Galois module equals the normalized absolute value of its order.

TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm (p : ℕ) [Fact (Nat.Prime p)]
  (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F]
  [TauCeti.FinitePadicExtension F p] (n : ℕ) [NeZero n] (A : TauCeti.ClassFieldTheory.GalRep n F)
  [Finite ↑A] [Fact (TauCeti.IsSmoothDiscrete (ZMod n) A)] :
  TauCeti.ClassFieldTheory.localEulerCharacteristic ⋯ A = TauCeti.ClassFieldTheory.localCardNorm p A

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm.

Other forms

Tate's local Euler characteristic formula, prime-to-ℓ case. Formalized in Tau Ceti as TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm_of_index_coprime.

TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm_of_index_coprime (p : ℕ)
  [Fact (Nat.Prime p)] {F : Type} [Field F] [CharZero F] [ValuativeRel F] [TopologicalSpace F]
  [IsNonarchimedeanLocalField F] [TauCeti.FinitePadicExtension F p] {ℓ : ℕ} [Fact (Nat.Prime ℓ)]
  (A : TauCeti.ClassFieldTheory.GalRep ℓ F) [Finite ↑A] [Fact (TauCeti.IsSmoothDiscrete (ZMod ℓ) A)]
  (N : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (hN : (↑N.toOpenSubgroup).index.Coprime ℓ)
  (hA : ∀ g ∈ N, ∀ (x : ↑A), (A.ρ g) x = x) :
  TauCeti.ClassFieldTheory.localEulerCharacteristic ⋯ A = TauCeti.ClassFieldTheory.localCardNorm p A

Sources

• Tau Ceti documentation: TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm
• Source of TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm in TauCeti/NumberTheory/ClassFieldTheory/Local/EulerCharacteristic/Theorem.lean

LeanTauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm · TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm_of_index_coprime

Uses 10

Proof usesThe dual Noether isomorphism · The Kummer isomorphism · The local invariant · Local Tate duality in degree one · Modular-Artin reduction of the local Euler characteristic formula · The Noether isomorphism for exact categories · Perfect local Tate duality in mixed characteristic · Shapiro's lemma for the normalized order · Shapiro's lemma in degree one · TauCeti.algebraicExtensionNormedField

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.