Mathlib.Topology.Algebra.Order.Archimedean

Module docstring

{"# Topology on archimedean groups and fields

In this file we prove the following theorems:

Rat.denseRange_cast: the coercion from ℚ to a linear ordered archimedean field has dense range;
AddSubgroup.dense_of_not_isolated_zero, AddSubgroup.dense_of_no_min: two sufficient conditions for a subgroup of an archimedean linear ordered additive commutative group to be dense;
AddSubgroup.dense_or_cyclic: an additive subgroup of an archimedean linear ordered additive commutative group G with order topology either is dense in G or is a cyclic subgroup. "}

Rat.denseRange_cast theorem

 {𝕜} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [Archimedean 𝕜] :
  DenseRange ((↑) : ℚ → 𝕜)

Full source

/-- Rational numbers are dense in a linear ordered archimedean field. -/
theorem Rat.denseRange_cast {𝕜} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
    [TopologicalSpace 𝕜] [OrderTopology 𝕜]
    [Archimedean 𝕜] : DenseRange ((↑) : ℚ → 𝕜) :=
  dense_of_exists_between fun _ _ h => Set.exists_range_iff.2 <| exists_rat_btwn h

Density of Rationals in Archimedean Fields

Informal description

Let $\mathbb{K}$ be a linear ordered archimedean field equipped with the order topology. Then the canonical embedding of the rational numbers $\mathbb{Q}$ into $\mathbb{K}$ has dense range, i.e., the set $\{q \in \mathbb{Q} \mid q \text{ embedded in } \mathbb{K}\}$ is dense in $\mathbb{K}$.

Subgroup.dense_of_not_isolated_one theorem

(S : Subgroup G) (hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε) : Dense (S : Set G)

Full source

/-- A subgroup of an archimedean linear ordered multiplicative commutative group with order
topology is dense provided that for all `ε > 1` there exists an element of the subgroup
that belongs to `(1, ε)`. -/
@[to_additive "An additive subgroup of an archimedean linear ordered additive commutative group with
order topology is dense provided that for all positive `ε` there exists a positive element of the
subgroup that is less than `ε`."]
theorem dense_of_not_isolated_one (S : Subgroup G) (hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε) :
    Dense (S : Set G) := by
  cases subsingleton_or_nontrivial G
  · refine fun x => _root_.subset_closure ?_
    rw [Subsingleton.elim x 1]
    exact one_mem S
  refine dense_of_exists_between fun a b hlt => ?_
  rcases hS (b / a) (one_lt_div'.2 hlt) with ⟨g, hgS, hg0, hg⟩
  rcases (existsUnique_add_zpow_mem_Ioc hg0 1 a).exists with ⟨m, hm⟩
  rw [one_mul] at hm
  refine ⟨g ^ m, zpow_mem hgS _, hm.1, hm.2.trans_lt ?_⟩
  rwa [lt_div_iff_mul_lt'] at hg

Density of Subgroup with Elements Arbitrarily Close to One

Informal description

Let $G$ be a linearly ordered commutative group with order topology, and let $S$ be a subgroup of $G$. If for every $\varepsilon > 1$ there exists an element $g \in S$ such that $1 < g < \varepsilon$, then $S$ is dense in $G$.

Subgroup.dense_of_no_min theorem

(S : Subgroup G) (hbot : S ≠ ⊥) (H : ¬∃ a : G, IsLeast {g : G | g ∈ S ∧ 1 < g} a) : Dense (S : Set G)

Full source

/-- Let `S` be a nontrivial subgroup in an archimedean linear ordered multiplicative commutative
group `G` with order topology. If the set of elements of `S` that are greater than one
 does not have a minimal element, then `S` is dense `G`. -/
@[to_additive "Let `S` be a nontrivial additive subgroup in an archimedean linear ordered additive
commutative group `G` with order topology. If the set of positive elements of `S` does not have a
minimal element, then `S` is dense `G`."]
theorem dense_of_no_min (S : Subgroup G) (hbot : S ≠ ⊥)
    (H : ¬∃ a : G, IsLeast { g : G | g ∈ S ∧ 1 < g } a) : Dense (S : Set G) := by
  refine S.dense_of_not_isolated_one fun ε ε1 => ?_
  contrapose! H
  exact exists_isLeast_one_lt hbot ε1 (disjoint_left.2 H)

Density of Subgroups Without Minimal Elements Above One in Archimedean Ordered Groups

Informal description

Let $G$ be a linearly ordered archimedean commutative group with order topology, and let $S$ be a nontrivial subgroup of $G$. If the set $\{g \in S \mid 1 < g\}$ does not have a minimal element, then $S$ is dense in $G$.

Subgroup.dense_or_cyclic theorem

(S : Subgroup G) : Dense (S : Set G) ∨ ∃ a : G, S = closure { a }

Full source

/-- A subgroup of an archimedean linear ordered multiplicative commutative group `G` with order
topology either is dense in `G` or is a cyclic subgroup. -/
@[to_additive dense_or_cyclic
 "An additive subgroup of an archimedean linear ordered additive commutative group `G`
with order topology either is dense in `G` or is a cyclic subgroup."]
theorem dense_or_cyclic (S : Subgroup G) : DenseDense (S : Set G) ∨ ∃ a : G, S = closure {a} := by
  refine (em _).imp (dense_of_not_isolated_one S) fun h => ?_
  push_neg at h
  rcases h with ⟨ε, ε1, hε⟩
  exact cyclic_of_isolated_one ε1 (disjoint_left.2 hε)

Density or Cyclicity of Subgroups in Ordered Commutative Groups

Informal description

Let $G$ be a linearly ordered commutative group with order topology, and let $S$ be a subgroup of $G$. Then either $S$ is dense in $G$, or there exists an element $a \in G$ such that $S$ is the cyclic subgroup generated by $a$.

Subgroup.dense_xor'_cyclic theorem

(s : Subgroup G) : Xor' (Dense (s : Set G)) (∃ a, s = .zpowers a)

Full source

/-- In a nontrivial densely linear ordered archimedean topological multiplicative group,
a subgroup is either dense or is cyclic, but not both.

For a non-exclusive `Or` version with weaker assumptions,
see `Subgroup.dense_or_cyclic` above. -/
@[to_additive dense_xor'_cyclic
 "In a nontrivial densely linear ordered archimedean topological additive group,
a subgroup is either dense or is cyclic, but not both.

For a non-exclusive `Or` version with weaker assumptions, see `AddSubgroup.dense_or_cyclic` above."]
theorem dense_xor'_cyclic (s : Subgroup G) :
    Xor' (Dense (s : Set G)) (∃ a, s = .zpowers a) := by
  if hd : Dense (s : Set G) then
    simp only [hd, xor_true]
    rintro ⟨a, rfl⟩
    exact not_denseRange_zpow hd
  else
    simp only [hd, xor_false, id, zpowers_eq_closure]
    exact s.dense_or_cyclic.resolve_left hd

Density or Cyclicity of Subgroups in Archimedean Ordered Groups (Exclusive Version)

Informal description

Let $G$ be a nontrivial densely linearly ordered archimedean topological commutative group. For any subgroup $S$ of $G$, exactly one of the following holds: 1. $S$ is dense in $G$, or 2. $S$ is a cyclic subgroup (i.e., there exists $a \in G$ such that $S = \{a^n \mid n \in \mathbb{Z}\}$).

Subgroup.dense_iff_ne_zpowers theorem

{s : Subgroup G} : Dense (s : Set G) ↔ ∀ a, s ≠ .zpowers a

Full source

@[to_additive]
theorem dense_iff_ne_zpowers {s : Subgroup G} :
    DenseDense (s : Set G) ↔ ∀ a, s ≠ .zpowers a := by
  simp [xor_iff_iff_not.1 s.dense_xor'_cyclic]

Density of Subgroup in Archimedean Ordered Group is Equivalent to Non-Cyclicity

Informal description

Let $G$ be a nontrivial densely linearly ordered archimedean topological commutative group. For any subgroup $S$ of $G$, the following are equivalent: 1. $S$ is dense in $G$. 2. For every element $a \in G$, the subgroup $S$ is not equal to the cyclic subgroup generated by $a$ (i.e., $S \neq \{a^n \mid n \in \mathbb{Z}\}$ for any $a \in G$).