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]

def with_zero_topology.topological_space {Γ₀ : Type u_2} [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

with_zero_topology.topological_space = topological_space.mk_of_nhds (function.update has_pure.pure 0 (⨅ (γ : Γ₀) (H : γ ≠ 0), filter.principal (set.Iio γ)))

theorem with_zero_topology.nhds_eq_update {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] :

nhds = function.update has_pure.pure 0 (⨅ (γ : Γ₀) (H : γ ≠ 0), filter.principal (set.Iio γ))

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

set.Iio γ ∈ nhds 0

theorem with_zero_topology.nhds_zero_of_units {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] (γ : Γ₀ˣ) :

set.Iio ↑γ ∈ nhds 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) :

nhds γ = has_pure.pure γ

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

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

nhds ↑γ = has_pure.pure ↑γ

The neighbourhood filter of an invertible element consists of all sets containing that element.

theorem with_zero_topology.singleton_mem_nhds_of_units {Γ₀ : Type u_2} [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 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 γ

theorem with_zero_topology.is_open_Iio {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] {a : Γ₀} :

is_open (set.Iio a)

Instances #

@[protected]

theorem with_zero_topology.order_closed_topology {Γ₀ : Type u_2} [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: the set {p : Γ₀ × Γ₀ | p.1 ≤ p.2} is closed.

theorem with_zero_topology.t3_space {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] :

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

@[protected]

theorem with_zero_topology.has_continuous_mul {Γ₀ : Type u_2} [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.

@[protected]

theorem with_zero_topology.has_continuous_inv₀ {Γ₀ : Type u_2} [linear_ordered_comm_group_with_zero Γ₀] :

has_continuous_inv₀ Γ₀