Class field theory

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.

DefinitionTate's theorem for a class formation, in every integer degree #

the generic theorem applied to the fundamental class, with the three hypotheses discharged by the three individually named consequences of the axioms. This is Artin–Tate's Main Theorem (Chapter XIV §4, Theorem 1).

TauCeti.ClassFieldTheory.ClassFormation.tateIso {G : Type} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
  {F : TauCeti.ClassFieldTheory.Formation G} (cf : TauCeti.ClassFieldTheory.ClassFormation F)
  (L : TauCeti.ClassFieldTheory.NormalLayer G) (r : ℤ) : ↑(L.TrivialTateH r) ≃+ ↑(L.TateH F (r + 2))

Lean

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

Sources

LeanTauCeti.ClassFieldTheory.ClassFormation.tateIso

Uses 1 · Used by 16

Statement usesTauCeti.ClassFieldTheory.tateTheorem

Used byFinite global reciprocity · Hilbert reciprocity · Local reciprocity for the Weil group · The global class formation · The global invariant · The global invariant is injective · The Kummer case of global existence (Milne VII, Lemma 9.3) · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · Local reciprocity for A(L) · The cokernel of the completed norm · The cyclotomic normalization of the local Artin map of a finite extension of ℚ_p · Global existence (Milne VII, Theorem 9.5) · The Kronecker–Weber theorem · The Kummer case of the second fundamental inequality · The principal ideal theorem for a class formation · The finite level of the generator theorem (NSW, proof of (7.4.1))

DefinitionLocal reciprocity for the Weil group #

For a nonarchimedean local field K of characteristic zero, the local Artin map is an isomorphism of topological groups from Kˣ onto the topological abelianization of the local Weil group (localWeilArtinEquiv_apply).

TauCeti.ClassFieldTheory.localWeilArtinEquiv (K : Type) [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] :
  Kˣ ≃ₜ* TopologicalAbelianization (TauCeti.ClassFieldTheory.WeilGroup K)

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.localWeilArtinEquiv.

Sources

LeanTauCeti.ClassFieldTheory.localWeilArtinEquiv

Uses 16

Statement usesThe Galois group of the maximal unramified extension is the profinite integers · The local class formation · Tate's theorem for a class formation, in every integer degree · TauCeti.algebraicExtensionNormedField

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 · Hensel's lemma for the norm · The Kummer isomorphism · The local invariant · Restriction through Shapiro's lemma · Tate's theorem · TauCeti.ClassFieldTheory.tateTheorem · The third isomorphism theorem for coset spaces

DefinitionFinite global reciprocity #

Finite global reciprocity C_K / N_{L/K}(C_L) ≃ Gal(L/K)^ab for a finite Galois extension L/K of number fields, embedded in the separable closure of K by ι: the abstract Artin reciprocity isomorphism ClassFormation.artinEquiv of the global class formation on the layer of L, read through globalLayerNormQuotientEquiv K L and layerGalEquiv ι. It does not depend on ι (globalArtinEquiv_eq_of_iota).

TauCeti.ClassFieldTheory.globalArtinEquiv.{u_1} (K : Type) [Field K] [NumberField K] (L : Type u_1)
  [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) :
  Additive
      (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K ⧸
        (↑(TauCeti.GlobalNumberFields.ideleClassNormMap K L)).range) ≃+
    Additive (Abelianization Gal(L/K))

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.globalArtinEquiv.

Sources

LeanTauCeti.ClassFieldTheory.globalArtinEquiv

Uses 4 · Used by 2

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

Proof usesThe semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w · TauCeti.algebraicExtensionNormedField

Used byThe norm index theorem · The Kronecker–Weber theorem

TheoremThe norm index theorem #

for a finite abelian extension L/K of number fields, [C_K : N_{L/K}(C_L)] = [L : K], since finite global reciprocity identifies the norm quotient with Gal(L/K)^ab, which is Gal(L/K) itself.

TauCeti.ClassFieldTheory.card_ideleClassNormQuotient.{u_1} (K : Type) [Field K] [NumberField K]
  (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] :
  Nat.card
      (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K ⧸
        (↑(TauCeti.GlobalNumberFields.ideleClassNormMap K L)).range) =
    Module.finrank K L

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.card_ideleClassNormQuotient.

Sources

LeanTauCeti.ClassFieldTheory.card_ideleClassNormQuotient

Uses 3 · Used by 1

Proof usesFinite global reciprocity · The semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w · TauCeti.algebraicExtensionNormedField

Used byThe Kummer case of global existence (Milne VII, Lemma 9.3)

TheoremHilbert reciprocity #

For a, b ∈ Kˣ, the Hilbert invariants of a and b at all the finite and infinite places of the number field K sum to zero.

TauCeti.ClassFieldTheory.hilbertProductFormula {K : Type} [Field K] [NumberField K] (a b : Kˣ) :
  ∑ v ∈ TauCeti.ClassFieldTheory.finiteHilbertSupport K a b,
        TauCeti.ClassFieldTheory.finiteHilbertInvariantAt K v a b +
      ∑ w, TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt K w a b =
    0

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.hilbertProductFormula.

Sources

LeanTauCeti.ClassFieldTheory.hilbertProductFormula

Uses 18 · Used by 1

Statement usesThe Kummer isomorphism · The local invariant

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 · The first half of Dedekind's different theorem · The Galois group of the maximal unramified extension is the profinite integers · The Hasse principle for Brauer classes, from idele-class H¹ · 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 · Tate's theorem · Tate's theorem for a class formation, in every integer degree · TauCeti.algebraicExtensionNormedField · TauCeti.ClassFieldTheory.tateTheorem

Used byHilbert's product formula

TheoremQuadratic reciprocity is Hilbert reciprocity for two odd primes #

For distinct odd primes p and q, the cohomological Hilbert invariants of p and q sum to zero over the places of ℚ exactly when (p / q) (q / p) = (-1) ^ ((p - 1)/2 · (q - 1)/2). So Hilbert's reciprocity law ∑_v inv_v((p) ∪ (q)) = 0 gives the quadratic reciprocity law, its dyadic factor being the sign.

TauCeti.ClassFieldTheory.sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt_eq_zero_iff
  {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] {a b : ℚˣ} (hp : p ≠ 2) (hq : q ≠ 2)
  (hpq : p ≠ q) (ha : ↑a = ↑p) (hb : ↑b = ↑q) :
  ∑ v ∈ TauCeti.ClassFieldTheory.finiteHilbertSupport ℚ a b,
          TauCeti.ClassFieldTheory.finiteHilbertInvariantAt ℚ v a b +
        ∑ w, TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt ℚ w a b =
      0 ↔
    legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt_eq_zero_iff.

Sources

LeanTauCeti.ClassFieldTheory.sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt_eq_zero_iff

Uses 10

Statement usesThe Kummer isomorphism · The local invariant

Proof usesThe cup-norm theorem · Dedekind's different theorem, the tame case · Euler's theorem on an n-th root of unity · The first half of Dedekind's different theorem · Hensel's lemma for the norm · Serre's formula for the Artin conductor · The splitting criterion for quaternion algebras · TauCeti.algebraicExtensionNormedField

DefinitionThe global invariant #

The global invariant H²(Gal(L/F), C_L) → ℚ/ℤ of a finite normal layer L/F inside Kˢ: the invariant of a class is the sum of the local invariants of a lift to the ideles of its inflation to some refinement of the layer. By globalInv_eq it does not depend on the refinement or on the lift, and globalInv_unique characterizes it by the equations globalInv_ideleToClassH2 and globalInv_infl.

TauCeti.ClassFieldTheory.globalInv (K : Type) [Field K] [NumberField K]
  (L : TauCeti.ClassFieldTheory.NormalLayer (TauCeti.AbsoluteGaloisGroup K)) :
  ↑(L.H (TauCeti.ClassFieldTheory.globalFormation K) 2) →+ AddCircle 1

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.globalInv.

Sources

LeanTauCeti.ClassFieldTheory.globalInv

Uses 25 · Used by 2

Statement usesThe local invariant · The semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w

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 · 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 Hasse principle for Brauer classes, from idele-class H¹ · Hensel's lemma for the norm · The Kummer case of the second fundamental inequality · The local class formation · The Mackey formula for the degree-one corestriction cochain · Restriction through Shapiro's lemma · 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

Used byThe global invariant is injective · The Kronecker–Weber theorem

TheoremThe global invariant is injective #

The global invariant is injective, because the idele-class H¹ vanishes and the sum of the local invariants vanishes only on the classes that die in the idele classes.

TauCeti.ClassFieldTheory.globalInv_injective {K : Type} [Field K] [NumberField K]
  (L : TauCeti.ClassFieldTheory.NormalLayer (TauCeti.AbsoluteGaloisGroup K)) :
  Function.Injective ⇑(TauCeti.ClassFieldTheory.globalInv K L)

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.globalInv_injective.

Sources

LeanTauCeti.ClassFieldTheory.globalInv_injective

Uses 26

Statement usesThe global invariant

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 · 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 Hasse principle for Brauer classes, from idele-class H¹ · Hensel's lemma for the norm · The Kummer case of the second fundamental inequality · The local class formation · The local invariant · The Mackey formula for the degree-one corestriction cochain · 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

DefinitionThe global class formation #

the idele-class formation of K is a class formation, whose invariant on a layer is the global invariant (globalClassFormation_inv).

TauCeti.ClassFieldTheory.globalClassFormation (K : Type) [Field K] [NumberField K] :
  TauCeti.ClassFieldTheory.ClassFormation (TauCeti.ClassFieldTheory.globalFormation K)

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.globalClassFormation.

Sources

LeanTauCeti.ClassFieldTheory.globalClassFormation

Uses 25 · Used by 5

Statement usesThe local invariant · The semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w

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 · 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 Hasse principle for Brauer classes, from idele-class H¹ · Hensel's lemma for the norm · The Kummer case of the second fundamental inequality · The local class formation · The Mackey formula for the degree-one corestriction cochain · Restriction through Shapiro's lemma · 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

Used byFinite global reciprocity · The idelic consequence of Furtwängler's theorem · The Kummer case of global existence (Milne VII, Lemma 9.3) · Global existence (Milne VII, Theorem 9.5) · The Kronecker–Weber theorem

DefinitionThe local invariant #

The local invariant inv_K : Br K ≃+ ℚ/ℤ of a nonarchimedean local field K, normalized by arithmetic Frobenius: on the classes inflated from an unramified extension E/K inside Kˢ it is the invariant TauCeti.ClassFieldTheory.unramifiedInv K E of the layer (invMap_relBrInfl).

TauCeti.ClassFieldTheory.invMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] : TauCeti.ClassFieldTheory.Br K ≃+ AddCircle 1

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.invMap.

Sources

LeanTauCeti.ClassFieldTheory.invMap

Uses 6 · Used by 24

Statement usesTauCeti.algebraicExtensionNormedField

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

Used byPerfect local Tate duality for E[m] · Hilbert reciprocity · Local reciprocity for the Weil group · Quadratic reciprocity is Hilbert reciprocity for two odd primes · The global class formation · The global invariant · The global invariant is injective · The local class formation · Demushkin's theorem · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · Local reciprocity for A(L) · Shafarevich's theorem · The cyclotomic normalization of the local Artin map of a finite extension of ℚ_p · Hilbert's product formula · Local Tate duality in degree one · Modular-Artin reduction of the local Euler characteristic formula · Perfect local Tate duality in mixed characteristic · Shapiro's lemma for the normalized order · Tate's duality on an open subgroup acting trivially on μₙ · Tate's local Euler characteristic formula · The Euler characteristic formula and G₀ · The Hasse principle for Brauer classes, from idele-class H¹ · The Kronecker–Weber theorem · The finite level of the generator theorem (NSW, proof of (7.4.1))

DefinitionThe local class formation #

the formation of the units of a separable closure of a nonarchimedean local field K is a class formation, with the invariant layerInv of a layer as invariant map.

TauCeti.ClassFieldTheory.localClassFormation (K : Type) [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
  TauCeti.ClassFieldTheory.ClassFormation (TauCeti.ClassFieldTheory.unitsFormation K)

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.localClassFormation.

Sources

LeanTauCeti.ClassFieldTheory.localClassFormation

Uses 8 · Used by 13

Statement usesThe local invariant

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 · Shapiro's lemma in degree one · TauCeti.algebraicExtensionNormedField

Used byHilbert reciprocity · Local reciprocity for the Weil group · The global class formation · The global invariant · The global invariant is injective · The Kummer case of global existence (Milne VII, Lemma 9.3) · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · Local reciprocity for A(L) · The cokernel of the completed norm · The cyclotomic normalization of the local Artin map of a finite extension of ℚ_p · The Kronecker–Weber theorem · The Kummer case of the second fundamental inequality · The finite level of the generator theorem (NSW, proof of (7.4.1))

TheoremThe Kummer case of global existence (Milne VII, Lemma 9.3)#

Let K be a number field containing the p-th roots of unity for a prime p. Every open subgroup of the idele class group C_K containing the p-th powers is the norm subgroup of a finite abelian extension of K.

TauCeti.ClassFieldTheory.exists_abelianLayer_globalNormSubgroup_eq_of_pow_mem {K : Type} [Field K]
  [NumberField K] {p : ℕ} [Fact (Nat.Prime p)] [HasEnoughRootsOfUnity K p]
  {N : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)} (hN : IsOpen ↑N)
  (hpow : ∀ (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K), c ^ p ∈ N) :
  ∃ V, V.IsAbelianClassFieldLayer ∧ TauCeti.ClassFieldTheory.globalNormSubgroup K V = N

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.exists_abelianLayer_globalNormSubgroup_eq_of_pow_mem.

Sources

LeanTauCeti.ClassFieldTheory.exists_abelianLayer_globalNormSubgroup_eq_of_pow_mem

Uses 19 · Used by 1

Proof usesArtin's theorem · Corestriction through Shapiro's lemma · Dedekind's bound · The Galois action on the semi-local decomposition · The global class formation · Hensel's lemma for the norm · The local class formation · The norm index theorem · 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 · 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

Used byGlobal existence (Milne VII, Theorem 9.5)

TheoremThe idelic consequence of Furtwängler's theorem #

If Lay represents L/F and E is its maximal abelian subextension, every idele class of F, extended to E, is a norm from L. The field E is pinned as the fixed field of the preimage of the commutator subgroup of the finite Galois group; no norm or principalization hypothesis is assumed.

TauCeti.ClassFieldTheory.ideleClassExtension_mem_range_ideleClassNormMap_commutator {K : Type}
  [Field K] [NumberField K] {F E L : IntermediateField K (SeparableClosure K)} [NumberField ↥F]
  [NumberField ↥E] [NumberField ↥L] [Algebra ↥F ↥E] [IsScalarTower (↥F) (↥E) (SeparableClosure K)]
  [Algebra ↥E ↥L] [IsScalarTower (↥E) (↥L) (SeparableClosure K)]
  (Lay : TauCeti.ClassFieldTheory.NormalLayer (TauCeti.AbsoluteGaloisGroup K))
  (hF : IntermediateField.fixedField ↑Lay.ground = F)
  (hE : IntermediateField.fixedField ↑(Lay.subgroupLayer (commutator Lay.Gal)).ground = E)
  (hL : IntermediateField.fixedField ↑Lay.top = L)
  (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers ↥F) ↥F) :
  (TauCeti.GlobalNumberFields.ideleClassExtension ↥F ↥E) c ∈
    (↑(TauCeti.GlobalNumberFields.ideleClassNormMap ↥E ↥L)).range

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.ideleClassExtension_mem_range_ideleClassNormMap_commutator.

Sources

LeanTauCeti.ClassFieldTheory.ideleClassExtension_mem_range_ideleClassNormMap_commutator

Uses 4

Proof usesThe global class formation · The principal ideal theorem for a class formation · The semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w · TauCeti.algebraicExtensionNormedField

DefinitionTauCeti.ClassFieldTheory.tateTheorem #

Tate's theorem (J. Tate, The higher dimensional cohomology groups of class field theory, Ann. of Math. 56 (1952); Artin–Tate, Chapter XIV §4), with its hypotheses stated one by one over the finite quotient system H ↦ L.subgroupLayer H:

h1: H¹(H, A^V) = 0 for every subgroup H ≤ U/V;
hcard: H²(H, A^V) has exactly #H elements;
hgen: the restriction of u to the layer of H generates that layer's H².

Then cup product with u is an isomorphism H^r(U/V, ℤ) ≃ H^{r+2}(U/V, A^V) in every integer degree r; its underlying homomorphism is cupClass F L u r (tateTheorem_toAddMonoidHom).

TauCeti.ClassFieldTheory.tateTheorem {G : Type} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
  (F : TauCeti.ClassFieldTheory.Formation G) (L : TauCeti.ClassFieldTheory.NormalLayer G)
  (u : ↑(L.H F 2)) (h1 : ∀ (H : Subgroup L.Gal), Subsingleton ↑((L.subgroupLayer H).H F 1))
  (hcard : ∀ (H : Subgroup L.Gal), Nat.card ↑((L.subgroupLayer H).H F 2) = Nat.card ↥H)
  (hgen :
    ∀ (H : Subgroup L.Gal) (x : ↑((L.subgroupLayer H).H F 2)),
      ∃ m, x = m • (CategoryTheory.ConcreteCategory.hom (⋯.cohomologyRes F 2)) u)
  (r : ℤ) : ↑(L.TrivialTateH r) ≃+ ↑(L.TateH F (r + 2))

Lean

Formalized in Tau Ceti as TauCeti.ClassFieldTheory.tateTheorem.

Sources

LeanTauCeti.ClassFieldTheory.tateTheorem

Uses 3 · Used by 14

Proof usesCorestriction through Shapiro's lemma · Restriction through Shapiro's lemma · Tate's theorem

Used byHilbert reciprocity · Local reciprocity for the Weil group · Tate's theorem for a class formation, in every integer degree · The global class formation · The global invariant · The global invariant is injective · The Kummer case of global existence (Milne VII, Lemma 9.3) · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · Local reciprocity for A(L) · The cyclotomic normalization of the local Artin map of a finite extension of ℚ_p · Global existence (Milne VII, Theorem 9.5) · The Kronecker–Weber theorem · The principal ideal theorem for a class formation · The finite level of the generator theorem (NSW, proof of (7.4.1))

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Class field theory

DefinitionTate's theorem for a class formation, in every integer degree#

Lean

Sources

DefinitionLocal reciprocity for the Weil group#

Lean

Sources

DefinitionFinite global reciprocity#

Lean

Sources

TheoremThe norm index theorem#

Lean

Sources

TheoremHilbert reciprocity#

Lean

Sources

TheoremQuadratic reciprocity is Hilbert reciprocity for two odd primes#

Lean

Sources

DefinitionThe global invariant#

Lean

Sources

TheoremThe global invariant is injective#

Lean

Sources

DefinitionThe global class formation#

Lean

Sources

DefinitionThe local invariant#

Lean

Sources

DefinitionThe local class formation#

Lean

Sources

TheoremThe Kummer case of global existence (Milne VII, Lemma 9.3)#

Lean

Sources

TheoremThe idelic consequence of Furtwängler's theorem#

Lean

Sources

DefinitionTauCeti.ClassFieldTheory.tateTheorem#

Lean

Sources

DefinitionTate's theorem for a class formation, in every integer degree #

DefinitionLocal reciprocity for the Weil group #

DefinitionFinite global reciprocity #

TheoremThe norm index theorem #

TheoremHilbert reciprocity #

TheoremQuadratic reciprocity is Hilbert reciprocity for two odd primes #

DefinitionThe global invariant #

TheoremThe global invariant is injective #

DefinitionThe global class formation #

DefinitionThe local invariant #

DefinitionThe local class formation #

TheoremThe idelic consequence of Furtwängler's theorem #

DefinitionTauCeti.ClassFieldTheory.tateTheorem #