Module

NormSubgroupRingEquiv.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.NormSubgroupRingEquiv

2 declarations indexed from sourceView source ↗

Module documentation

Transport of finite-extension norm subgroups

Compatible field equivalences carry the actual group of field norms to the actual group of field norms. This is the norm comparison needed when finite local class-field theory is transported to a small representative.

Imports2

Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.FieldNormSubgroup
Mathlib.RingTheory.Norm.Basic

Imported by3

theorem

fieldNormHom_map_ringEquiv

L30 ↗

ClassFieldTheory.fieldNormHom_map_ringEquiv

Documentation

The field-norm homomorphisms commute with compatible field equivalences.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v w x
variable {F : Type u} {M : Type v} {F' : Type w} {M' : Type x}
  [Field F] [Field M] [Field F'] [Field M']
  [Algebra F M] [Algebra F' M']
  [FiniteDimensional F M] [FiniteDimensional F' M']

Lean source · statement

theorem fieldNormHom_map_ringEquiv
    (eF : F ≃+* F') (eM : M ≃+* M')
    (he : (algebraMap F' M').comp eF.toRingHom =
      eM.toRingHom.comp (algebraMap F M))
    (y : Mˣ) :
    (Units.mapEquiv eF.toMulEquiv) (fieldNormHom F M y) =
      fieldNormHom F' M' (Units.mapEquiv eM.toMulEquiv y)

theorem

fieldNormSubgroup_map_ringEquiv

L45 ↗

ClassFieldTheory.fieldNormSubgroup_map_ringEquiv