The topology on linearly ordered commutative groups with zero

Let Γ₀ be a linearly ordered commutative group to which we have adjoined a zero element. Then Γ₀ may naturally be endowed with a topology that turns Γ₀ into a topological monoid. Neighborhoods of zero are sets containing { γ | γ < γ₀ } for some invertible element γ₀ and every invertible element is open. In particular the topology is the following: "a subset U ⊆ Γ₀ is open if 0 ∉ U or if there is an invertible γ₀ ∈ Γ₀ such that { γ | γ < γ₀ } ⊆ U", see WithZeroTopology.isOpen_iff.

We prove this topology is ordered and T₅ (in addition to be compatible with the monoid structure).

All this is useful to extend a valuation to a completion. This is an abstract version of how the absolute value (resp. p-adic absolute value) on ℚ is extended to ℝ (resp. ℚₚ).

Implementation notes

This topology is defined as a scoped instance since it may not be the desired topology on a linearly ordered commutative group with zero. You can locally activate this topology using open WithZeroTopology.

def WithZeroTopology.topologicalSpace {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] : TopologicalSpace Γ₀

The topology on a linearly ordered commutative group with a zero element adjoined. A subset U is open if 0 ∉ U or if there is an invertible element γ₀ such that {γ | γ < γ₀} ⊆ U.

Equations

• WithZeroTopology.topologicalSpace = nhdsAdjoint 0 (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), Filter.principal (Set.Iio γ))

theorem WithZeroTopology.nhds_eq_update {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] : nhds = Function.update pure 0 (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), Filter.principal (Set.Iio γ))

Neighbourhoods of zero

theorem WithZeroTopology.nhds_zero {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] : nhds 0 = ⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), Filter.principal (Set.Iio γ)

theorem WithZeroTopology.hasBasis_nhds_zero {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] : Filter.HasBasis (nhds 0) (fun (γ : Γ₀) => γ ≠ 0) Set.Iio

In a linearly ordered group with zero element adjoined, U is a neighbourhood of 0 if and only if there exists a nonzero element γ₀ such that Iio γ₀ ⊆ U.

theorem WithZeroTopology.Iio_mem_nhds_zero {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {γ : Γ₀} (hγ : γ ≠ 0) : Set.Iio γ ∈ nhds 0

theorem WithZeroTopology.nhds_zero_of_units {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ) : Set.Iio ↑γ ∈ nhds 0

If γ is an invertible element of a linearly ordered group with zero element adjoined, then Iio (γ : Γ₀) is a neighbourhood of 0.

theorem WithZeroTopology.tendsto_zero {α : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {l : Filter α} {f : α → Γ₀} : Filter.Tendsto f l (nhds 0) ↔ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : α) in l, f x < γ₀

Neighbourhoods of non-zero elements

@[simp]

theorem WithZeroTopology.nhds_of_ne_zero {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {γ : Γ₀} (h₀ : γ ≠ 0) : nhds γ = pure γ

The neighbourhood filter of a nonzero element consists of all sets containing that element.

theorem WithZeroTopology.nhds_coe_units {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ) : nhds ↑γ = pure ↑γ

The neighbourhood filter of an invertible element consists of all sets containing that element.

theorem WithZeroTopology.singleton_mem_nhds_of_units {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ) : {↑γ} ∈ nhds ↑γ

If γ is an invertible element of a linearly ordered group with zero element adjoined, then {γ} is a neighbourhood of γ.

theorem WithZeroTopology.singleton_mem_nhds_of_ne_zero {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {γ : Γ₀} (h : γ ≠ 0) : {γ} ∈ nhds γ

If γ is a nonzero element of a linearly ordered group with zero element adjoined, then {γ} is a neighbourhood of γ.

theorem WithZeroTopology.hasBasis_nhds_of_ne_zero {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {x : Γ₀} (h : x ≠ 0) : Filter.HasBasis (nhds x) (fun (x : Unit) => True) fun (x_1 : Unit) => {x}

theorem WithZeroTopology.hasBasis_nhds_units {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ) : Filter.HasBasis (nhds ↑γ) (fun (x : Unit) => True) fun (x : Unit) => {↑γ}

theorem WithZeroTopology.tendsto_of_ne_zero {α : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {l : Filter α} {f : α → Γ₀} {γ : Γ₀} (h : γ ≠ 0) : Filter.Tendsto f l (nhds γ) ↔ ∀ᶠ (x : α) in l, f x = γ

theorem WithZeroTopology.tendsto_units {α : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {l : Filter α} {f : α → Γ₀} {γ₀ : Γ₀ˣ} : Filter.Tendsto f l (nhds ↑γ₀) ↔ ∀ᶠ (x : α) in l, f x = ↑γ₀

theorem WithZeroTopology.Iio_mem_nhds {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {γ₁ : Γ₀} {γ₂ : Γ₀} (h : γ₁ < γ₂) : Set.Iio γ₂ ∈ nhds γ₁

Open/closed sets

theorem WithZeroTopology.isOpen_iff {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {s : Set Γ₀} : IsOpen s ↔ 0 ∉ s ∨ ∃ (γ : Γ₀), γ ≠ 0 ∧ Set.Iio γ ⊆ s

theorem WithZeroTopology.isClosed_iff {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {s : Set Γ₀} : IsClosed s ↔ 0 ∈ s ∨ ∃ (γ : Γ₀), γ ≠ 0 ∧ s ⊆ Set.Ici γ

theorem WithZeroTopology.isOpen_Iio {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {a : Γ₀} : IsOpen (Set.Iio a)

Instances

def WithZeroTopology.orderClosedTopology {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] : OrderClosedTopology Γ₀

The topology on a linearly ordered group with zero element adjoined is compatible with the order structure: the set {p : Γ₀ × Γ₀ | p.1 ≤ p.2} is closed.

Equations

• ⋯ = ⋯

def WithZeroTopology.t5Space {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] : T5Space Γ₀

The topology on a linearly ordered group with zero element adjoined is T₅.

Equations

• ⋯ = ⋯

@[deprecated WithZeroTopology.t5Space]

theorem WithZeroTopology.t3Space {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] : T3Space Γ₀

The topology on a linearly ordered group with zero element adjoined is T₃.

def WithZeroTopology.instContinuousMulTopologicalSpaceToMulToMulZeroClassToMulZeroOneClassToMonoidWithZeroToGroupWithZeroToCommGroupWithZero {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] : ContinuousMul Γ₀

The topology on a linearly ordered group with zero element adjoined makes it a topological monoid.

Equations

• ⋯ = ⋯

def WithZeroTopology.instHasContinuousInv₀ToZeroToLinearOrderedCommMonoidWithZeroToInvTopologicalSpace {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] : HasContinuousInv₀ Γ₀

Equations

• ⋯ = ⋯