NYLL
Module

MathlibFrobeniusHilbertComparison.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.MathlibFrobeniusHilbertComparison
31 declarations indexed from sourceView source ↗

Module documentation

Frobenius and Hilbert class fields implementation

This module supplies the implementation proofs for the compact public statements in ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.

The prime element exposed below is the arithmetic-normalized prime Artin element. Its residue action identifies it with Mathlib's arithmetic Frobenius at every unramified finite prime.

Imports30
Imported by12

Declarations

theorem

chosenFinitePlaceIsUnramified_of_isUnramifiedIn

L74 ↗
ClassFieldTheory.GlobalClassFieldComparison.chosenFinitePlaceIsUnramified_of_isUnramifiedIn
Documentation

Convert Mathlib's ideal-theoretic unramifiedness of a base prime into the chosen-completion formulation used by the current Artin implementation.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section PrimeArtin
open scoped Pointwise
open AlgebraicNumberTheory.Valuations
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem chosenFinitePlaceIsUnramified_of_isUnramifiedIn
    (v : HeightOneSpectrum (𝓞 K))
    (hunram : Algebra.IsUnramifiedIn (𝓞 L) v.asIdeal) :
    _root_.ChosenFinitePlaceIsUnramified
      (K := K) (L := L) v
theorem

arithmeticPrimeArtin_eq_inverse

L94 ↗
ClassFieldTheory.GlobalClassFieldComparison.arithmeticPrimeArtin_eq_inverse
Documentation

The arithmetic-normalized prime Artin element is the inverse of the geometric-normalized prime Artin element. This fixes the relation between the two reciprocity conventions.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section PrimeArtin
open scoped Pointwise
open AlgebraicNumberTheory.Valuations
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem arithmeticPrimeArtin_eq_inverse
    (v : HeightOneSpectrum (𝓞 K)) :
    GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
          (K := K) (L := L) v =
      (GlobalClassFieldTheory.GlobalClassFields.finitePlacePrimeArtin
          (K := K) (L := L) v)⁻¹
theorem

arithmeticPrimeArtin_stabilizes_chosenPrime

L106 ↗
ClassFieldTheory.GlobalClassFieldComparison.arithmeticPrimeArtin_stabilizes_chosenPrime
Documentation

The arithmetic prime Artin element preserves the chosen prime above the base prime. This is the decomposition-group part of its Frobenius property; the residue-field congruence is a separate comparison.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section PrimeArtin
open scoped Pointwise
open AlgebraicNumberTheory.Valuations
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · full declaration
theorem arithmeticPrimeArtin_stabilizes_chosenPrime
    (v : HeightOneSpectrum (𝓞 K)) :
    let w := chosenFinitePlaceExtension (L := L) v
    let W := finitePlaceExtensionCentre (K := K) (L := L) v w
    GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := L) v ∈
      MulAction.stabilizer (L ≃ₐ[K] L) W.asIdeal := by
  let w := chosenFinitePlaceExtension (L := L) v
  let W := finitePlaceExtensionCentre (K := K) (L := L) v w
  let σ := GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
    (K := K) (L := L) v
  have hgeo :
      GlobalClassFieldTheory.GlobalClassFields.finitePlacePrimeArtin
          (K := K) (L := L) v ∈
        finitePlaceDecompositionGroup (K := K) (L := L) v := by
    rw [GlobalClassFieldTheory.GlobalClassFields.finitePlacePrimeArtin_eq_chosenFinitePlaceArtin]
    rw [← GlobalClassFieldTheory.Reciprocity.chosenFinitePlaceArtinMonoidHom_range]
    exact ⟨FiniteIdeleGroup.chosenLocalOrderSection v 1, rfl⟩
  have hσ : σ ∈ finitePlaceDecompositionGroup (K := K) (L := L) v := by
    change GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := L) v ∈
      finitePlaceDecompositionGroup (K := K) (L := L) v
    rw [GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin_eq_inv]
    exact Subgroup.inv_mem _ hgeo
  have hσinv : σ⁻¹ ∈ finitePlaceDecompositionGroup (K := K) (L := L) v :=
    Subgroup.inv_mem _ hσ
  have hw :
      absoluteValueExtensionConjugate
          (HeightOneSpectrum.adicAbv K v) w σ⁻¹ = w :=
    (mem_finitePlaceDecompositionGroup_iff v σ⁻¹).mp hσinv
  have hW : finitePlaceEquiv K L σ W = W := by
    have hcentre := finitePlaceExtensionCentre_conjugate
      (K := K) (L := L) v w σ⁻¹
    rw [hw] at hcentre
    simpa only [inv_inv] using hcentre.symm
  have hIdeal := congrArg HeightOneSpectrum.asIdeal hW
  have hIdeal' :
      W.asIdeal.map
          (NumberField.RingOfIntegers.mapAlgEquiv σ).toRingEquiv = W.asIdeal := by
    simpa only [finitePlaceEquiv_asIdeal] using hIdeal
  change σ ∈ MulAction.stabilizer (L ≃ₐ[K] L) W.asIdeal
  rw [MulAction.mem_stabilizer_iff, Ideal.pointwise_smul_def]
  exact hIdeal'
theorem

arithmeticPrimeArtin_stabilizes_prime

L152 ↗
ClassFieldTheory.GlobalClassFieldComparison.arithmeticPrimeArtin_stabilizes_prime
Documentation

In an abelian extension, the arithmetic prime Artin element preserves every prime above the base prime, not only the chosen one.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section PrimeArtin
open scoped Pointwise
open AlgebraicNumberTheory.Valuations
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem arithmeticPrimeArtin_stabilizes_prime
    (v : HeightOneSpectrum (𝓞 K))
    (w : HeightOneSpectrum (𝓞 L))
    (hw : w.asIdeal.LiesOver v.asIdeal) :
    GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := L) v ∈
      MulAction.stabilizer (L ≃ₐ[K] L) w.asIdeal
theorem

orderOf_arithmeticPrimeArtin_eq_inertiaDegree

L191 ↗
ClassFieldTheory.GlobalClassFieldComparison.orderOf_arithmeticPrimeArtin_eq_inertiaDegree
Documentation

At an ideal-theoretically unramified finite prime, the order of the arithmetic-normalized prime Artin element is the common inertia degree of the prime ideals above the base prime.

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section PrimeArtin
open scoped Pointwise
open AlgebraicNumberTheory.Valuations
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
open _root_.GlobalClassFieldTheory.GlobalClassFields
  (orderOf_arithmeticFinitePlacePrimeArtin_eq_finitePlaceLocalDegree_of_chosenUnramified) in
open _root_.GlobalClassFieldTheory.IdealClassFieldTheory
  (finitePlaceLocalDegree_eq_inertiaDegree_of_chosenUnramified) in
Lean source · statement
theorem orderOf_arithmeticPrimeArtin_eq_inertiaDegree
    (v : HeightOneSpectrum (𝓞 K))
    (hunram : Algebra.IsUnramifiedIn (𝓞 L) v.asIdeal) :
    orderOf
        (GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
          (K := K) (L := L) v) =
      Ideal.inertiaDegIn v.asIdeal (𝓞 L)
theorem

arithmeticPrimeArtin_eq_one_iff_splitsCompletely

L218 ↗
ClassFieldTheory.GlobalClassFieldComparison.arithmeticPrimeArtin_eq_one_iff_splitsCompletely
Documentation

At an ideal-theoretically unramified finite prime, the arithmetic-normalized prime Artin element is trivial exactly when the finite place actually splits completely.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section PrimeArtin
open scoped Pointwise
open AlgebraicNumberTheory.Valuations
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
open _root_.GlobalClassFieldTheory.GlobalClassFields
  (arithmeticFinitePlacePrimeArtin_eq_one_iff_splitsCompletely_of_chosenUnramified) in
Lean source · statement
theorem arithmeticPrimeArtin_eq_one_iff_splitsCompletely
    (v : HeightOneSpectrum (𝓞 K))
    (hunram : Algebra.IsUnramifiedIn (𝓞 L) v.asIdeal) :
    GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
          (K := K) (L := L) v =
        1 ↔
      _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v
theorem

orderOf_arithmeticFrobeniusAt_eq_inertiaDegree

L240 ↗
ClassFieldTheory.GlobalClassFieldComparison.orderOf_arithmeticFrobeniusAt_eq_inertiaDegree
Documentation

Mathlib's arithmetic Frobenius has order equal to the residue degree at an unramified prime. The proof compares its residue action with the finite-field Frobenius and uses the decomposition-group cardinality.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section ArithmeticFrobenius
open scoped Pointwise
Lean source · statement
theorem orderOf_arithmeticFrobeniusAt_eq_inertiaDegree
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
    (v : HeightOneSpectrum (𝓞 K))
    (w : HeightOneSpectrum (𝓞 L))
    (hw : w.asIdeal.LiesOver v.asIdeal)
    (hunram : Algebra.IsUnramifiedAt (𝓞 K) w.asIdeal) :
    orderOf (arithmeticFrobeniusAt (K := K) w) =
      w.asIdeal.inertiaDeg (𝓞 K)
theorem

arithmeticFrobeniusAt_eq_of_liesOver

L304 ↗
ClassFieldTheory.GlobalClassFieldComparison.arithmeticFrobeniusAt_eq_of_liesOver
Documentation

In an abelian extension, Mathlib's chosen arithmetic Frobenius is independent of the prime above a fixed base prime. Mathlib chooses conjugate lifts, and conjugacy is equality in the abelian Galois group.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
Lean source · statement
theorem arithmeticFrobeniusAt_eq_of_liesOver
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
    (v : HeightOneSpectrum (𝓞 K))
    (w w' : HeightOneSpectrum (𝓞 L))
    (hw : w.asIdeal.LiesOver v.asIdeal)
    (hw' : w'.asIdeal.LiesOver v.asIdeal) :
    arithmeticFrobeniusAt (K := K) w =
      arithmeticFrobeniusAt (K := K) w'
theorem

arithmeticPrimeArtin_eq_arithmeticFrobeniusAt

L331 ↗
ClassFieldTheory.GlobalClassFieldComparison.arithmeticPrimeArtin_eq_arithmeticFrobeniusAt
Documentation

At an unramified finite prime, the arithmetic-normalized prime Artin element is Mathlib's arithmetic Frobenius, independently of the chosen prime above the base prime.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
open _root_.GlobalClassFieldTheory.GlobalClassFields
  (arithmeticFinitePlacePrimeArtin_eq_chosenFinitePlaceArithmeticFrobenius) in
Lean source · statement
theorem arithmeticPrimeArtin_eq_arithmeticFrobeniusAt
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
    (v : HeightOneSpectrum (𝓞 K))
    (w : HeightOneSpectrum (𝓞 L))
    (hw : w.asIdeal.LiesOver v.asIdeal)
    (hunram : Algebra.IsUnramifiedAt (𝓞 K) w.asIdeal) :
    GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := L) v =
      arithmeticFrobeniusAt (K := K) w
theorem

finitePrimeSplitsCompletely_iff_original

L458 ↗
ClassFieldTheory.GlobalClassFieldComparison.finitePrimeSplitsCompletely_iff_original
Documentation

Ideal-theoretic complete splitting at every prime above a finite place agrees with the decomposition-group definition used by the existing library.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
Lean source · statement
theorem finitePrimeSplitsCompletely_iff_original
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K)) :
    FinitePrimeSplitsCompletely K L v ↔
      _root_.FinitePlaceSplitsCompletely (K := K) (L := L) v
def

bigHilbertClassFieldEmbedding

L522 ↗
ClassFieldTheory.GlobalClassFieldComparison.bigHilbertClassFieldEmbedding
Documentation

Embed the selected big Hilbert class field in the separable closure of its original base field.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def bigHilbertClassFieldEmbedding :
    GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField K →ₐ[K]
      SeparableClosure K
def

bigHilbertClassFieldFiniteAbelianExtension

L529 ↗
ClassFieldTheory.GlobalClassFieldComparison.bigHilbertClassFieldFiniteAbelianExtension
Documentation

The selected big Hilbert class field, represented in the public type of finite abelian subextensions of the separable closure.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def bigHilbertClassFieldFiniteAbelianExtension :
    FiniteAbelianExtension K
def

bigHilbertClassFieldEquiv

L538 ↗
ClassFieldTheory.GlobalClassFieldComparison.bigHilbertClassFieldEquiv
Documentation

The original selected field and its public separable-closure realization are equivalent over the base.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def bigHilbertClassFieldEquiv :
    GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField K ≃ₐ[K]
      bigHilbertClassFieldFiniteAbelianExtension K
def

smallHilbertClassFieldEmbedding

L544 ↗
ClassFieldTheory.GlobalClassFieldComparison.smallHilbertClassFieldEmbedding
Documentation

The selected small Hilbert class field in the separable closure.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def smallHilbertClassFieldEmbedding :
    GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField K →ₐ[K]
      SeparableClosure K
def

smallHilbertClassFieldFiniteAbelianExtension

L549 ↗
ClassFieldTheory.GlobalClassFieldComparison.smallHilbertClassFieldFiniteAbelianExtension
Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def smallHilbertClassFieldFiniteAbelianExtension :
    FiniteAbelianExtension K
def

smallHilbertClassFieldEquiv

L556 ↗
ClassFieldTheory.GlobalClassFieldComparison.smallHilbertClassFieldEquiv
Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def smallHilbertClassFieldEquiv :
    GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField K ≃ₐ[K]
      smallHilbertClassFieldFiniteAbelianExtension K
theorem

bigHilbertClassField_degree_eq_narrowClassGroup_card

L565 ↗
ClassFieldTheory.GlobalClassFieldComparison.bigHilbertClassField_degree_eq_narrowClassGroup_card
Documentation

The selected big Hilbert class field has degree equal to the order of the narrow class group of the original number field.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
open _root_.GlobalClassFieldTheory.GlobalClassFields
  (bigHilbertClassField_finrank_over_original_eq_narrowClassGroup_card) in
Lean source · statement
theorem bigHilbertClassField_degree_eq_narrowClassGroup_card :
    Module.finrank K
        (GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField K) =
      Nat.card (RayClass.NarrowClassGroup K)
theorem

smallHilbertClassField_degree_eq_classNumber

L576 ↗
ClassFieldTheory.GlobalClassFieldComparison.smallHilbertClassField_degree_eq_classNumber
Documentation

The selected small Hilbert class field has degree equal to the ordinary class number of the original number field.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
open _root_.GlobalClassFieldTheory.GlobalClassFields
  (smallHilbertClassField_finrank_over_original_eq_classNumber) in
Lean source · statement
theorem smallHilbertClassField_degree_eq_classNumber :
    Module.finrank K
        (GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField K) =
      NumberField.classNumber K
theorem

bigHilbertClassField_unramifiedAtFinitePlaces

L585 ↗
ClassFieldTheory.GlobalClassFieldComparison.bigHilbertClassField_unramifiedAtFinitePlaces
Documentation

The selected big Hilbert class field is unramified at every finite place.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem bigHilbertClassField_unramifiedAtFinitePlaces :
    _root_.IsUnramifiedAtFinitePlaces K
      (GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField K)
theorem

nonempty_algHom_to_selectedBigHilbertClassField

L595 ↗
ClassFieldTheory.GlobalClassFieldComparison.nonempty_algHom_to_selectedBigHilbertClassField
Documentation

Every publicly represented finite-prime-unramified abelian extension embeds into the selected big Hilbert class field.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
open _root_.GlobalClassFieldTheory.GlobalClassFields
  (finiteUnramifiedAbelianExtension_nonempty_algHom_bigHilbertClassField) in
Lean source · statement
theorem nonempty_algHom_to_selectedBigHilbertClassField
    (F : FiniteAbelianExtension K)
    (hF : IsUnramifiedAtFinitePlaces K F) :
    Nonempty (F →ₐ[K]
      GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField K)
theorem

exists_bigHilbertClassField

L607 ↗
ClassFieldTheory.GlobalClassFieldComparison.exists_bigHilbertClassField
Documentation

The intrinsic big Hilbert class field exists inside the chosen separable closure of the base.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem exists_bigHilbertClassField :
    ∃ E : FiniteAbelianExtension K, IsBigHilbertClassField E
theorem

bigHilbertClassField_degree_eq_narrowClassGroup_card_of_isBig

L625 ↗
ClassFieldTheory.GlobalClassFieldComparison.bigHilbertClassField_degree_eq_narrowClassGroup_card_of_isBig
Documentation

Every intrinsic big Hilbert class field has the degree of the selected implementation, hence the narrow class number.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem bigHilbertClassField_degree_eq_narrowClassGroup_card_of_isBig
    (E : FiniteAbelianExtension K)
    (hE : IsBigHilbertClassField E) :
    Module.finrank K E = Nat.card (RayClass.NarrowClassGroup K)
theorem

smallHilbertClassField_everywhereUnramified

L652 ↗
ClassFieldTheory.GlobalClassFieldComparison.smallHilbertClassField_everywhereUnramified
Documentation

The selected small Hilbert class field is unramified at all finite and infinite places.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem smallHilbertClassField_everywhereUnramified :
    _root_.IsEverywhereUnramified K
      (GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField K)
theorem

nonempty_algHom_to_selectedSmallHilbertClassField

L662 ↗
ClassFieldTheory.GlobalClassFieldComparison.nonempty_algHom_to_selectedSmallHilbertClassField
Documentation

Any publicly represented everywhere-unramified abelian extension embeds into the selected small Hilbert class field.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
open _root_.GlobalClassFieldTheory.GlobalClassFields
  (finiteAbelianExtension_nonempty_algHom_to_smallHilbertClassField_of_everywhereUnramified) in
Lean source · statement
theorem nonempty_algHom_to_selectedSmallHilbertClassField
    (F : FiniteAbelianExtension K)
    (hF : IsEverywhereUnramified K F) :
    Nonempty (F →ₐ[K]
      GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField K)
theorem

exists_smallHilbertClassField

L684 ↗
ClassFieldTheory.GlobalClassFieldComparison.exists_smallHilbertClassField
Documentation

The intrinsic small Hilbert class field exists inside the chosen separable closure of the base.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem exists_smallHilbertClassField :
    ∃ E : FiniteAbelianExtension K, IsSmallHilbertClassField E
theorem

smallHilbertClassField_degree_eq_classNumber_of_isSmall

L702 ↗
ClassFieldTheory.GlobalClassFieldComparison.smallHilbertClassField_degree_eq_classNumber_of_isSmall
Documentation

Every intrinsic small Hilbert class field has the degree of the selected implementation, hence the class number.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem smallHilbertClassField_degree_eq_classNumber_of_isSmall
    (E : FiniteAbelianExtension K)
    (hE : IsSmallHilbertClassField E) :
    Module.finrank K E = NumberField.classNumber K
def

smallHilbertClassFieldEquivOfIsSmall

L729 ↗
ClassFieldTheory.GlobalClassFieldComparison.smallHilbertClassFieldEquivOfIsSmall
Documentation

Every intrinsic small Hilbert class field is isomorphic over the base to the selected implementation.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def smallHilbertClassFieldEquivOfIsSmall
    (E : FiniteAbelianExtension K)
    (hE : IsSmallHilbertClassField E) :
    E ≃ₐ[K]
      GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField K
theorem

finitePrime_splitsCompletelyInSmallHilbertClassField_iff_principal

L749 ↗
ClassFieldTheory.GlobalClassFieldComparison.finitePrime_splitsCompletelyInSmallHilbertClassField_iff_principal
Documentation

A finite prime actually splits completely in the selected small Hilbert class field exactly when its prime fractional ideal is principal.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
open _root_.GlobalClassFieldTheory.IdealClassFieldTheory
  (finitePlaceSplitsCompletelyInSmallHilbertClassField_iff_principal) in
Lean source · statement
theorem finitePrime_splitsCompletelyInSmallHilbertClassField_iff_principal
    (v : HeightOneSpectrum (𝓞 K)) :
    _root_.FinitePlaceSplitsCompletely
          (K := K)
          (L := GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField K)
          v ↔
      FractionalIdealGroup.prime v ∈
        (toPrincipalIdeal (𝓞 K) K).range
theorem

finitePrime_splitsCompletelyInSmallHilbertClassField_iff_principal_of_isSmall

L762 ↗
ClassFieldTheory.GlobalClassFieldComparison.finitePrime_splitsCompletelyInSmallHilbertClassField_iff_principal_of_isSmall
Documentation

The complete-splitting criterion transfers from the selected small Hilbert class field to every intrinsic one.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePrime_splitsCompletelyInSmallHilbertClassField_iff_principal_of_isSmall
    (E : FiniteAbelianExtension K)
    (hE : IsSmallHilbertClassField E)
    (v : HeightOneSpectrum (𝓞 K)) :
    FinitePrimeSplitsCompletely K E v ↔
      finitePrimeFractionalIdeal v ∈
        (toPrincipalIdeal (𝓞 K) K).range
theorem

ideals_becomePrincipalInSmallHilbertClassField

L785 ↗
ClassFieldTheory.GlobalClassFieldComparison.ideals_becomePrincipalInSmallHilbertClassField
Documentation

Every integral ideal becomes principal after extension to the selected small Hilbert class field.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem ideals_becomePrincipalInSmallHilbertClassField :
    ∀ I : Ideal (𝓞 K),
      (I.map
        (algebraMap
          (𝓞 K)
          (𝓞 (GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField K)))).IsPrincipal
theorem

ideals_becomePrincipalInSmallHilbertClassField_of_isSmall

L796 ↗
ClassFieldTheory.GlobalClassFieldComparison.ideals_becomePrincipalInSmallHilbertClassField_of_isSmall
Documentation

Principalization transfers from the selected small Hilbert class field to every intrinsic one.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
open NumberField IsDedekindDomain
open LocalFieldTheory
open scoped ValuativeRel
section HilbertClassFields
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem ideals_becomePrincipalInSmallHilbertClassField_of_isSmall
    (E : FiniteAbelianExtension K)
    (hE : IsSmallHilbertClassField E) :
    ∀ I : Ideal (𝓞 K),
      (I.map (algebraMap (𝓞 K) (𝓞 E))).IsPrincipal

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.