Module

PadicLinearOfContinuous.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PadicLinearOfContinuous

6 declarations indexed from sourceView source ↗

Module documentation

Continuous additive maps of p-adic modules are p-adic linear

This is the density argument used explicitly in the local-field structure theory, the field-unit structure theorem: compatibility with ordinary integral powers, together with continuity of the p-adic scalar orbit, forces compatibility with every p-adic scalar.

Imports5

Mathlib.NumberTheory.Padics.RingHoms
Mathlib.Topology.Algebra.Module.Basic
Mathlib.LinearAlgebra.Pi
Mathlib.LinearAlgebra.Isomorphisms
Mathlib.RingTheory.Finiteness.Finsupp

Imported by5

def

continuousAddEquivOfMultiplicativeSource

L30 ↗

LocalFieldTheory.DiscreteValuationField.continuousAddEquivOfMultiplicativeSource

Documentation

Turn a topological group equivalence whose source is an additive group written multiplicatively into the inverse topological additive equivalence.

Source context 2 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField

Lean source · statement

def continuousAddEquivOfMultiplicativeSource
    {C G : Type*} [AddZeroClass C] [MulOneClass G]
    [TopologicalSpace C] [TopologicalSpace G]
    (e : Multiplicative C ≃ₜ* G) : Additive G ≃ₜ+ C

def

continuousMulEquivOfAdditiveTarget

L41 ↗

LocalFieldTheory.DiscreteValuationField.continuousMulEquivOfAdditiveTarget

Documentation

Turn a topological additive equivalence into the corresponding topological multiplicative equivalence after tagging the source multiplicatively.

Source context 2 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField

Lean source · statement

def continuousMulEquivOfAdditiveTarget
    {C G : Type*} [AddZeroClass C] [MulOneClass G]
    [TopologicalSpace C] [TopologicalSpace G]
    (e : C ≃ₜ+ Additive G) : Multiplicative C ≃ₜ* G

theorem

map_padicInt_smul_of_continuous

L60 ↗

LocalFieldTheory.DiscreteValuationField.map_padicInt_smul_of_continuous

Documentation

A continuous additive homomorphism between topological Z_p-modules is Z_p-linear. The proof checks natural scalars and extends over the dense copy of ℕ in Z_p.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
variable {A B : Type*}
variable [TopologicalSpace A] [TopologicalSpace B]
variable [AddCommMonoid A] [AddCommMonoid B]
variable [Module ℤ_[p] A] [Module ℤ_[p] B]
variable [ContinuousSMul ℤ_[p] A] [ContinuousSMul ℤ_[p] B]
variable [T2Space B]

Lean source · statement

theorem map_padicInt_smul_of_continuous
    (f : A →+ B) (hf : Continuous f) (a : ℤ_[p]) (x : A) :
    f (a • x) = a • f x

def

padicLinearEquivOfContinuousAddEquiv

L74 ↗

LocalFieldTheory.DiscreteValuationField.padicLinearEquivOfContinuousAddEquiv

Documentation

Package the preceding density argument as a linear equivalence.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
variable {A B : Type*}
variable [TopologicalSpace A] [TopologicalSpace B]
variable [AddCommMonoid A] [AddCommMonoid B]
variable [Module ℤ_[p] A] [Module ℤ_[p] B]
variable [ContinuousSMul ℤ_[p] A] [ContinuousSMul ℤ_[p] B]
variable [T2Space B]

Lean source · statement

def padicLinearEquivOfContinuousAddEquiv
    (e : A ≃+ B) (he : Continuous e) : A ≃ₗ[ℤ_[p]] B

theorem

continuous_padicInt_finPi_linearMap

L84 ↗

LocalFieldTheory.DiscreteValuationField.continuous_padicInt_finPi_linearMap

Documentation

Every Z_p-linear map from a finite Cartesian power of Z_p is continuous when the target has continuous addition and scalar multiplication. This is the elementary finite-basis continuity step used in the mixed-characteristic part of the field-unit structure theorem.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
variable {A B : Type*}
variable [TopologicalSpace A] [TopologicalSpace B]
variable [AddCommMonoid A] [AddCommMonoid B]
variable [Module ℤ_[p] A] [Module ℤ_[p] B]
variable [ContinuousSMul ℤ_[p] A] [ContinuousSMul ℤ_[p] B]
variable [T2Space B]

Lean source · statement

theorem continuous_padicInt_finPi_linearMap
    {M : Type*} [TopologicalSpace M] [AddCommMonoid M]
    [Module ℤ_[p] M] [ContinuousAdd M] [ContinuousSMul ℤ_[p] M]
    (d : ℕ) (f : (Fin d → ℤ_[p]) →ₗ[ℤ_[p]] M) : Continuous f

theorem

moduleFinite_of_surjective_of_ker

L111 ↗

LocalFieldTheory.DiscreteValuationField.moduleFinite_of_surjective_of_ker

Documentation

Finite generation across a short exact sequence, phrased for a surjective linear map. This avoids unfolding a large ambient module when a finite kernel and finite quotient are already available.

Source context 9 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
variable {A B : Type*}
variable [TopologicalSpace A] [TopologicalSpace B]
variable [AddCommMonoid A] [AddCommMonoid B]
variable [Module ℤ_[p] A] [Module ℤ_[p] B]
variable [ContinuousSMul ℤ_[p] A] [ContinuousSMul ℤ_[p] B]
variable [T2Space B]

Lean source · statement

theorem moduleFinite_of_surjective_of_ker
    {R M N : Type*} [Ring R]
    [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
    (f : M →ₗ[R] N) (hf : Function.Surjective f)
    [Module.Finite R N] [Module.Finite R (LinearMap.ker f)] :
    Module.Finite R M

Module documentation

Continuous additive maps of p-adic modules are p-adic linear

Declarations

continuousAddEquivOfMultiplicativeSource

continuousMulEquivOfAdditiveTarget

map_padicInt_smul_of_continuous

padicLinearEquivOfContinuousAddEquiv

continuous_padicInt_finPi_linearMap

moduleFinite_of_surjective_of_ker