Module

Core.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.FinitePlaceArtin.Core

2 declarations indexed from sourceView source ↗

Module documentation

Image and kernel of finite-place Artin homomorphisms

This module identifies the image with the chosen decomposition group and the kernel with the chosen local norm subgroup.

Imports6

Imported by6

theorem

chosenFinitePlaceArtinMonoidHom_range

L43 ↗

GlobalClassFieldTheory.Reciprocity.chosenFinitePlaceArtinMonoidHom_range

Documentation

The image of the chosen finite-place Artin homomorphism is exactly the chosen decomposition group.

Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem chosenFinitePlaceArtinMonoidHom_range
    (v : HeightOneSpectrum (𝓞 K)) :
    (chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v).range =
      finitePlaceDecompositionGroup
        (K := K) (L := L) v

theorem

chosenFinitePlaceArtinMonoidHom_ker

L140 ↗

GlobalClassFieldTheory.Reciprocity.chosenFinitePlaceArtinMonoidHom_ker