NYLL
Module

FinitePrime.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.FinitePrime
3 declarations indexed from sourceView source ↗

Module documentation

Normalized finite-prime ideles

This file defines the idele supported at one finite place with normalized local order one, and computes its associated fractional ideal and ideal class. These constructions are independent of class field theory.

Imports9
Imported by9

Declarations

def

finitePrimeIdele

L38 ↗
IdeleGroup.finitePrimeIdele
Documentation

The idele supported at v whose normalized local order is one.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace IdeleGroup
open NumberField IsDedekindDomain
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
def finitePrimeIdele
    (v : HeightOneSpectrum (𝓞 K)) :
    IdeleGroup K
theorem

fractionalIdeal_finitePrimeIdele

L46 ↗
IdeleGroup.fractionalIdeal_finitePrimeIdele
Documentation

The fractional ideal of the normalized one-place prime idele is the corresponding prime ideal.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace IdeleGroup
open NumberField IsDedekindDomain
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem fractionalIdeal_finitePrimeIdele
    (v : HeightOneSpectrum (𝓞 K)) :
    fractionalIdeal (finitePrimeIdele v) =
      FractionalIdealGroup.prime v
theorem

idealClass_finitePrimeIdele

L100 ↗
IdeleGroup.idealClass_finitePrimeIdele
Documentation

The ordinary ideal class of the normalized one-place prime idele is the class of the corresponding prime ideal.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace IdeleGroup
open NumberField IsDedekindDomain
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem idealClass_finitePrimeIdele
    (v : HeightOneSpectrum (𝓞 K)) :
    idealClass (finitePrimeIdele v) =
      ClassGroup.mk K (FractionalIdealGroup.prime v)

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