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 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 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
, t3_space
, has_continuous_mul
) then follow.
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
- linear_ordered_comm_group_with_zero.nhds_fun Γ₀ x = ite (x = 0) (⨅ (γ₀ : Γ₀ˣ), filter.principal {γ : Γ₀ | γ < ↑γ₀}) (has_pure.pure x)
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.
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.
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.
The neighbourhood filter of an invertible element consists of all sets containing that element.
The neighbourhood filter of a nonzero element consists of all sets containing that element.
If γ is an invertible element of a linearly ordered group with zero element adjoined, then {γ} is a neighbourhood of γ.
If γ is a nonzero element of a linearly ordered group with zero element adjoined, then {γ} is a neighbourhood of γ.
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.
If γ is an invertible element of a linearly ordered group with zero element adjoined, then {x | x < γ} is a neighbourhood of 0.
If γ is a nonzero element of a linearly ordered group with zero element adjoined, then {x | x < γ} is a neighbourhood of 0.
The topology on a linearly ordered group with zero element adjoined is compatible with the order structure.
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.