Module

IntrinsicFrobeniusArtinComparison.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FixedFieldIntrinsicReciprocity.IntrinsicFrobeniusArtinComparison

2 declarations indexed from sourceView source ↗

Module documentation

Intrinsic Frobenius Artin comparison

This module identifies the canonical local Artin homomorphism of an actual finite fixed-field extension with its ambient fixed-field norm-residue symbol.

Imports2

Mathlib.FieldTheory.Galois.Basic
Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FixedFieldIntrinsicReciprocity.PrimeComparison

Imported by2

instance

intrinsicFixedFieldArtin_absoluteFinite

L38 ↗

LocalClassFieldTheory.intrinsicFixedFieldArtin_absoluteFinite

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
section IntrinsicFixedFieldArtinComparison
variable
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      Gal(SeparableClosure K/K))
    (J : ClosedSubgroup Gal(SeparableClosure K/K))
    (hJH : J.toSubgroup ≤ H.field.toSubgroup)
    [hJnormal : (extensionSubgroup H.field J hJH).Normal]
    [hJfinite : Finite
      (H.field.toSubgroup ⧸ extensionSubgroup H.field J hJH)]

Lean source · statement

instance intrinsicFixedFieldArtin_absoluteFinite :
    Finite
      ((baseField
        Gal(SeparableClosure K/K)).toSubgroup ⧸
        extensionSubgroup
          (baseField Gal(SeparableClosure K/K))
          H.field (le_baseField H.field))

theorem

intrinsicFixedFieldLocalArtinMonoidHom_eq_abstractFixedFieldNormResidueSymbol

L51 ↗

LocalClassFieldTheory.intrinsicFixedFieldLocalArtinMonoidHom_eq_abstractFixedFieldNormResidueSymbol

Documentation

The canonical local Artin homomorphism of the actual finite fixed-field extension agrees with the ambient fixed-field norm-residue symbol. The proof uses the given valuation-preserving equivalence of separable closures to construct actual norm-class representatives.

Source context 8 commands