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.

theorem Rat.denseRange_cast {𝕜 : Type u_1} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [Archimedean 𝕜] : DenseRange Rat.cast

Rational numbers are dense in a linear ordered archimedean field.

theorem Subgroup.dense_of_not_isolated_one {G : Type u_1} [LinearOrderedCommGroup G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] (S : Subgroup G) (hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Set.Ioo 1 ε) : Dense ↑S

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, ε).

theorem AddSubgroup.dense_of_not_isolated_zero {G : Type u_1} [LinearOrderedAddCommGroup G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] (S : AddSubgroup G) (hS : ∀ ε > 0, ∃ g ∈ S, g ∈ Set.Ioo 0 ε) : Dense ↑S

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 Subgroup.dense_of_no_min {G : Type u_1} [LinearOrderedCommGroup G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] (S : Subgroup G) (hbot : S ≠ ⊥) (H : ¬∃ (a : G), IsLeast {g : G | g ∈ S ∧ 1 < g} a) : Dense ↑S

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.

theorem AddSubgroup.dense_of_no_min {G : Type u_1} [LinearOrderedAddCommGroup G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] (S : AddSubgroup G) (hbot : S ≠ ⊥) (H : ¬∃ (a : G), IsLeast {g : G | g ∈ S ∧ 0 < g} a) : Dense ↑S

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 Subgroup.dense_or_cyclic {G : Type u_1} [LinearOrderedCommGroup G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] (S : Subgroup G) : Dense ↑S ∨ ∃ (a : G), S = closure {a}

A subgroup of an archimedean linear ordered multiplicative commutative group G with order topology either is dense in G or is a cyclic subgroup.

theorem AddSubgroup.dense_or_cyclic {G : Type u_1} [LinearOrderedAddCommGroup G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] (S : AddSubgroup G) : Dense ↑S ∨ ∃ (a : G), S = closure {a}

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 Subgroup.dense_xor'_cyclic {G : Type u_1} [LinearOrderedCommGroup G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] (s : Subgroup G) : Xor' (Dense ↑s) (∃ (a : G), s = zpowers a)

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.

theorem AddSubgroup.dense_xor'_cyclic {G : Type u_1} [LinearOrderedAddCommGroup G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] [Nontrivial G] [DenselyOrdered G] (s : AddSubgroup G) : Xor' (Dense ↑s) (∃ (a : G), s = zmultiples a)

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 Subgroup.dense_iff_ne_zpowers {G : Type u_1} [LinearOrderedCommGroup G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] {s : Subgroup G} : Dense ↑s ↔ ∀ (a : G), s ≠ zpowers a

theorem AddSubgroup.dense_iff_ne_zmultiples {G : Type u_1} [LinearOrderedAddCommGroup G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] [Nontrivial G] [DenselyOrdered G] {s : AddSubgroup G} : Dense ↑s ↔ ∀ (a : G), s ≠ zmultiples a