mathlib documentation

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.

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) [linear_ordered_comm_group_with_zero Γ₀] :
directed ge (λ (γ₀ : units Γ₀), 𝓟 {γ : Γ₀ | γ < γ₀})

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) [linear_ordered_comm_group_with_zero Γ₀] (x : Γ₀) {s : set Γ₀} (s_in : s linear_ordered_comm_group_with_zero.nhds_fun Γ₀ x) :
∃ (t : set Γ₀) (H : t linear_ordered_comm_group_with_zero.nhds_fun Γ₀ x), t s ∀ (y : Γ₀), y ts linear_ordered_comm_group_with_zero.nhds_fun Γ₀ y

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.

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

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

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

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} [linear_ordered_comm_group_with_zero Γ₀] :
(𝓝 0).has_basis (λ (_x : units Γ₀), true) (λ (γ₀ : units Γ₀), {γ : Γ₀ | γ < γ₀})

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} [linear_ordered_comm_group_with_zero Γ₀] (γ : units Γ₀) :
{x : Γ₀ | x < γ} 𝓝 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} [linear_ordered_comm_group_with_zero Γ₀] {α : Type u_2} {F : filter α} {f : α → Γ₀} :
filter.tendsto f F (𝓝 0) ∀ (γ₀ : units Γ₀), {x : α | f x < γ₀} F
theorem linear_ordered_comm_group_with_zero.nhds_zero_of_ne_zero {Γ₀ : Type u_1} [linear_ordered_comm_group_with_zero Γ₀] (γ : Γ₀) (h : γ 0) :
{x : Γ₀ | x < γ} 𝓝 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} [linear_ordered_comm_group_with_zero Γ₀] (γ : units Γ₀) :
(𝓝 γ).has_basis (λ (i : unit), true) (λ (i : unit), {γ})
theorem linear_ordered_comm_group_with_zero.has_basis_nhds_of_ne_zero {Γ₀ : Type u_1} [linear_ordered_comm_group_with_zero Γ₀] {x : Γ₀} (h : x 0) :
(𝓝 x).has_basis (λ (i : unit), true) (λ (i : unit), {x})
theorem linear_ordered_comm_group_with_zero.tendsto_units {Γ₀ : Type u_1} [linear_ordered_comm_group_with_zero Γ₀] {α : Type u_2} {F : filter α} {f : α → Γ₀} {γ₀ : units Γ₀} :
filter.tendsto f F (𝓝 γ₀) {x : α | f x = γ₀} F
theorem linear_ordered_comm_group_with_zero.tendsto_of_ne_zero {Γ₀ : Type u_1} [linear_ordered_comm_group_with_zero Γ₀] {α : Type u_2} {F : filter α} {f : α → Γ₀} {γ : Γ₀} (h : γ 0) :
filter.tendsto f F (𝓝 γ) {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.