Module

NormSubgroupFunctoriality.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.NormSubgroupFunctoriality

4 declarations indexed from sourceView source ↗

Module documentation

Functoriality of finite-extension norm subgroups

The local existence proof repeatedly enlarges a finite extension and replaces finite extensions by isomorphic realizations. This file records the resulting identities for unit norms and their images in the base field.

Imports1

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.NormQuotient

Imported by5

theorem

normSubgroup_le_of_tower

L27 ↗

LocalFieldTheory.normSubgroup_le_of_tower

Documentation

Enlarging the top field in a finite tower can only shrink its norm subgroup in the base field.

Source context 3 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory

Lean source · statement

theorem normSubgroup_le_of_tower
    (K M L : Type) [Field K] [Field M] [Field L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L] [FiniteDimensional M L] :
    localNormSubgroup K L ≤ localNormSubgroup K M

theorem

normUnits_algEquiv

L38 ↗

LocalFieldTheory.normUnits_algEquiv

Documentation

The norm on units is unchanged after replacing a finite extension by an isomorphic realization.

Source context 3 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory

Lean source · statement

theorem normUnits_algEquiv
    (K L M : Type) [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    (e : L ≃ₐ[K] M) (x : Lˣ) :
    normUnits K M (Units.mapEquiv e.toMulEquiv x) = normUnits K L x

theorem

normSubgroup_algEquiv

L48 ↗

LocalFieldTheory.normSubgroup_algEquiv

Documentation

Norm subgroups are unchanged after replacing an extension by an isomorphic realization.

Source context 3 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory

Lean source · statement

theorem normSubgroup_algEquiv
    (K L M : Type) [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    (e : L ≃ₐ[K] M) :
    localNormSubgroup K M = localNormSubgroup K L

theorem

normSubgroup_le_of_algHom

L71 ↗

LocalFieldTheory.normSubgroup_le_of_algHom

Documentation

An algebra embedding of finite extensions reverses inclusion of their norm subgroups.

Source context 3 commands

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

noncomputable section
namespace LocalFieldTheory
open LocalFieldTheory

Lean source · statement

theorem normSubgroup_le_of_algHom
    (K M D : Type) [Field K] [Field M] [Field D]
    [Algebra K M] [Algebra K D]
    [FiniteDimensional K M] [FiniteDimensional K D]
    (i : M →ₐ[K] D) :
    localNormSubgroup K D ≤ localNormSubgroup K M

Module documentation

Functoriality of finite-extension norm subgroups

Declarations

normSubgroup_le_of_tower

normUnits_algEquiv

normSubgroup_algEquiv

normSubgroup_le_of_algHom