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.

def linear_ordered_comm_group_with_zero.nhds_fun (Γ₀ : Type u_1) [linear_ordered_comm_group_with_zero Γ₀] (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

linear_ordered_comm_group_with_zero.nhds_fun Γ₀ x = ite (x = 0) (⨅ (γ₀ : Γ₀ˣ), 𝓟 {γ : Γ₀ | γ < ↑γ₀}) (pure x)

@[protected]

def linear_ordered_comm_group_with_zero.topological_space (Γ₀ : Type u_1) [linear_ordered_comm_group_with_zero Γ₀] :

topological_space Γ₀

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

linear_ordered_comm_group_with_zero.topological_space Γ₀ = topological_space.mk_of_nhds (linear_ordered_comm_group_with_zero.nhds_fun Γ₀)

theorem linear_ordered_comm_group_with_zero.directed_lt (Γ₀ : Type u_1) [linear_ordered_comm_group_with_zero Γ₀] :

directed ge (λ (γ₀ : Γ₀ˣ), 𝓟 {γ : Γ₀ | γ < ↑γ₀})

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

theorem linear_ordered_comm_group_with_zero.pure_le_nhds_fun (Γ₀ : Type u_1) [linear_ordered_comm_group_with_zero Γ₀] :

pure ≤ linear_ordered_comm_group_with_zero.nhds_fun Γ₀

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 ∈ t → s ∈ 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.

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

𝓝 ↑γ = pure ↑γ

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.

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

{↑γ} ∈ 𝓝 ↑γ

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 : Γ₀ˣ), 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} [linear_ordered_comm_group_with_zero Γ₀] (γ : Γ₀ˣ) :

{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) ↔ ∀ (γ₀ : Γ₀ˣ), {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 Γ₀] (γ : Γ₀ˣ) :

(𝓝 ↑γ).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 : α → Γ₀} {γ₀ : Γ₀ˣ} :

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]

def linear_ordered_comm_group_with_zero.ordered_topology (Γ₀ : Type u_1) [linear_ordered_comm_group_with_zero Γ₀] :

order_closed_topology Γ₀

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

@[protected, instance]

def linear_ordered_comm_group_with_zero.regular_space (Γ₀ : Type u_1) [linear_ordered_comm_group_with_zero Γ₀] :

regular_space Γ₀

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

@[protected, instance]

def linear_ordered_comm_group_with_zero.has_continuous_mul (Γ₀ : Type u_1) [linear_ordered_comm_group_with_zero Γ₀] :

has_continuous_mul Γ₀

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