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

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) (⨅ (γ₀ : Γ₀ˣ), filter.principal {γ : Γ₀ | γ < ↑γ₀}) (has_pure.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 (λ (γ₀ : Γ₀ˣ), filter.principal {γ : Γ₀ | γ < ↑γ₀})

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 Γ₀] :

has_pure.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 Γ₀] (γ : Γ₀ˣ) :

nhds ↑γ = has_pure.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) :

nhds γ = has_pure.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 Γ₀] (γ : Γ₀ˣ) :

{↑γ} ∈ nhds ↑γ

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) :

{γ} ∈ 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} [linear_ordered_comm_group_with_zero Γ₀] :

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

{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} [linear_ordered_comm_group_with_zero Γ₀] {α : Type u_2} {F : filter α} {f : α → Γ₀} :

filter.tendsto f F (nhds 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 < γ} ∈ 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} [linear_ordered_comm_group_with_zero Γ₀] (γ : Γ₀ˣ) :

(nhds ↑γ).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) :

(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} [linear_ordered_comm_group_with_zero Γ₀] {x : Γ₀} (h : x ≠ 0) :

{x} ∈ nhds 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 (nhds ↑γ₀) ↔ {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 (nhds γ) ↔ {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.t3_space (Γ₀ : Type u_1) [linear_ordered_comm_group_with_zero Γ₀] :

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

@[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.