Module

EmbeddedAbelianSubextension.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.EmbeddedAbelianSubextension

2 declarations indexed from sourceView source ↗

Module documentation

Embedded finite abelian subextensions

An embedding of an actual finite abelian extension into the rational separable closure determines a finite abelian subextension of the fixing subgroup of the embedded base field. This file also allows that base fixing subgroup to be replaced by a propositionally equal selected subgroup, as is needed by concrete class-field realizations.

Imports3

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.FiniteAbelianSubextension
Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalNormResidueNaturality
Mathlib.FieldTheory.Galois.Abelian

Imported by3

def

numberFieldEmbeddedAbelianSubextension

L36 ↗

GlobalClassFieldTheory.GlobalClassFields.numberFieldEmbeddedAbelianSubextension

Documentation

An actual finite abelian extension embedded in the rational separable closure, represented as a finite abelian subextension of a selected base subgroup equal to the fixing subgroup of the embedded base field.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open Reciprocity

Lean source · statement

def numberFieldEmbeddedAbelianSubextension
    (K E : Type)
    [Field K] [NumberField K]
    [Field E] [NumberField E]
    [Algebra K E] [FiniteDimensional K E]
    [IsAbelianGalois K E]
    (j : E →ₐ[ℚ] SeparableClosure ℚ)
    (B : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hbase : numberFieldEmbeddedBaseSubgroup K E j = B) :
    FiniteAbelianSubextension B

theorem

numberFieldEmbeddedAbelianSubextension_field

L70 ↗

GlobalClassFieldTheory.GlobalClassFields.numberFieldEmbeddedAbelianSubextension_field