Module

FractionalIdealNorm.lean

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.FractionalIdealNorm

1 declaration indexed from sourceView source ↗

Module documentation

Relative norm of nonzero fractional ideals

The norm sends a finite-prime factor upstairs to the prime below it, with exponent multiplied by the inertia degree. Prime factorization extends this rule to a multiplicative map on all nonzero fractional ideals.

Imports2

Imported by3

def

fractionalIdealNorm

L31 ↗

ClassFieldTheory.fractionalIdealNorm

Documentation

The relative norm of nonzero fractional ideals of number fields, defined by its inertia-degree-weighted action on prime exponents.

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 · statement

def fractionalIdealNorm
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] :
    NumberFieldFractionalIdealGroup L →*
      NumberFieldFractionalIdealGroup K

Module documentation

Relative norm of nonzero fractional ideals

Declarations

fractionalIdealNorm