NYLL
Module

InfiniteHilbertFactorNaturality.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.InfiniteHilbertFactorNaturality
2 declarations indexed from sourceView source ↗

Module documentation

Naturality of the infinite Hilbert factor

The real-place sign in the explicit infinite Hilbert factor is unchanged under an equivalence of number fields. This reindexes the infinite part of the product formula when a field is replaced by a small model.

Imports3
Imported by2

Declarations

theorem

infinitePlace_embedding_of_isReal_congr

L30 ↗
ClassFieldTheory.infinitePlace_embedding_of_isReal_congr
Documentation

Corresponding real embeddings assign the same real value to a field element and its image under the field equivalence.

Source context 5 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace ClassFieldTheory
universe u v
Lean source · statement
theorem infinitePlace_embedding_of_isReal_congr
    {F : Type u} {G : Type v} [Field F] [Field G]
    (e : F ≃+* G) (W : InfinitePlace G)
    (hv : ((infinitePlaceEquivOfRingEquiv e).symm W).IsReal)
    (hW : W.IsReal) (x : F) :
    InfinitePlace.embedding_of_isReal hv x =
      InfinitePlace.embedding_of_isReal hW (e x)
theorem

globalInfinitePlaceHilbertSymbol_congr

L46 ↗
ClassFieldTheory.globalInfinitePlaceHilbertSymbol_congr
Documentation

The explicit infinite Hilbert factor commutes with equivalence of number fields, including the exceptional quadratic real-place sign.

Source context 5 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace ClassFieldTheory
universe u v
Lean source · statement
theorem globalInfinitePlaceHilbertSymbol_congr
    {F : Type u} {G : Type v}
    [Field F] [NumberField F] [Field G] [NumberField G]
    (e : F ≃+* G) (n : ℕ+)
    (hmuF : (primitiveRoots (n : ℕ) F).Nonempty)
    (W : InfinitePlace G) (a b : Fˣ) :
    rootsOfUnityEquivOfRingEquiv e n hmuF
        (globalInfinitePlaceHilbertSymbol F n
          ((infinitePlaceEquivOfRingEquiv e).symm W) a b) =
      globalInfinitePlaceHilbertSymbol G n W
        (Units.mapEquiv e.toMulEquiv a)
        (Units.mapEquiv e.toMulEquiv b)

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