NYLL
Module

FieldNormSubgroupTower.lean

Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.FieldNormSubgroupTower
1 declaration indexed from sourceView source ↗

Module documentation

Norm subgroups in a tower

The norm from a larger field factors through the norm from every intermediate field. Thus enlarging a finite extension can only shrink its subgroup of norms in the base field. No local-field or Galois assumption is needed.

Imports2
Imported by1

Declarations

theorem

fieldNormSubgroup_le_of_tower

L26 ↗
ClassFieldTheory.fieldNormSubgroup_le_of_tower
Documentation

In a finite tower K ⊆ M ⊆ L, every norm from L to K is a norm from M to K.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v w
Lean source · statement
theorem fieldNormSubgroup_le_of_tower
    (K : Type u) (M : Type v) (L : Type w)
    [Field K] [Field M] [Field L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L] [FiniteDimensional K L] :
    fieldNormSubgroup K L ≤ fieldNormSubgroup K M

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