mathlib3 documentation

topology.algebra.with_zero_topology

The topology on linearly ordered commutative groups with zero #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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", see linear_ordered_comm_group_with_zero.is_open_iff.

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 a global instance since it may not be the desired topology on a linearly ordered commutative group with zero. You can locally activate this topology using open_locale with_zero_topology.

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

Neighbourhoods of zero #

theorem with_zero_topology.nhds_zero {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] :
nhds 0 = (γ : Γ₀) (H : γ 0), filter.principal (set.Iio γ)
theorem with_zero_topology.has_basis_nhds_zero {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] :
(nhds 0).has_basis (λ (γ : Γ₀), γ 0) set.Iio

In a linearly ordered group with zero element adjoined, U is a neighbourhood of 0 if and only if there exists a nonzero element γ₀ such that Iio γ₀ ⊆ U.

theorem with_zero_topology.Iio_mem_nhds_zero {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {γ : Γ₀} (hγ : γ 0) :

If γ is an invertible element of a linearly ordered group with zero element adjoined, then Iio (γ : Γ₀) is a neighbourhood of 0.

theorem with_zero_topology.tendsto_zero {α : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {l : filter α} {f : α Γ₀} :
filter.tendsto f l (nhds 0) (γ₀ : Γ₀), γ₀ 0 (∀ᶠ (x : α) in l, f x < γ₀)

Neighbourhoods of non-zero elements #

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

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

The neighbourhood filter of an invertible 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 with_zero_topology.singleton_mem_nhds_of_ne_zero {Γ₀ : Type u_2} [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 with_zero_topology.has_basis_nhds_of_ne_zero {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {x : Γ₀} (h : x 0) :
(nhds x).has_basis (λ (i : unit), true) (λ (i : unit), {x})
theorem with_zero_topology.has_basis_nhds_units {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] (γ : Γ₀ˣ) :
(nhds γ).has_basis (λ (i : unit), true) (λ (i : unit), {γ})
theorem with_zero_topology.tendsto_of_ne_zero {α : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {l : filter α} {f : α Γ₀} {γ : Γ₀} (h : γ 0) :
filter.tendsto f l (nhds γ) ∀ᶠ (x : α) in l, f x = γ
theorem with_zero_topology.tendsto_units {α : Type u_1} {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {l : filter α} {f : α Γ₀} {γ₀ : Γ₀ˣ} :
filter.tendsto f l (nhds γ₀) ∀ᶠ (x : α) in l, f x = γ₀
theorem with_zero_topology.Iio_mem_nhds {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {γ₁ γ₂ : Γ₀} (h : γ₁ < γ₂) :
set.Iio γ₂ nhds γ₁

Open/closed sets #

theorem with_zero_topology.is_open_iff {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {s : set Γ₀} :
is_open s 0 s (γ : Γ₀) (H : γ 0), set.Iio γ s
theorem with_zero_topology.is_closed_iff {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {s : set Γ₀} :
is_closed s 0 s (γ : Γ₀) (H : γ 0), s set.Ici γ

Instances #

@[protected]

The topology on a linearly ordered group with zero element adjoined is compatible with the order structure: the set {p : Γ₀ × Γ₀ | p.1 ≤ p.2} is closed.

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

@[protected]

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