Documentation

Mathlib.Topology.Algebra.WithZeroTopology

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", see WithZeroTopology.isOpen_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 defined as a scoped 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 WithZeroTopology.

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
Instances For
    theorem WithZeroTopology.nhds_eq_update {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] :
    nhds = Function.update pure 0 (⨅ (γ : Γ₀), ⨅ (_ : γ 0), Filter.principal (Set.Iio γ))

    Neighbourhoods of zero #

    theorem WithZeroTopology.nhds_zero {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] :
    nhds 0 = ⨅ (γ : Γ₀), ⨅ (_ : γ 0), Filter.principal (Set.Iio γ)
    theorem WithZeroTopology.hasBasis_nhds_zero {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] :
    (nhds 0).HasBasis (fun (γ : Γ₀) => γ 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 WithZeroTopology.Iio_mem_nhds_zero {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {γ : Γ₀} (hγ : γ 0) :
    theorem WithZeroTopology.nhds_zero_of_units {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ) :
    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 WithZeroTopology.tendsto_zero {α : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {l : Filter α} {f : αΓ₀} :
    Filter.Tendsto f l (nhds 0) ∀ (γ₀ : Γ₀), γ₀ 0∀ᶠ (x : α) in l, f x < γ₀

    Neighbourhoods of non-zero elements #

    @[simp]
    theorem WithZeroTopology.nhds_of_ne_zero {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {γ : Γ₀} (h₀ : γ 0) :
    nhds γ = pure γ

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

    theorem WithZeroTopology.nhds_coe_units {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ) :
    nhds γ = pure γ

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

    theorem WithZeroTopology.singleton_mem_nhds_of_units {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ) :
    {γ} nhds γ

    If γ is an invertible element of a linearly ordered group with zero element adjoined, then {γ} is a neighbourhood of γ.

    theorem WithZeroTopology.singleton_mem_nhds_of_ne_zero {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {γ : Γ₀} (h : γ 0) :
    {γ} nhds γ

    If γ is a nonzero element of a linearly ordered group with zero element adjoined, then {γ} is a neighbourhood of γ.

    theorem WithZeroTopology.hasBasis_nhds_of_ne_zero {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {x : Γ₀} (h : x 0) :
    (nhds x).HasBasis (fun (x : Unit) => True) fun (x_1 : Unit) => {x}
    theorem WithZeroTopology.hasBasis_nhds_units {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ) :
    (nhds γ).HasBasis (fun (x : Unit) => True) fun (x : Unit) => {γ}
    theorem WithZeroTopology.tendsto_of_ne_zero {α : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {l : Filter α} {f : αΓ₀} {γ : Γ₀} (h : γ 0) :
    Filter.Tendsto f l (nhds γ) ∀ᶠ (x : α) in l, f x = γ
    theorem WithZeroTopology.tendsto_units {α : Type u_1} {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {l : Filter α} {f : αΓ₀} {γ₀ : Γ₀ˣ} :
    Filter.Tendsto f l (nhds γ₀) ∀ᶠ (x : α) in l, f x = γ₀
    theorem WithZeroTopology.Iio_mem_nhds {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {γ₁ : Γ₀} {γ₂ : Γ₀} (h : γ₁ < γ₂) :
    Set.Iio γ₂ nhds γ₁

    Open/closed sets #

    theorem WithZeroTopology.isOpen_iff {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {s : Set Γ₀} :
    IsOpen s 0s ∃ (γ : Γ₀), γ 0 Set.Iio γ s
    theorem WithZeroTopology.isClosed_iff {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {s : Set Γ₀} :
    IsClosed s 0 s ∃ (γ : Γ₀), γ 0 s Set.Ici γ

    Instances #

    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.

    Equations
    • =
    Instances For

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

      Equations
      • =
      Instances For

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

        Equations
        • =
        Instances For