Module

FractionalIdealNormExponentMap.lean

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.FractionalIdealNormExponentMap

2 declarations indexed from sourceView source ↗

Module documentation

Norm of a fractional-ideal exponent vector

A finite prime of an extension contracts to a finite prime of the base. The norm sends its exponent to the prime below, multiplied by the inertia degree. The resulting map on finitely supported exponent vectors is additive.

Imports5

Mathlib.Algebra.BigOperators.Finsupp.Basic
Mathlib.NumberTheory.NumberField.Basic
Mathlib.RingTheory.DedekindDomain.Factorization
Mathlib.RingTheory.Ideal.GoingUp
Mathlib.RingTheory.Ideal.Norm.RelNorm

Imported by2

def

fractionalIdealNormPrimeBelow

L33 ↗

ClassFieldTheory.fractionalIdealNormPrimeBelow

Documentation

The finite prime below a finite prime in an extension of number fields.

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 v

Lean source · full declaration

def fractionalIdealNormPrimeBelow
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    (W : HeightOneSpectrum (𝓞 L)) :
    HeightOneSpectrum (𝓞 K) where
  asIdeal := W.asIdeal.under (𝓞 K)
  isPrime := inferInstance
  ne_bot :=
    Ring.ne_bot_of_isMaximal_of_not_isField
      (M := W.asIdeal.under (𝓞 K)) inferInstance
      (RingOfIntegers.not_isField K)

def