Module

IsRayCongruent.lean

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.IsRayCongruent

5 declarations indexed from sourceView source ↗

Module documentation

Ray congruences

Imports2

Imported by5

def

finitePlaceUnitEmbedding

L26 ↗

ClassFieldTheory.finitePlaceUnitEmbedding

Documentation

The diagonal embedding of field units into a finite completion.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

def finitePlaceUnitEmbedding
    {K : Type u} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) :
    Kˣ →* (v.adicCompletion K)ˣ

def

IsRayCongruent

L34 ↗

ClassFieldTheory.IsRayCongruent

Documentation

A field unit satisfies the finite congruences and real positivity conditions specified by a ray modulus.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

def IsRayCongruent
    {K : Type u} [Field K] [NumberField K]
    (m : RayClassModulus K) (x : Kˣ) : Prop

theorem

one

L46 ↗

ClassFieldTheory.IsRayCongruent.one

Documentation

The identity satisfies every ray congruence.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace IsRayCongruent

Lean source · statement

theorem one {K : Type u} [Field K] [NumberField K]
    (m : RayClassModulus K) : IsRayCongruent m 1

theorem

mul

L55 ↗

ClassFieldTheory.IsRayCongruent.mul

Documentation

Ray-congruent nonzero elements are closed under multiplication.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace IsRayCongruent

Lean source · statement

theorem mul {K : Type u} [Field K] [NumberField K]
    {m : RayClassModulus K} {x y : Kˣ}
    (hx : IsRayCongruent m x) (hy : IsRayCongruent m y) :
    IsRayCongruent m (x * y)

theorem

inv

L67 ↗

ClassFieldTheory.IsRayCongruent.inv

Documentation

Ray-congruent nonzero elements are closed under inversion.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace IsRayCongruent

Lean source · statement

theorem inv {K : Type u} [Field K] [NumberField K]
    {m : RayClassModulus K} {x : Kˣ}
    (hx : IsRayCongruent m x) : IsRayCongruent m x⁻¹

Module documentation

Ray congruences

Declarations

finitePlaceUnitEmbedding

IsRayCongruent

one

mul

inv