# 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.

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), )
Instances For
theorem WithZeroTopology.nhds_eq_update {Γ₀ : Type u_2} :
nhds = Function.update pure 0 (⨅ (γ : Γ₀), ⨅ (_ : γ 0), )

### Neighbourhoods of zero #

theorem WithZeroTopology.nhds_zero {Γ₀ : Type u_2} :
nhds 0 = ⨅ (γ : Γ₀), ⨅ (_ : γ 0),
theorem WithZeroTopology.hasBasis_nhds_zero {Γ₀ : Type u_2} :
(nhds 0).HasBasis (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} {γ : Γ₀} (hγ : γ 0) :
theorem WithZeroTopology.nhds_zero_of_units {Γ₀ : Type u_2} (γ : Γ₀ˣ) :
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} {l : } {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} {γ : Γ₀} (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} (γ : Γ₀ˣ) :
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} (γ : Γ₀ˣ) :
{γ} 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} {γ : Γ₀} (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} {x : Γ₀} (h : x 0) :
(nhds x).HasBasis (fun (x : Unit) => True) fun (x_1 : Unit) => {x}
theorem WithZeroTopology.hasBasis_nhds_units {Γ₀ : Type u_2} (γ : Γ₀ˣ) :
(nhds γ).HasBasis (fun (x : Unit) => True) fun (x : Unit) => {γ}
theorem WithZeroTopology.tendsto_of_ne_zero {α : Type u_1} {Γ₀ : Type u_2} {l : } {f : αΓ₀} {γ : Γ₀} (h : γ 0) :
Filter.Tendsto f l (nhds γ) ∀ᶠ (x : α) in l, f x = γ
theorem WithZeroTopology.tendsto_units {α : Type u_1} {Γ₀ : Type u_2} {l : } {f : αΓ₀} {γ₀ : Γ₀ˣ} :
Filter.Tendsto f l (nhds γ₀) ∀ᶠ (x : α) in l, f x = γ₀
theorem WithZeroTopology.Iio_mem_nhds {Γ₀ : Type u_2} {γ₁ : Γ₀} {γ₂ : Γ₀} (h : γ₁ < γ₂) :
Set.Iio γ₂ nhds γ₁

### Open/closed sets #

theorem WithZeroTopology.isOpen_iff {Γ₀ : Type u_2} {s : Set Γ₀} :
0s ∃ (γ : Γ₀), γ 0 s
theorem WithZeroTopology.isClosed_iff {Γ₀ : Type u_2} {s : Set Γ₀} :
0 s ∃ (γ : Γ₀), γ 0 s
theorem WithZeroTopology.isOpen_Iio {Γ₀ : Type u_2} {a : Γ₀} :

### Instances #

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
• =
Instances For
def WithZeroTopology.t5Space {Γ₀ : Type u_2} :
T5Space Γ₀

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

Equations
• =
Instances For
@[deprecated WithZeroTopology.t5Space]
theorem WithZeroTopology.t3Space {Γ₀ : Type u_2} :
T3Space Γ₀

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

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

Equations
• =
Instances For
Equations
• =
Instances For