Characterisation of the integers

Stream: Is there code for X?

[Oliver Nash]

I believe the following is true. I tried Aristotle but it didn't work for me. However ChatGPT agrees with me.

import Mathlib.GroupTheory.SpecificGroups.Cyclic
import Mathlib.Topology.Algebra.Order.Archimedean

open Filter Set

@[to_additive]
instance (G : Type*) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G]
    [TopologicalSpace G] [OrderTopology G] [DiscreteTopology G] :
    IsCyclic G := by
  nontriviality G
  obtain ⟨g, h₁, h₂⟩ : ∃ g : G, 1 < g ∧ Ioo 1 g = ∅ := by
    -- `{1}` is open
    sorry
  refine ⟨g, fun g' ↦ (?_ : ∃ k : ℤ, g ^ k = g')⟩
  have h₃ (g' : G) (hg' : 1 < g') : ∃ n : ℕ, g ^ n = g' := by
    -- smallest `n` such that `g' ≤ g ^ (n + 1)`
    sorry
  -- trivial cases analysis on `lt_trichotomy g' 1`
  sorry

I can't justify taking the time to close these sorrys but if anyone fancies a fun little project, I'd be very grateful!

[Yaël Dillies]

Don't [LinearOrder G] [TopologicalSpace G] [OrderTopology G] [DiscreteTopology G] together imply Subsingleton G?

[Yaël Dillies]

Oh, I guess not! It is more of a local finiteness condition.

[Ruben Van de Velde]

  -- trivial cases analysis on `lt_trichotomy g' 1`
  obtain h|rfl|h := lt_trichotomy g' 1
  · obtain ⟨n, hn⟩ := h₃ g'⁻¹ <| by simp [h]
    use -n
    simpa [inv_eq_iff_eq_inv]
  · obtain ⟨n, hn⟩ := h₃ g h₁
    use n - 1
    rw [← mul_left_inj g, ← zpow_add_one, one_mul, sub_add_cancel, zpow_natCast, hn]
  · obtain ⟨n, hn⟩ := h₃ _ h
    use n
    simpa

[Yakov Pechersky]

We have that a linear mularchimedean group is either isomorphic to Z (multiplicative), or is densely ordered. So discretetopology makes it be the first case.

[Aaron Liu]

Yaël Dillies said:

Don't [LinearOrder G] [TopologicalSpace G] [OrderTopology G] [DiscreteTopology G] together imply Subsingleton G?

It means your order is a tower of ℤ, so that it can be expressed as G ≃o α ×ₗ ℤ for some α.

[Aaron Liu]

or I guess it could be terminated on the ends by ℕ and ℕᵒᵈ

[Aaron Liu]

or I guess it could be finite

[Aaron Liu]

I think those are the only options

[Aaron Liu]

I guess this could be expressed more concisely as it's a docs#SuccOrder and a docs#PredOrder

[Oliver Nash]

Yakov Pechersky said:

We have that a linear mularchimedean group is either isomorphic to Z (multiplicative), or is densely ordered. So discretetopology makes it be the first case.

Oh that's great! Looking now I guess something like docs#LinearOrderedCommGroup.discrete_iff_not_denselyOrdered will be very useful (though I do wonder if the conclusion of that lemma should use the slightly weaker IsCyclic G rather than Nonempty (G ≃+o ℤ)).

[Oliver Nash]

OK so I guess the route is:

import Mathlib.GroupTheory.ArchimedeanDensely
import Mathlib.GroupTheory.SpecificGroups.Cyclic
import Mathlib.Topology.Algebra.Order.Archimedean

open Filter Set

instance {G : Type*} [LinearOrder G] [TopologicalSpace G]
    [DiscreteTopology G] [OrderTopology G] [DenselyOrdered G] :
    Subsingleton G := by
  refine ⟨fun a b ↦ ?_⟩
  wlog h : a < b
  · rcases eq_or_ne b a with rfl | h'
    · rfl
    · exact (this b a (lt_of_le_of_ne (by simpa using h) h')).symm
  sorry

-- @[to_additive]
instance (G : Type*) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G]
    [TopologicalSpace G] [OrderTopology G] [DiscreteTopology G] :
    IsCyclic G := by
  nontriviality G
  have : ¬ DenselyOrdered G := fun contra ↦ false_of_nontrivial_of_subsingleton G
  obtain ⟨e⟩ := (LinearOrderedCommGroup.discrete_iff_not_denselyOrdered G).mpr this
  exact e.isCyclic.mpr inferInstance

[Yakov Pechersky]

Yup! Having the iso (even from a nonempty) gives access to more operations. Unless we have a IsCyclic G \iff Nonempty MulEquiv also?

[Oliver Nash]

I don't have time to think about this in detail but what I thought regarding the Nonempty (G ≃+o ℤ) point was that this certainly is useful but that I'd make a def which provides this from [Infinite G] [IsCyclic G] and then just use IsCyclic in the lemma I mentioned.

[Oliver Nash]

Oh Aristotle proved this last bit! I like this workflow (ask ChatGPT, kick off Aristotle, review some other PRs, and come back to a working proof).

import Mathlib.GroupTheory.ArchimedeanDensely
import Mathlib.GroupTheory.SpecificGroups.Cyclic
import Mathlib.Topology.Algebra.Order.Archimedean
import Mathlib.Topology.Order.DenselyOrdered

open Set

-- Courtesy of Aristotle!
instance foo {G : Type*} [LinearOrder G] [TopologicalSpace G]
    [DiscreteTopology G] [OrderTopology G] [DenselyOrdered G] :
    Subsingleton G := by
  refine ⟨fun a b ↦ ?_⟩
  wlog h : a < b
  · rcases eq_or_ne b a with rfl | h'
    · rfl
    · exact (this b a (lt_of_le_of_ne (by simpa using h) h')).symm
  -- By contradiction, assume $a < b$.
  by_contra h_lt
  obtain ⟨c, hc⟩ : ∃ c : G, a < c ∧ c < b := by
    exact exists_between h
  -- Since $G$ is discrete, the interval $(a, b)$ is closed.
  have h_closed : IsClosed (Set.Ioo a b) := by
    exact isClosed_discrete (Ioo a b)
  -- Since $G$ is discrete, the interval $(a, b)$ is both open and closed, hence it must be equal
  -- to its closure.
  have h_eq_closure : Set.Ioo a b = closure (Set.Ioo a b) := by
    rw [ h_closed.closure_eq ];
  -- Since $G$ is discrete, the interval $(a, b)$ is equal to its closure, which is $\{a, b\}$.
  have h_closure : closure (Set.Ioo a b) = Set.Icc a b := by
    exact closure_Ioo h_lt
  -- Since $a < b$, the interval $(a, b)$ cannot be equal to $[a, b]$ because $a$ and $b$ are not
  -- in $(a, b)$.
  have h_contradiction : a ∉ Set.Ioo a b ∧ b ∉ Set.Ioo a b := by
    simp +decide [ h ];
  exact h_contradiction.1 ( h_eq_closure.symm ▸ h_closure.symm ▸ Set.left_mem_Icc.mpr h.le )

-- @[to_additive]
instance bar (G : Type*) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G]
    [TopologicalSpace G] [OrderTopology G] [DiscreteTopology G] :
    IsCyclic G := by
  nontriviality G
  have : ¬ DenselyOrdered G := fun contra ↦ false_of_nontrivial_of_subsingleton G
  obtain ⟨e⟩ := (LinearOrderedCommGroup.discrete_iff_not_denselyOrdered G).mpr this
  exact e.isCyclic.mpr inferInstance

#print axioms foo
#print axioms bar

[Yakov Pechersky]

Agreed with you on the IsCyclic, there would have to be several defs (mulEquiv, orderMulIso) depending on the assumptions on G. The other reason I did it using the Nonempty style -- I really wanted the similar statement about mularchimedean linearly ordered groups with zero, where [IsCyclic G0\^x] is clunkier.