Definition of (Non-archimedean) local fields

Given a topological field K equipped with an equivalence class of valuations (a ValuativeRel), we say that it is a non-archimedean local field if the topology comes from the given valuation, and it is locally compact and non-discrete.

class IsNonarchimedeanLocalField (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] extends IsValuativeTopology K, LocallyCompactSpace K, ValuativeRel.IsNontrivial K : Prop

Given a topological field K equipped with an equivalence class of valuations (a ValuativeRel), we say that it is a non-archimedean local field if the topology comes from the given valuation, and it is locally compact and non-discrete.

This implies the following typeclasses via inferInstance

• IsValuativeTopology K
• LocallyCompactSpace K
• IsTopologicalDivisionRing K
• ValuativeRel.IsNontrivial K
• ValuativeRel.IsRankLeOne K
• ValuativeRel.IsDiscrete K
• IsDiscreteValuationRing 𝒪[K]
• Finite 𝓀[K]

Assuming we have a compatible UniformSpace K instance (e.g. via IsTopologicalAddGroup.toUniformSpace and isUniformAddGroup_of_addCommGroup) then

• CompleteSpace K
• CompleteSpace 𝒪[K]

• mem_nhds_iff {s : Set K} {x : K} : s ∈ nhds x ↔ ∃ (γ : (ValuativeRel.ValueGroupWithZero K)ˣ), (fun (x_1 : K) => x + x_1) '' {z : K | (ValuativeRel.valuation K) z < ↑γ} ⊆ s
• local_compact_nhds (x : K) (n : Set K) : n ∈ nhds x → ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s
• condition : ∃ (γ : ValueGroupWithZero K), γ ≠ 0 ∧ γ ≠ 1

instance IsNonarchimedeanLocalField.instIsTopologicalDivisionRing (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsTopologicalDivisionRing K

theorem IsNonarchimedeanLocalField.isCompact_closedBall (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (γ : ValuativeRel.ValueGroupWithZero K) : IsCompact {x : K | (ValuativeRel.valuation K) x ≤ γ}

instance IsNonarchimedeanLocalField.instCompactSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : CompactSpace ↥(ValuativeRel.valuation K).integer

instance IsNonarchimedeanLocalField.instCompatibleValueGroupWithZeroV (K : Type u_2) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsValuativeTopology K] : Valued.v.Compatible

instance IsNonarchimedeanLocalField.instIsDiscreteValuationRingSubtypeMemSubringIntegerValueGroupWithZeroValuation (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsDiscreteValuationRing ↥(ValuativeRel.valuation K).integer

noncomputable def IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : ValuativeRel.ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ)

The value group of a local field is (uniquely) isomorphic to ℤᵐ⁰.

Equations

• IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt K = ⋯.some

instance IsNonarchimedeanLocalField.instIsDiscrete (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : ValuativeRel.IsDiscrete K

instance IsNonarchimedeanLocalField.instIsRankLeOne (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : ValuativeRel.IsRankLeOne K

instance IsNonarchimedeanLocalField.instFiniteResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Finite (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

instance IsNonarchimedeanLocalField.instCompleteSpace (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] : CompleteSpace K

instance IsNonarchimedeanLocalField.instCompleteSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] : CompleteSpace ↥(ValuativeRel.valuation K).integer