Module

HilbertClassFieldPrimeSplitting.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldPrimeSplitting

28 declarations indexed from sourceView source ↗

Module documentation

Prime splitting for a maximal everywhere-unramified cyclic norm quotient

Suppose a cyclic extension is unramified at every finite and infinite place and its degree is the ordinary class number. Its actual idèle-class norm quotient is then the small-Hilbert reciprocity quotient. This file transports prime Frobenius classes across that identification and proves that trivial Frobenius is equivalent to principality of the prime ideal.

Imports4

Imported by3

theorem

hilbertPrimeSplittingClassGroupIsMulCommutative

L35 ↗

GlobalClassFieldTheory.GlobalClassFields.hilbertPrimeSplittingClassGroupIsMulCommutative

Documentation

The canonical idèle-class multiplication makes every subgroup normal.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup

Lean source · statement

theorem hilbertPrimeSplittingClassGroupIsMulCommutative
    (F : Type) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

def

bigHilbertFrobeniusClass

L51 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertFrobeniusClass

Documentation

The prime Frobenius class in the big-Hilbert reciprocity quotient.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

def bigHilbertFrobeniusClass
    (v : HeightOneSpectrum (𝓞 K)) :
    IdeleClassGroup K ⧸
      bigHilbertClassFieldNormSubgroup (K := K)

theorem

mulEquiv_symm_apply_eq_one_iff

L61 ↗

GlobalClassFieldTheory.GlobalClassFields.mulEquiv_symm_apply_eq_one_iff

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem mulEquiv_symm_apply_eq_one_iff
    {G H : Type} [Group G] [Group H]
    (e : G ≃* H) (x : H) :
    e.symm x = 1 ↔ x = 1

theorem

mulEquiv_apply_trans_symm

L74 ↗

GlobalClassFieldTheory.GlobalClassFields.mulEquiv_apply_trans_symm

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem mulEquiv_apply_trans_symm
    {G H I : Type} [Group G] [Group H] [Group I]
    (e : G ≃* H) (f : H ≃* I) (x : I) :
    e ((e.trans f).symm x) = f.symm x

theorem

quotientMulEquivOfEq_trans_apply_mk

L80 ↗

GlobalClassFieldTheory.GlobalClassFields.quotientMulEquivOfEq_trans_apply_mk

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem quotientMulEquivOfEq_trans_apply_mk
    {G I : Type} [Group G] [Group I]
    (M N : Subgroup G) [M.Normal] [N.Normal]
    (h : M = N) (e : G ⧸ N ≃* I) (x : G) :
    ((QuotientGroup.quotientMulEquivOfEq h).trans e)
        (QuotientGroup.mk' M x) =
      e (QuotientGroup.mk' N x)

def

primeHasTotallyPositiveGenerator

L91 ↗

GlobalClassFieldTheory.GlobalClassFields.primeHasTotallyPositiveGenerator

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

def primeHasTotallyPositiveGenerator
    (v : HeightOneSpectrum (𝓞 K)) : Prop

theorem

finitePrimeIdele_mem_narrowDenominator_imp_primeHasTotallyPositiveGenerator

L101 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePrimeIdele_mem_narrowDenominator_imp_primeHasTotallyPositiveGenerator

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem
    finitePrimeIdele_mem_narrowDenominator_imp_primeHasTotallyPositiveGenerator
    (v : HeightOneSpectrum (𝓞 K))
    (hv : finitePrimeIdele v ∈
      RayClass.narrowDenominator (K := K)) :
    primeHasTotallyPositiveGenerator v

theorem

primeHasTotallyPositiveGenerator_imp_finitePrimeIdele_mem_narrowDenominator

L165 ↗

GlobalClassFieldTheory.GlobalClassFields.primeHasTotallyPositiveGenerator_imp_finitePrimeIdele_mem_narrowDenominator

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem
    primeHasTotallyPositiveGenerator_imp_finitePrimeIdele_mem_narrowDenominator
    (v : HeightOneSpectrum (𝓞 K))
    (hgenerator : primeHasTotallyPositiveGenerator v) :
    finitePrimeIdele v ∈
      RayClass.narrowDenominator (K := K)

theorem

finitePrimeIdele_mem_narrowDenominator_iff_primeHasTotallyPositiveGenerator

L223 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePrimeIdele_mem_narrowDenominator_iff_primeHasTotallyPositiveGenerator

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem
    finitePrimeIdele_mem_narrowDenominator_iff_primeHasTotallyPositiveGenerator
    (v : HeightOneSpectrum (𝓞 K)) :
    finitePrimeIdele v ∈
        RayClass.narrowDenominator (K := K) ↔
      primeHasTotallyPositiveGenerator v

theorem

bigHilbertFrobeniusClass_eq_one_iff_exists_totallyPositiveGenerator

L235 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertFrobeniusClass_eq_one_iff_exists_totallyPositiveGenerator

Documentation

The big-Hilbert Frobenius class is trivial exactly when the prime has a generator whose principal idèle is positive at every real infinite place.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem
    bigHilbertFrobeniusClass_eq_one_iff_exists_totallyPositiveGenerator
    (v : HeightOneSpectrum (𝓞 K)) :
    bigHilbertFrobeniusClass v = 1 ↔
      ∃ x : Kˣ,
        IdeleGroup.principalIdele K x ∈
          RayClass.idelePrimeToModulusSubgroup
            (RayClass.Modulus.narrowOfFinite
              (0 : RayClass.FiniteModulus K)) ∧
        toPrincipalIdeal (𝓞 K) K x =
          FractionalIdealGroup.prime v

def

maximalFiniteUnramifiedCyclicFrobeniusClass

L260 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalFiniteUnramifiedCyclicFrobeniusClass

Documentation

The prime Frobenius class in the actual norm quotient of a maximal finite-unramified cyclic extension.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]
omit [IsUnramifiedAtInfinitePlaces K L] in

Lean source · statement

def maximalFiniteUnramifiedCyclicFrobeniusClass
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        Nat.card (RayClass.NarrowClassGroup K))
    (v : HeightOneSpectrum (𝓞 K)) :
    IdeleClassGroup K ⧸
      (_root_.ideleClassNorm K L).range

theorem

maximalFiniteUnramifiedCyclicFrobeniusClass_eq_finitePrimeIdeleClass

L279 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalFiniteUnramifiedCyclicFrobeniusClass_eq_finitePrimeIdeleClass

Documentation

The maximal finite-unramified norm-quotient Frobenius class is represented by the one-place prime idèle class.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]
omit [IsUnramifiedAtInfinitePlaces K L] in

Lean source · statement

theorem
    maximalFiniteUnramifiedCyclicFrobeniusClass_eq_finitePrimeIdeleClass
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        Nat.card (RayClass.NarrowClassGroup K))
    (v : HeightOneSpectrum (𝓞 K)) :
    maximalFiniteUnramifiedCyclicFrobeniusClass
        (K := K) (L := L) hunramified hdegree v =
      QuotientGroup.mk'
        ((_root_.ideleClassNorm K L).range)
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K)
          (finitePrimeIdele v))

theorem

orderOf_maximalFiniteUnramifiedCyclicFrobeniusClass

L335 ↗

GlobalClassFieldTheory.GlobalClassFields.orderOf_maximalFiniteUnramifiedCyclicFrobeniusClass

Documentation

The order of the actual maximal finite-unramified Frobenius class is the order of its narrow ideal class.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]
omit [IsUnramifiedAtInfinitePlaces K L] in

Lean source · statement

theorem orderOf_maximalFiniteUnramifiedCyclicFrobeniusClass
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        Nat.card (RayClass.NarrowClassGroup K))
    (v : HeightOneSpectrum (𝓞 K)) :
    orderOf
        (maximalFiniteUnramifiedCyclicFrobeniusClass
          (K := K) (L := L) hunramified hdegree v) =
      orderOf
        (QuotientGroup.mk'
          (RayClass.narrowDenominator (K := K))
          (finitePrimeIdele v))

theorem

maximalFiniteUnramifiedCyclicFrobeniusClass_eq_one_iff_exists_totallyPositiveGenerator

L361 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalFiniteUnramifiedCyclicFrobeniusClass_eq_one_iff_exists_totallyPositiveGenerator

Documentation

The Frobenius class in the actual maximal finite-unramified norm quotient is trivial exactly when the prime has a totally positive generator.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]
omit [IsUnramifiedAtInfinitePlaces K L] in

Lean source · statement

theorem
    maximalFiniteUnramifiedCyclicFrobeniusClass_eq_one_iff_exists_totallyPositiveGenerator
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        Nat.card (RayClass.NarrowClassGroup K))
    (v : HeightOneSpectrum (𝓞 K)) :
    maximalFiniteUnramifiedCyclicFrobeniusClass
        (K := K) (L := L) hunramified hdegree v = 1 ↔
      ∃ x : Kˣ,
        IdeleGroup.principalIdele K x ∈
          RayClass.idelePrimeToModulusSubgroup
            (RayClass.Modulus.narrowOfFinite
              (0 : RayClass.FiniteModulus K)) ∧
        toPrincipalIdeal (𝓞 K) K x =
          FractionalIdealGroup.prime v

theorem

finitePrimeIdeleClass_eq_one_of_splitsCompletely

L391 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePrimeIdeleClass_eq_one_of_splitsCompletely

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]
omit [IsCyclic (L ≃ₐ[K] L)] [IsUnramifiedAtInfinitePlaces K L] in

Lean source · statement

theorem finitePrimeIdeleClass_eq_one_of_splitsCompletely
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    QuotientGroup.mk'
        ((_root_.ideleClassNorm K L).range)
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K)
          (finitePrimeIdele v)) = 1

theorem

finitePlaceSplitsCompletely_imp_maximalFiniteUnramifiedCyclicFrobeniusClass_eq_one

L416 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePlaceSplitsCompletely_imp_maximalFiniteUnramifiedCyclicFrobeniusClass_eq_one

Documentation

Actual complete splitting in a maximal finite-unramified cyclic extension forces triviality of the corresponding norm-quotient Frobenius class.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]
omit [IsUnramifiedAtInfinitePlaces K L] in

Lean source · statement

theorem
    finitePlaceSplitsCompletely_imp_maximalFiniteUnramifiedCyclicFrobeniusClass_eq_one
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        Nat.card (RayClass.NarrowClassGroup K))
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    maximalFiniteUnramifiedCyclicFrobeniusClass
        (K := K) (L := L) hunramified hdegree v = 1

theorem

finitePlaceSplitsCompletely_imp_exists_totallyPositiveGenerator_of_maximalFiniteUnramifiedCyclic

L439 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePlaceSplitsCompletely_imp_exists_totallyPositiveGenerator_of_maximalFiniteUnramifiedCyclic

Documentation

Every prime which actually splits completely in a maximal finite-unramified cyclic extension has a totally positive generator.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]
omit [IsUnramifiedAtInfinitePlaces K L] in

Lean source · statement

theorem
    finitePlaceSplitsCompletely_imp_exists_totallyPositiveGenerator_of_maximalFiniteUnramifiedCyclic
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        Nat.card (RayClass.NarrowClassGroup K))
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    ∃ x : Kˣ,
      IdeleGroup.principalIdele K x ∈
        RayClass.idelePrimeToModulusSubgroup
          (RayClass.Modulus.narrowOfFinite
            (0 : RayClass.FiniteModulus K)) ∧
      toPrincipalIdeal (𝓞 K) K x =
        FractionalIdealGroup.prime v

def

maximalEverywhereUnramifiedCyclicNormQuotientEquivSmallHilbertQuotient

L465 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalEverywhereUnramifiedCyclicNormQuotientEquivSmallHilbertQuotient

Documentation

At maximal everywhere-unramified cyclic degree, the actual norm quotient is canonically the small-Hilbert reciprocity quotient.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

def maximalEverywhereUnramifiedCyclicNormQuotientEquivSmallHilbertQuotient
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        NumberField.classNumber K) :
    (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) ≃*
      (IdeleClassGroup K ⧸
        smallHilbertClassFieldNormSubgroup (K := K))

def

maximalEverywhereUnramifiedCyclicFrobeniusClass

L482 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalEverywhereUnramifiedCyclicFrobeniusClass

Documentation

The prime Frobenius class in the actual norm quotient of a maximal everywhere-unramified cyclic extension.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

def maximalEverywhereUnramifiedCyclicFrobeniusClass
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        NumberField.classNumber K)
    (v : HeightOneSpectrum (𝓞 K)) :
    IdeleClassGroup K ⧸
      (_root_.ideleClassNorm K L).range

theorem

maximalEverywhereUnramifiedCyclicNormQuotientEquivSmallHilbertQuotient_frobeniusClass

L498 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalEverywhereUnramifiedCyclicNormQuotientEquivSmallHilbertQuotient_frobeniusClass

Documentation

The actual maximal norm-quotient Frobenius class corresponds to the small-Hilbert Frobenius class.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem
    maximalEverywhereUnramifiedCyclicNormQuotientEquivSmallHilbertQuotient_frobeniusClass
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        NumberField.classNumber K)
    (v : HeightOneSpectrum (𝓞 K)) :
    maximalEverywhereUnramifiedCyclicNormQuotientEquivSmallHilbertQuotient
        (K := K) (L := L) hunramifiedFinite hdegree
        (maximalEverywhereUnramifiedCyclicFrobeniusClass
          (K := K) (L := L) hunramifiedFinite hdegree v) =
      IdealClassFieldTheory.smallHilbertFrobeniusClass v

theorem

maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_finitePrimeIdeleClass

L521 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_finitePrimeIdeleClass

Documentation

The maximal norm-quotient Frobenius class is represented by the one-place prime idèle class.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem
    maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_finitePrimeIdeleClass
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        NumberField.classNumber K)
    (v : HeightOneSpectrum (𝓞 K)) :
    maximalEverywhereUnramifiedCyclicFrobeniusClass
        (K := K) (L := L) hunramifiedFinite hdegree v =
      QuotientGroup.mk'
        ((_root_.ideleClassNorm K L).range)
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K)
          (finitePrimeIdele v))

theorem

orderOf_maximalEverywhereUnramifiedCyclicFrobeniusClass

L575 ↗

GlobalClassFieldTheory.GlobalClassFields.orderOf_maximalEverywhereUnramifiedCyclicFrobeniusClass

Documentation

The order of the actual norm-quotient Frobenius class is the order of the corresponding ordinary ideal class.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem orderOf_maximalEverywhereUnramifiedCyclicFrobeniusClass
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        NumberField.classNumber K)
    (v : HeightOneSpectrum (𝓞 K)) :
    orderOf
        (maximalEverywhereUnramifiedCyclicFrobeniusClass
          (K := K) (L := L) hunramifiedFinite hdegree v) =
      orderOf
        (ClassGroup.mk K (FractionalIdealGroup.prime v))

theorem

maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_one_iff_smallHilbertClassFieldSplitsCompletely

L596 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_one_iff_smallHilbertClassFieldSplitsCompletely

Documentation

Under the canonical quotient identification, complete splitting in the small Hilbert class field is equivalent to triviality of the corresponding Frobenius class in the actual maximal norm quotient.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem
  maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_one_iff_smallHilbertClassFieldSplitsCompletely
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        NumberField.classNumber K)
    (v : HeightOneSpectrum (𝓞 K)) :
    maximalEverywhereUnramifiedCyclicFrobeniusClass
        (K := K) (L := L) hunramifiedFinite hdegree v = 1 ↔
      IdealClassFieldTheory.SplitsCompletelyInSmallHilbertClassField v

theorem

maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_one_iff_principal

L634 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_one_iff_principal

Documentation

The Frobenius class in the actual maximal norm quotient is trivial exactly when the corresponding prime ideal is principal.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem
    maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_one_iff_principal
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        NumberField.classNumber K)
    (v : HeightOneSpectrum (𝓞 K)) :
    maximalEverywhereUnramifiedCyclicFrobeniusClass
        (K := K) (L := L) hunramifiedFinite hdegree v = 1 ↔
      FractionalIdealGroup.prime v ∈
        (toPrincipalIdeal (𝓞 K) K).range

theorem

maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_one_iff_exists_generator

L656 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_one_iff_exists_generator

Documentation

Existential generator form of the trivial-Frobenius criterion in the actual maximal norm quotient.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem
    maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_one_iff_exists_generator
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        NumberField.classNumber K)
    (v : HeightOneSpectrum (𝓞 K)) :
    maximalEverywhereUnramifiedCyclicFrobeniusClass
        (K := K) (L := L) hunramifiedFinite hdegree v = 1 ↔
      ∃ x : Kˣ,
        toPrincipalIdeal (𝓞 K) K x =
          FractionalIdealGroup.prime v

theorem

finitePlaceSplitsCompletely_imp_maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_one

L677 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePlaceSplitsCompletely_imp_maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_one

Documentation

If a finite prime actually splits completely in the maximal everywhere-unramified cyclic extension, then its norm-quotient Frobenius class is trivial.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem
    finitePlaceSplitsCompletely_imp_maximalEverywhereUnramifiedCyclicFrobeniusClass_eq_one
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        NumberField.classNumber K)
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    maximalEverywhereUnramifiedCyclicFrobeniusClass
        (K := K) (L := L) hunramifiedFinite hdegree v = 1

theorem

finitePlaceSplitsCompletely_imp_prime_principal_of_maximalEverywhereUnramifiedCyclic

L699 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePlaceSplitsCompletely_imp_prime_principal_of_maximalEverywhereUnramifiedCyclic

Documentation

In a maximal everywhere-unramified cyclic extension, every prime which actually splits completely is principal.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem
    finitePlaceSplitsCompletely_imp_prime_principal_of_maximalEverywhereUnramifiedCyclic
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        NumberField.classNumber K)
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    FractionalIdealGroup.prime v ∈
      (toPrincipalIdeal (𝓞 K) K).range

theorem

not_finitePlaceSplitsCompletely_of_prime_not_principal_of_maximalEverywhereUnramifiedCyclic

L720 ↗

GlobalClassFieldTheory.GlobalClassFields.not_finitePlaceSplitsCompletely_of_prime_not_principal_of_maximalEverywhereUnramifiedCyclic

Documentation

A nonprincipal prime cannot split completely in a maximal everywhere-unramified cyclic extension.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
attribute [local instance] hilbertPrimeSplittingClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    [IsUnramifiedAtInfinitePlaces K L]

Lean source · statement

theorem
    not_finitePlaceSplitsCompletely_of_prime_not_principal_of_maximalEverywhereUnramifiedCyclic
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        NumberField.classNumber K)
    (v : HeightOneSpectrum (𝓞 K))
    (hprincipal :
      FractionalIdealGroup.prime v ∉
        (toPrincipalIdeal (𝓞 K) K).range) :
    ¬ _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v

Module documentation

Prime splitting for a maximal everywhere-unramified cyclic norm quotient

Declarations