# mathlibdocumentation

topology.algebra.with_zero_topology

# 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", but this fact is not proven here since the neighborhoods description is what is actually useful.

We prove this topology is ordered and regular (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 not defined as an instance since it may not be the desired topology on a linearly ordered commutative group with zero. You can locally activate this topology using local attribute [instance] linear_ordered_comm_group_with_zero.topological_space All other instances will (ordered_topology, regular_space, has_continuous_mul) then follow.

def linear_ordered_comm_group_with_zero.nhds_fun (Γ₀ : Type u_1) (x : Γ₀) :
filter Γ₀

The neighbourhoods around γ ∈ Γ₀, used in the definition of the topology on Γ₀. These neighbourhoods are defined as follows: A set s is a neighbourhood of 0 if there is an invertible γ₀ ∈ Γ₀ such that {γ | γ < γ₀} ⊆ s. If γ ≠ 0, then every set that contains γ is a neighbourhood of γ.

Equations
@[protected]

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
theorem linear_ordered_comm_group_with_zero.directed_lt (Γ₀ : Type u_1)  :
(λ (γ₀ : Γ₀ˣ), filter.principal {γ : Γ₀ | γ < γ₀})

The neighbourhoods {γ | γ < γ₀} of 0 form a directed set indexed by the invertible elements γ₀.

At all points of a linearly ordered commutative group with a zero element adjoined, the pure filter is smaller than the filter given by nhds_fun.

theorem linear_ordered_comm_group_with_zero.nhds_fun_ok (Γ₀ : Type u_1) (x : Γ₀) {s : set Γ₀} (s_in : s ) :
∃ (t : set Γ₀) (H : , t s ∀ (y : Γ₀), y t

For every point Γ₀, and every “neighbourhood” s of it (described by nhds_fun), there is a smaller “neighbourhood” t ⊆ s, such that s is a “neighbourhood“ of all the points in t.

theorem linear_ordered_comm_group_with_zero.nhds_coe_units {Γ₀ : Type u_1} (γ : Γ₀ˣ) :

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

@[simp]
theorem linear_ordered_comm_group_with_zero.nhds_of_ne_zero {Γ₀ : Type u_1} (γ : Γ₀) (h : γ 0) :

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

theorem linear_ordered_comm_group_with_zero.singleton_nhds_of_units {Γ₀ : Type u_1} (γ : Γ₀ˣ) :
{γ}

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

theorem linear_ordered_comm_group_with_zero.singleton_nhds_of_ne_zero {Γ₀ : Type u_1} (γ : Γ₀) (h : γ 0) :
{γ} nhds γ

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

theorem linear_ordered_comm_group_with_zero.has_basis_nhds_zero {Γ₀ : Type u_1}  :
(nhds 0).has_basis (λ (_x : Γ₀ˣ), true) (λ (γ₀ : Γ₀ˣ), {γ : Γ₀ | γ < γ₀})

If U is a neighbourhood of 0 in a linearly ordered group with zero element adjoined, then there exists an invertible element γ₀ such that {γ | γ < γ₀} ⊆ U.

theorem linear_ordered_comm_group_with_zero.nhds_zero_of_units {Γ₀ : Type u_1} (γ : Γ₀ˣ) :
{x : Γ₀ | x < γ} nhds 0

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

theorem linear_ordered_comm_group_with_zero.tendsto_zero {Γ₀ : Type u_1} {α : Type u_2} {F : filter α} {f : α → Γ₀} :
(nhds 0) ∀ (γ₀ : Γ₀ˣ), {x : α | f x < γ₀} F
theorem linear_ordered_comm_group_with_zero.nhds_zero_of_ne_zero {Γ₀ : Type u_1} (γ : Γ₀) (h : γ 0) :
{x : Γ₀ | x < γ} nhds 0

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

theorem linear_ordered_comm_group_with_zero.has_basis_nhds_units {Γ₀ : Type u_1} (γ : Γ₀ˣ) :
(nhds γ).has_basis (λ (i : unit), true) (λ (i : unit), {γ})
theorem linear_ordered_comm_group_with_zero.has_basis_nhds_of_ne_zero {Γ₀ : Type u_1} {x : Γ₀} (h : x 0) :
(nhds x).has_basis (λ (i : unit), true) (λ (i : unit), {x})
theorem linear_ordered_comm_group_with_zero.singleton_mem_nhds_of_ne_zero {Γ₀ : Type u_1} {x : Γ₀} (h : x 0) :
{x} nhds x
theorem linear_ordered_comm_group_with_zero.tendsto_units {Γ₀ : Type u_1} {α : Type u_2} {F : filter α} {f : α → Γ₀} {γ₀ : Γ₀ˣ} :
(nhds γ₀) {x : α | f x = γ₀} F
theorem linear_ordered_comm_group_with_zero.tendsto_of_ne_zero {Γ₀ : Type u_1} {α : Type u_2} {F : filter α} {f : α → Γ₀} {γ : Γ₀} (h : γ 0) :
(nhds γ) {x : α | f x = γ} F
@[protected, instance]

The topology on a linearly ordered group with zero element adjoined is compatible with the order structure.

@[protected, instance]

The topology on a linearly ordered group with zero element adjoined is T₃ (aka regular).

@[protected, instance]

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