Module

SmallHilbertSplitting.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.SmallHilbertSplitting

5 declarations indexed from sourceView source ↗

Module documentation

Splitting in the small Hilbert class field

The small Hilbert class field has reciprocity quotient the ordinary ideal class group. Thus the Frobenius class of a finite prime is its ordinary ideal class, and it is trivial precisely when the prime ideal is principal.

Imports2

Imported by3

theorem

smallHilbertSplittingClassGroupIsMulCommutative

L30 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertSplittingClassGroupIsMulCommutative

Documentation

Canonical class-group commutativity supplies normality for the quotient.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain

Lean source · statement

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

def

smallHilbertFrobeniusClass

L41 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFrobeniusClass

Documentation

The Frobenius class of a finite prime in the reciprocity quotient of the small Hilbert class field.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
attribute [local instance] smallHilbertSplittingClassGroupIsMulCommutative
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

def smallHilbertFrobeniusClass
    (v : HeightOneSpectrum (𝓞 K)) :
    IdeleClassGroup K ⧸
      GlobalClassFields.smallHilbertClassFieldNormSubgroup

def

SplitsCompletelyInSmallHilbertClassField

L51 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.SplitsCompletelyInSmallHilbertClassField

Documentation

Reciprocity formulation of complete splitting in the small Hilbert class field: the prime 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 IdealClassFieldTheory
open NumberField IsDedekindDomain
attribute [local instance] smallHilbertSplittingClassGroupIsMulCommutative
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

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

theorem

splitsCompletelyInSmallHilbertClassField_iff_principal

L57 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.splitsCompletelyInSmallHilbertClassField_iff_principal

Documentation

A finite prime splits completely in the small Hilbert class field if and only if its 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 IdealClassFieldTheory
open NumberField IsDedekindDomain
attribute [local instance] smallHilbertSplittingClassGroupIsMulCommutative
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

theorem splitsCompletelyInSmallHilbertClassField_iff_principal
    (v : HeightOneSpectrum (𝓞 K)) :
    SplitsCompletelyInSmallHilbertClassField v ↔
      FractionalIdealGroup.prime v ∈
        (toPrincipalIdeal (𝓞 K) K).range

theorem

splitsCompletelyInSmallHilbertClassField_iff_exists_generator

L79 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.splitsCompletelyInSmallHilbertClassField_iff_exists_generator

Documentation

Existential generator form of the small Hilbert splitting criterion.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
attribute [local instance] smallHilbertSplittingClassGroupIsMulCommutative
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

theorem splitsCompletelyInSmallHilbertClassField_iff_exists_generator
    (v : HeightOneSpectrum (𝓞 K)) :
    SplitsCompletelyInSmallHilbertClassField v ↔
      ∃ x : Kˣ,
        toPrincipalIdeal (𝓞 K) K x =
          FractionalIdealGroup.prime v

Module documentation

Splitting in the small Hilbert class field

Declarations

smallHilbertSplittingClassGroupIsMulCommutative

smallHilbertFrobeniusClass

SplitsCompletelyInSmallHilbertClassField

splitsCompletelyInSmallHilbertClassField_iff_principal

splitsCompletelyInSmallHilbertClassField_iff_exists_generator