English
For a linearly ordered group, the set of all integer powers a^k (k ∈ Z) is dense in the group if and only if it is surjective onto the group.
Русский
Для линейно упорядоченной группы множество целочисленных степеней a^k (k ∈ Z) плотно в группе тогда и только тогда, когда они образуют сюръективное отображение на группу.
LaTeX
$$$\text{DenseRange}(a^{\cdot}\!:\mathbb{Z}\to G) \iff \text{Surjective}(a^{\cdot}\!:\mathbb{Z}\to G).$$$
Lean4
/-- In a linearly ordered multiplicative group, the integer powers of an element are dense
iff they are the whole group. -/
@[to_additive /-- In a linearly ordered additive group, the integer multiples of an element are
dense iff they are the whole group. -/
]
theorem denseRange_zpow_iff_surjective {a : G} : DenseRange (a ^ · : ℤ → G) ↔ Surjective (a ^ · : ℤ → G) :=
by
refine ⟨fun h ↦ ?_, fun h ↦ h.denseRange⟩
wlog ha₀ : 1 < a generalizing a
· simp only [← range_eq_univ, DenseRange] at *
rcases (not_lt.1 ha₀).eq_or_lt with rfl | hlt
· simpa only [one_zpow, range_const, dense_iff_closure_eq, closure_singleton] using h
· have H : range (a⁻¹ ^ · : ℤ → G) = range (a ^ · : ℤ → G) := by
simpa only [← inv_zpow, zpow_neg, comp_def] using neg_surjective.range_comp (a ^ · : ℤ → G)
rw [← H]
apply this <;> simpa only [H, one_lt_inv']
intro b
obtain ⟨m, hm, hm'⟩ : ∃ m : ℤ, a ^ m ∈ Ioo b (b * a * a) :=
by
have hne : (Ioo b (b * a * a)).Nonempty := ⟨b * a, by simpa⟩
simpa using h.exists_mem_open isOpen_Ioo hne
rcases eq_or_ne b (a ^ (m - 1)) with rfl | hne; · simp
suffices (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
by
rcases h.exists_mem_open isOpen_Ioo this with ⟨l, hl⟩
have : m < l ∧ l < m + 1 := by simpa [zpow_lt_zpow_iff_right ha₀] using hl
cutsat
rcases hne.lt_or_gt with hlt | hlt
· refine ⟨b * a * a, hm', ?_⟩
simpa only [zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv, lt_div_iff_mul_lt, mul_lt_mul_iff_right] using hlt
· use b * a
simp only [mem_Ioo, zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv, mul_lt_mul_iff_right] at hlt ⊢
exact ⟨div_lt_iff_lt_mul.1 hlt, hm⟩
