Module

CyclicIdeleClassNormIndex.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.CyclicIdeleClassNormIndex

27 declarations indexed from sourceView source ↗

Module documentation

The global class-field axiom

This file proves the cyclic idele-class norm-index formula. The first input is the H⁻¹ calculation for the principal-idele term in

1 → Lˣ → I_L → C_L → 1.

For a cyclic extension this term vanishes by Hilbert 90. The result below is transported through the actual low-degree Tate comparison and then through the equivariant identification of Lˣ with the subgroup of principal relative ideles.

Imports19

Imported by7

theorem

herbrandH0_pow_card_eq_one

L54 ↗

GlobalClassFieldTheory.ClassFieldAxiom.herbrandH0_pow_card_eq_one

Documentation

Every degree-zero Tate class is annihilated by the order of the acting group. For a fixed representative a, its group norm is a ^ |G|. This exponent observation drives the prime-degree descent step.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand

Lean source · statement

theorem herbrandH0_pow_card_eq_one
    {G A : Type}
    [Group G] [Fintype G]
    [CommGroup A] [MulDistribMulAction G A]
    (q : HerbrandH0 G A) :
    q ^ Fintype.card G = 1

theorem

ideleClassHerbrandH0_pow_finrank_eq_one

L80 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ideleClassHerbrandH0_pow_finrank_eq_one

Documentation

Specialization of the exponent calculation to the actual relative idele class group.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand

Lean source · full declaration

theorem ideleClassHerbrandH0_pow_finrank_eq_one
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (q :
      letI :=
        RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
      HerbrandH0 (L ≃ₐ[K] L)
        (RelativeIdeleGroup.ClassGroup K L)) :
    letI :=
      RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
    q ^ Module.finrank K L = 1 := by
  let :=
    RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
  rw [← IsGalois.card_aut_eq_finrank,
    Nat.card_eq_fintype_card]
  exact herbrandH0_pow_card_eq_one q

instance

cyclicNormBase_isMulCommutative

L101 ↗

GlobalClassFieldTheory.ClassFieldAxiom.cyclicNormBase_isMulCommutative

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity

Lean source · statement

instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A)

theorem

ideleClassNormQuotient_pow_finrank_eq_one

L108 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ideleClassNormQuotient_pow_finrank_eq_one

Documentation

The concrete class-norm quotient C_K / N C_L has exponent dividing [L:K].

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNormQuotient_pow_finrank_eq_one
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (q : RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient K L) :
    q ^ Module.finrank K L = 1

theorem

pow_injective_of_exponent_of_coprime

L128 ↗

GlobalClassFieldTheory.ClassFieldAxiom.pow_injective_of_exponent_of_coprime

Documentation

If a commutative group has exponent dividing p, then every d-power map with d coprime to p is injective. In the prime-degree argument, p is the extension degree and d is the roots-of-unity base-change degree.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · full declaration

theorem pow_injective_of_exponent_of_coprime
    {A : Type} [CommGroup A]
    (p d : ℕ)
    (hexponent : ∀ x : A, x ^ p = 1)
    (hcoprime : d.Coprime p) :
    Function.Injective (fun x : A => x ^ d) := by
  intro x y hxy
  change x ^ d = y ^ d at hxy
  have hdpow : (x * y⁻¹) ^ d = 1 := by
    calc
      (x * y⁻¹) ^ d = x ^ d * (y ^ d)⁻¹ := by
        rw [mul_pow, inv_pow]
      _ = 1 := by rw [hxy, mul_inv_cancel]
  have horder_d : orderOf (x * y⁻¹) ∣ d :=
    orderOf_dvd_of_pow_eq_one hdpow
  have horder_p : orderOf (x * y⁻¹) ∣ p :=
    orderOf_dvd_of_pow_eq_one (hexponent (x * y⁻¹))
  have horder_gcd :
      orderOf (x * y⁻¹) ∣ Nat.gcd d p :=
    Nat.dvd_gcd horder_d horder_p
  rw [hcoprime.gcd_eq_one] at horder_gcd
  have hxy_one : x * y⁻¹ = 1 :=
    orderOf_eq_one_iff.mp (Nat.dvd_one.mp horder_gcd)
  exact mul_inv_eq_one.mp hxy_one

theorem

ideleClassNormQuotient_pow_injective_of_coprime

L155 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ideleClassNormQuotient_pow_injective_of_coprime

Documentation

On the actual class-norm quotient, every power coprime to the extension degree is injective.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · full declaration

theorem ideleClassNormQuotient_pow_injective_of_coprime
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (d : ℕ)
    (hd : d.Coprime (Module.finrank K L)) :
    Function.Injective
      (fun q : RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient K L => q ^ d) := by
  let :=
    RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
  let e :=
    RelativeIdeleGroup.Cohomology.ideleClassHerbrandH0EquivNormQuotient K L
  have hpow :
      Function.Injective
        (fun x : HerbrandH0 (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L) =>
          x ^ d) :=
    pow_injective_of_exponent_of_coprime
      (A := HerbrandH0 (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L))
      (Module.finrank K L) d
      (ideleClassHerbrandH0_pow_finrank_eq_one K L) hd
  intro x y hxy
  apply e.symm.injective
  apply hpow
  exact
    ((map_pow e.symm x d).symm.trans (congrArg e.symm hxy)).trans
      (map_pow e.symm y d)

theorem

pushoutNormQuotientMap_injective_of_coprime

L191 ↗

GlobalClassFieldTheory.ClassFieldAxiom.pushoutNormQuotientMap_injective_of_coprime

Documentation

Source-producing form of the roots-of-unity base-change step. For a pushout square N = M ⊗[K] L, if [M:K] is coprime to [L:K], the induced map

C_K / N_{L/K}C_L → C_M / N_{N/M}C_N

is injective. The target is expressed in the fixed-bottom-field tower model, so no unproved identification 𝔸_K ⊗_K M ≃ 𝔸_M is assumed.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem pushoutNormQuotientMap_injective_of_coprime
    (K M L N : Type)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]
    [IsGalois K L]
    (hcoprime :
      (Module.finrank K M).Coprime
        (Module.finrank K L)) :
    Function.Injective
      (pushoutNormQuotientMap K M L N)

instance

cyclicNormRelative_isMulCommutative

L216 ↗

GlobalClassFieldTheory.ClassFieldAxiom.cyclicNormRelative_isMulCommutative

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IntermediateNormQuotientCommutativity

Lean source · statement

instance cyclicNormRelative_isMulCommutative
    (A B : Type) [Field A] [NumberField A] [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B)

def

actualPushoutNormQuotientMap

L226 ↗

GlobalClassFieldTheory.ClassFieldAxiom.actualPushoutNormQuotientMap

Documentation

The pushout map with its target changed from the fixed-bottom tower presentation to the actual norm quotient C_M / N_{N/M} C_N.

Only the Galois hypothesis on the auxiliary extension M/K is needed for this last comparison.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IntermediateNormQuotientCommutativity
local instance cyclicNormRelative_isMulCommutative
    (A B : Type) [Field A] [NumberField A] [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def actualPushoutNormQuotientMap
    (K M L N : Type)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]
    [IsGalois K M] :
    RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient K L →
      RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient M N

theorem

actualPushoutNormQuotientMap_mk

L248 ↗

GlobalClassFieldTheory.ClassFieldAxiom.actualPushoutNormQuotientMap_mk

Documentation

The actual pushout norm-quotient map sends a quotient representative to the corresponding base-changed representative.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IntermediateNormQuotientCommutativity
local instance cyclicNormRelative_isMulCommutative
    (A B : Type) [Field A] [NumberField A] [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem actualPushoutNormQuotientMap_mk
    (K M L N : Type)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]
    [IsGalois K M]
    (c : IdeleClassGroup K) :
    actualPushoutNormQuotientMap K M L N
        (QuotientGroup.mk'
          (RelativeIdeleGroup.Cohomology.ideleClassNorm K L).range c) =
      QuotientGroup.mk'
        (RelativeIdeleGroup.Cohomology.ideleClassNorm M N).range
        (_root_.relativeIdeleClassBaseChangeMulEquiv
          (K := K) (L := M)
          (RelativeIdeleGroup.classInclusion K M c))

theorem

actualPushoutNormQuotientMap_injective_of_coprime

L286 ↗

GlobalClassFieldTheory.ClassFieldAxiom.actualPushoutNormQuotientMap_injective_of_coprime

Documentation

Actual-target form of the injective roots-of-unity base-change step.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IntermediateNormQuotientCommutativity
local instance cyclicNormRelative_isMulCommutative
    (A B : Type) [Field A] [NumberField A] [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem actualPushoutNormQuotientMap_injective_of_coprime
    (K M L N : Type)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]
    [IsGalois K L] [IsGalois K M]
    (hcoprime :
      (Module.finrank K M).Coprime
        (Module.finrank K L)) :
    Function.Injective
      (actualPushoutNormQuotientMap K M L N)

theorem

ideleClassNormQuotient_card_le_actualPushout

L314 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ideleClassNormQuotient_card_le_actualPushout

Documentation

Cardinal consequence with the actual N/M norm quotient as target.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IntermediateNormQuotientCommutativity
local instance cyclicNormRelative_isMulCommutative
    (A B : Type) [Field A] [NumberField A] [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNormQuotient_card_le_actualPushout
    (K M L N : Type)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]
    [IsGalois K L] [IsGalois K M]
    [Finite (RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient M N)]
    (hcoprime :
      (Module.finrank K M).Coprime
        (Module.finrank K L)) :
    Nat.card (RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient K L) ≤
      Nat.card (RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient M N)

theorem

ideleClassNorm_index_le_prime_of_finrank_eq

L342 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ideleClassNorm_index_le_prime_of_finrank_eq

Documentation

Prime-degree upper bound. After adjoining the p-th roots of unity, the prime-power Kummer calculation gives norm index p for the concrete cyclotomic pushout. Coprimality of the cyclotomic degree then makes the actual pushout map on norm quotients injective.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IntermediateNormQuotientCommutativity
local instance cyclicNormRelative_isMulCommutative
    (A B : Type) [Field A] [NumberField A] [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNorm_index_le_prime_of_finrank_eq
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (p : ℕ) (hp : p.Prime)
    (hdegree : Module.finrank K L = p) :
    (RelativeIdeleGroup.Cohomology.ideleClassNorm K L).range.index ≤ p

theorem

ideleClassNormQuotient_card_le_actual_tower_mul

L414 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ideleClassNormQuotient_card_le_actual_tower_mul

Documentation

Actual tower form of the cardinal bound:

#(C_K / N_{L/K}C_L) ≤ #(C_M / N_{L/M}C_L) · #(C_K / N_{M/K}C_M).

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IntermediateNormQuotientCommutativity
local instance cyclicNormRelative_isMulCommutative
    (A B : Type) [Field A] [NumberField A] [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNormQuotient_card_le_actual_tower_mul
    (K M L : Type)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M]
    [Finite (RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient M L)]
    [Finite (RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient K M)] :
    Nat.card (RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient K L) ≤
      Nat.card (RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient M L) *
        Nat.card (RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient K M)

theorem

relativeIdeleClassNorm_index_eq_finrank_cyclic

L465 ↗

GlobalClassFieldTheory.ClassFieldAxiom.relativeIdeleClassNorm_index_eq_finrank_cyclic

Documentation

Relative-coordinate source for the norm-index calculation.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem relativeIdeleClassNorm_index_eq_finrank_cyclic
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)] :
    (RelativeIdeleGroup.Cohomology.ideleClassNorm K L).range.index =
      Module.finrank K L

theorem

ideleClassNorm_index_eq_finrank_cyclic

L623 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ideleClassNorm_index_eq_finrank_cyclic

Documentation

The ordinary idele-class norm has index equal to the degree for every finite cyclic extension.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNorm_index_eq_finrank_cyclic
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)] :
    (_root_.ideleClassNorm K L).range.index =
      Module.finrank K L

theorem

relativeIdeleClassNormQuotient_finite_of_actual_tower

L637 ↗

GlobalClassFieldTheory.ClassFieldAxiom.relativeIdeleClassNormQuotient_finite_of_actual_tower

Documentation

Finiteness propagation through the actual tower norm-quotient sequence.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem relativeIdeleClassNormQuotient_finite_of_actual_tower
    (K M L : Type)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M]
    [Finite (RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient M L)]
    [Finite (RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient K M)] :
    Finite (RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient K L)

theorem

relativeIdeleClassNormQuotient_finite_and_card_le_finrank_abelian

L695 ↗

GlobalClassFieldTheory.ClassFieldAxiom.relativeIdeleClassNormQuotient_finite_and_card_le_finrank_abelian

Documentation

The relative-coordinate presentation of the idele-class norm quotient is finite and has cardinality at most the extension degree for every finite abelian Galois extension.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    relativeIdeleClassNormQuotient_finite_and_card_le_finrank_abelian
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    Finite (RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient K L) ∧
      Nat.card (RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient K L) ≤
        Module.finrank K L

theorem

ideleClassNormQuotient_finite_abelian

L825 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ideleClassNormQuotient_finite_abelian

Documentation

Finiteness of the actual ordinary idele-class norm quotient of a finite abelian Galois extension.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNormQuotient_finite_abelian
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    Finite
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)

theorem

ideleClassNormQuotient_card_le_finrank_abelian

L841 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ideleClassNormQuotient_card_le_finrank_abelian

Documentation

Degree upper bound for the cardinality of the actual ordinary idele-class norm quotient of a finite abelian Galois extension.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNormQuotient_card_le_finrank_abelian
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    Nat.card
        (IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K L).range) ≤
      Module.finrank K L

theorem

ideleClass_lowDegree_card_eq_finrank_cyclic

L860 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ideleClass_lowDegree_card_eq_finrank_cyclic

Documentation

The cardinalities of the actual Herbrand models of the low Tate groups for a finite cyclic extension. The canonical Herbrand support gives the Herbrand quotient |G|; the norm-index theorem supplies the matching upper bound for H⁰, so the standard low-degree cardinal lemma forces H⁻¹ to have one element.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · full declaration

theorem ideleClass_lowDegree_card_eq_finrank_cyclic
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (sigma : L ≃ₐ[K] L)
    (hsigma :
      ∀ tau : L ≃ₐ[K] L,
        tau ∈ Subgroup.zpowers sigma) :
    letI :=
      RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
    Nat.card
          (HerbrandH0 (L ≃ₐ[K] L)
            (RelativeIdeleGroup.ClassGroup K L)) =
        Module.finrank K L ∧
      Nat.card
          (HerbrandHMinusOne (L ≃ₐ[K] L)
            (RelativeIdeleGroup.ClassGroup K L) sigma) =
        1 := by
  let :=
    RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
  let : IsCyclic (L ≃ₐ[K] L) :=
    ⟨⟨sigma, hsigma⟩⟩
  obtain ⟨hC, hCvalue⟩ :=
    Cohomology.ideleClass_herbrandQuotient_eq_card_of_supported_local_calculation
      (K := K) (L := L)
      (_root_.ideleClassHerbrandSupport
        (K := K) (L := L))
      sigma hsigma
      (_root_.relativeSupportedAboveHerbrandSupport_sup_principal_eq_top
        (K := K) (L := L))
      (Cohomology.chosenFinitePlaceIsUnramified_of_notMem_ideleClassHerbrandSupport
        (K := K) (L := L))
  let :
      Finite
        (HerbrandH0 (L ≃ₐ[K] L)
          (RelativeIdeleGroup.ClassGroup K L)) :=
    hC.1
  let :
      Finite
        (HerbrandHMinusOne (L ≃ₐ[K] L)
          (RelativeIdeleGroup.ClassGroup K L) sigma) :=
    hC.2
  have hQuotient :
      herbrandQuotient
          (G := L ≃ₐ[K] L)
          (A := RelativeIdeleGroup.ClassGroup K L)
          sigma =
        (Module.finrank K L : ℚ) := by
    simpa only [Fintype.card_eq_nat_card,
      IsGalois.card_aut_eq_finrank K L] using
      hCvalue
  have hH0 :
      Nat.card
          (HerbrandH0 (L ≃ₐ[K] L)
            (RelativeIdeleGroup.ClassGroup K L)) =
        Module.finrank K L := by
    calc
      Nat.card
            (HerbrandH0 (L ≃ₐ[K] L)
              (RelativeIdeleGroup.ClassGroup K L)) =
          (RelativeIdeleGroup.Cohomology.ideleClassNorm K L).range.index :=
        (RelativeIdeleGroup.Cohomology.ideleClassNorm_index_eq_herbrandH0_card
          K L).symm
      _ = Module.finrank K L :=
        relativeIdeleClassNorm_index_eq_finrank_cyclic K L
  exact
    CyclicCohomology.lowDegree_card_eq_of_herbrandQuotient_eq_nat_of_le
      sigma (Module.finrank K L) Module.finrank_pos
      hQuotient hH0.le

theorem

ideleClass_tate_lowDegree_finite_card_eq_finrank_cyclic

L933 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ideleClass_tate_lowDegree_finite_card_eq_finrank_cyclic

Documentation

Finiteness and cardinalities of the actual low-degree Tate cohomology groups of the relative idele class representation.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · full declaration

theorem ideleClass_tate_lowDegree_finite_card_eq_finrank_cyclic
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (sigma : L ≃ₐ[K] L)
    (hsigma :
      ∀ tau : L ≃ₐ[K] L,
        tau ∈ Subgroup.zpowers sigma) :
    letI :=
      RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
    Finite
          (tateCohomology
            (Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
              (RelativeIdeleGroup.ClassGroup K L)) 0) ∧
      Finite
          (tateCohomology
            (Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
              (RelativeIdeleGroup.ClassGroup K L)) (-1)) ∧
      Nat.card
          (tateCohomology
            (Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
              (RelativeIdeleGroup.ClassGroup K L)) 0) =
        Module.finrank K L ∧
      Nat.card
          (tateCohomology
            (Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
              (RelativeIdeleGroup.ClassGroup K L)) (-1)) =
        1 := by
  let :=
    RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
  have hHerbrand :=
    ideleClass_lowDegree_card_eq_finrank_cyclic
      K L sigma hsigma
  let :
      Finite
        (HerbrandH0 (L ≃ₐ[K] L)
          (RelativeIdeleGroup.ClassGroup K L)) :=
    Nat.finite_of_card_ne_zero (by
      rw [hHerbrand.1]
      exact Nat.ne_of_gt Module.finrank_pos)
  let :
      Finite
        (HerbrandHMinusOne (L ≃ₐ[K] L)
          (RelativeIdeleGroup.ClassGroup K L) sigma) :=
    Nat.finite_of_card_ne_zero (by
      rw [hHerbrand.2]
      exact one_ne_zero)
  let e0 :
      tateCohomology
          (Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
            (RelativeIdeleGroup.ClassGroup K L)) 0 ≃
        Additive
          (HerbrandH0 (L ≃ₐ[K] L)
            (RelativeIdeleGroup.ClassGroup K L)) :=
    (tateH0IsoHerbrandH0
      (G := L ≃ₐ[K] L)
      (A := RelativeIdeleGroup.ClassGroup K L)).toLinearEquiv.toEquiv
  let em :
      tateCohomology
          (Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
            (RelativeIdeleGroup.ClassGroup K L)) (-1) ≃
        Additive
          (HerbrandHMinusOne (L ≃ₐ[K] L)
            (RelativeIdeleGroup.ClassGroup K L) sigma) :=
    (tateHMinusOneIsoHerbrandHMinusOne
      (G := L ≃ₐ[K] L)
      (A := RelativeIdeleGroup.ClassGroup K L)
      sigma hsigma).toLinearEquiv.toEquiv
  let :
      Finite
        (tateCohomology
          (Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
            (RelativeIdeleGroup.ClassGroup K L)) 0) :=
    Finite.of_injective e0 e0.injective
  let :
      Finite
        (tateCohomology
          (Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
            (RelativeIdeleGroup.ClassGroup K L)) (-1)) :=
    Finite.of_injective em em.injective
  refine ⟨inferInstance, inferInstance, ?_, ?_⟩
  · calc
      Nat.card
            (tateCohomology
              (Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
                (RelativeIdeleGroup.ClassGroup K L)) 0) =
          Nat.card
            (Additive
              (HerbrandH0 (L ≃ₐ[K] L)
                (RelativeIdeleGroup.ClassGroup K L))) :=
        Nat.card_congr e0
      _ = Module.finrank K L := by
        change
          Nat.card
              (HerbrandH0 (L ≃ₐ[K] L)
                (RelativeIdeleGroup.ClassGroup K L)) =
            Module.finrank K L
        exact hHerbrand.1
  · calc
      Nat.card
            (tateCohomology
              (Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
                (RelativeIdeleGroup.ClassGroup K L)) (-1)) =
          Nat.card
            (Additive
              (HerbrandHMinusOne (L ≃ₐ[K] L)
                (RelativeIdeleGroup.ClassGroup K L) sigma)) :=
        Nat.card_congr em
      _ = 1 := by
        change
          Nat.card
              (HerbrandHMinusOne (L ≃ₐ[K] L)
                (RelativeIdeleGroup.ClassGroup K L) sigma) =
            1
        exact hHerbrand.2

theorem

ideleClass_tateHMinusOne_subsingleton_cyclic

L1052 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ideleClass_tateHMinusOne_subsingleton_cyclic

Documentation

The degree-minus-one vanishing conclusion in the exact multiplicative form consumed by the Hasse norm principle.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · full declaration

theorem ideleClass_tateHMinusOne_subsingleton_cyclic
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (sigma : L ≃ₐ[K] L)
    (hsigma :
      ∀ tau : L ≃ₐ[K] L,
        tau ∈ Subgroup.zpowers sigma) :
    letI :=
      RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
    Subsingleton
      (Multiplicative
        (tateCohomology
          (Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
            (RelativeIdeleGroup.ClassGroup K L)) (-1))) := by
  let :=
    RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
  have h :=
    ideleClass_tate_lowDegree_finite_card_eq_finrank_cyclic
      K L sigma hsigma
  change
    Subsingleton
      (tateCohomology
        (Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
          (RelativeIdeleGroup.ClassGroup K L)) (-1))
  exact (Nat.card_eq_one_iff_unique.mp h.2.2.2).1

theorem

fieldUnitsHerbrandHMinusOne_subsingleton

L1082 ↗

GlobalClassFieldTheory.ClassFieldAxiom.fieldUnitsHerbrandHMinusOne_subsingleton

Documentation

Hilbert 90 makes the actual multiplicative H⁻¹(G,Lˣ) a subsingleton for a supplied cyclic generator.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · full declaration

theorem fieldUnitsHerbrandHMinusOne_subsingleton
    (K L : Type)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (σ : L ≃ₐ[K] L)
    (hσ : ∀ τ : L ≃ₐ[K] L, τ ∈ Subgroup.zpowers σ) :
    letI :=
      LocalClassFieldTheory.galoisGroupFieldUnitsMulDistribMulAction K L
    Subsingleton (HerbrandHMinusOne (L ≃ₐ[K] L) Lˣ σ) := by
  let :=
    LocalClassFieldTheory.galoisGroupFieldUnitsMulDistribMulAction K L
  let e :=
    LocalClassFieldTheory.herbrandHminusOneEquivUnitsTateHminusOne
      K L σ hσ
  constructor
  intro x y
  apply e.injective
  have hTateSubsingleton :
      Subsingleton
        (tateCohomology
          (Rep.ofAlgebraAutOnUnits K L) (-1)) :=
    (Nat.card_eq_one_iff_unique.mp
      (LocalClassFieldTheory.unitsTateHminusOne_card_eq_one
        K L σ hσ)).1
  exact hTateSubsingleton.elim (e x) (e y)

theorem

fieldUnitsHerbrandHMinusOne_card_eq_one

L1109 ↗

GlobalClassFieldTheory.ClassFieldAxiom.fieldUnitsHerbrandHMinusOne_card_eq_one

Documentation

Cardinal form of the Hilbert-90 calculation.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · full declaration

theorem fieldUnitsHerbrandHMinusOne_card_eq_one
    (K L : Type)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (σ : L ≃ₐ[K] L)
    (hσ : ∀ τ : L ≃ₐ[K] L, τ ∈ Subgroup.zpowers σ) :
    letI :=
      LocalClassFieldTheory.galoisGroupFieldUnitsMulDistribMulAction K L
    Nat.card (HerbrandHMinusOne (L ≃ₐ[K] L) Lˣ σ) = 1 := by
  let :=
    LocalClassFieldTheory.galoisGroupFieldUnitsMulDistribMulAction K L
  let :
      Subsingleton
        (HerbrandHMinusOne (L ≃ₐ[K] L) Lˣ σ) :=
    fieldUnitsHerbrandHMinusOne_subsingleton K L σ hσ
  exact Nat.card_eq_one_iff_unique.mpr
    ⟨inferInstance, ⟨1⟩⟩

theorem

principalIdelesHerbrandHMinusOne_subsingleton

L1129 ↗

GlobalClassFieldTheory.ClassFieldAxiom.principalIdelesHerbrandHMinusOne_subsingleton

Documentation

Transport Hilbert 90 from field units to the actual subgroup of principal relative ideles.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · full declaration

theorem principalIdelesHerbrandHMinusOne_subsingleton
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (σ : L ≃ₐ[K] L)
    (hσ : ∀ τ : L ≃ₐ[K] L, τ ∈ Subgroup.zpowers σ) :
    letI :=
      LocalClassFieldTheory.galoisGroupFieldUnitsMulDistribMulAction K L
    letI :=
      RelativeIdeleGroup.Cohomology.relativeIdeleMulDistribMulAction K L
    letI :=
      RelativeIdeleGroup.Cohomology.principalIdeleMulDistribMulAction K L
    Subsingleton
      (HerbrandHMinusOne (L ≃ₐ[K] L)
        (RelativeIdeleGroup.principalSubgroup K L) σ) := by
  let :=
    LocalClassFieldTheory.galoisGroupFieldUnitsMulDistribMulAction K L
  let :=
    RelativeIdeleGroup.Cohomology.relativeIdeleMulDistribMulAction K L
  let :=
    RelativeIdeleGroup.Cohomology.principalIdeleMulDistribMulAction K L
  let e :=
    fieldUnitsHerbrandHMinusOneEquivPrincipalIdeles
      K L σ
  let :
      Subsingleton
        (HerbrandHMinusOne (L ≃ₐ[K] L) Lˣ σ) :=
    fieldUnitsHerbrandHMinusOne_subsingleton K L σ hσ
  constructor
  intro x y
  apply e.symm.injective
  exact Subsingleton.elim (e.symm x) (e.symm y)

theorem

principalIdelesHerbrandHMinusOne_card_eq_one

L1165 ↗

GlobalClassFieldTheory.ClassFieldAxiom.principalIdelesHerbrandHMinusOne_card_eq_one

Documentation

Cardinal form for the principal-idele term in the class-group exact sequence.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
section NormQuotientCommutativity
local instance cyclicNormBase_isMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · full declaration

theorem principalIdelesHerbrandHMinusOne_card_eq_one
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (σ : L ≃ₐ[K] L)
    (hσ : ∀ τ : L ≃ₐ[K] L, τ ∈ Subgroup.zpowers σ) :
    letI :=
      RelativeIdeleGroup.Cohomology.relativeIdeleMulDistribMulAction K L
    letI :=
      RelativeIdeleGroup.Cohomology.principalIdeleMulDistribMulAction K L
    Nat.card
      (HerbrandHMinusOne (L ≃ₐ[K] L)
        (RelativeIdeleGroup.principalSubgroup K L) σ) = 1 := by
  let :=
    LocalClassFieldTheory.galoisGroupFieldUnitsMulDistribMulAction K L
  let :=
    RelativeIdeleGroup.Cohomology.relativeIdeleMulDistribMulAction K L
  let :=
    RelativeIdeleGroup.Cohomology.principalIdeleMulDistribMulAction K L
  let :
      Subsingleton
        (HerbrandHMinusOne (L ≃ₐ[K] L)
          (RelativeIdeleGroup.principalSubgroup K L) σ) :=
    principalIdelesHerbrandHMinusOne_subsingleton K L σ hσ
  exact Nat.card_eq_one_iff_unique.mpr
    ⟨inferInstance, ⟨1⟩⟩

Module documentation

The global class-field axiom

Declarations