Module

NormContinuity.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.NormContinuity

3 declarations indexed from sourceView source ↗

Module documentation

Continuity of finite field norms

This module records the analytic input used by the topological finite local reciprocity law: on a finite-dimensional normed algebra, the field norm is a determinant and is therefore continuous. It also bundles the corresponding statements for field units and valuation-ring units.

Imports4

Nyll.ValuedFieldTheory.LocalField.NormUnits
Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.Basic
Mathlib.Analysis.Normed.Module.FiniteDimension
Mathlib.Topology.Instances.Matrix

Imported by5

theorem

algebraNorm_continuous_of_finiteDimensional

L34 ↗

LocalFieldTheory.algebraNorm_continuous_of_finiteDimensional

Documentation

The field norm of a finite-dimensional normed algebra over a complete nontrivially normed field is continuous.

Source context 5 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem algebraNorm_continuous_of_finiteDimensional
    (K : Type u) (L : Type v)
    [NontriviallyNormedField K] [NormedField L]
    [Algebra K L] [FiniteDimensional K L] [CompleteSpace K]
    [ContinuousSMul K L] :
    Continuous (Algebra.norm K : L → K)

theorem

normUnits_continuous_of_finiteDimensional

L50 ↗

LocalFieldTheory.normUnits_continuous_of_finiteDimensional

Documentation

The field norm induced on unit groups is continuous.

Source context 5 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem normUnits_continuous_of_finiteDimensional
    (K : Type u) (L : Type v)
    [NontriviallyNormedField K] [NormedField L]
    [Algebra K L] [FiniteDimensional K L] [CompleteSpace K]
    [ContinuousSMul K L] :
    Continuous (normUnits K L)

theorem

integerUnitsToFieldUnits_continuous

L62 ↗

LocalFieldTheory.integerUnitsToFieldUnits_continuous

Documentation

The canonical inclusion from valuation-ring units to field units is continuous for the subtype topologies.

Source context 5 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem integerUnitsToFieldUnits_continuous
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] :
    Continuous (integerUnitsToFieldUnits K)

Module documentation

Continuity of finite field norms

Declarations

algebraNorm_continuous_of_finiteDimensional

normUnits_continuous_of_finiteDimensional

integerUnitsToFieldUnits_continuous