feat(GroupTheory/ArchimedeanDensely): locally finite linearly ordered groups are mul archimedean

[pechersky]

for CFT workshop

---

[github-actions]

PR summary 5eb29c4828

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ MulArchimedean.of_locallyFiniteOrder

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[YaelDillies]

Can you prove this by first establishing that they are all isomorphic to ℤ? Proof: Pick the unique element one that covers 0 and the unique element negOne that's covered by 0. one + negOne = negOne + one = 0, one, negOne generate G and have infinite torsion, all by order theory.

[erdOne]

I'm trying to do what Yael said.

[pechersky]

I think that will require an in-line MulArchimedean instance anyway, to show that your "1" generates.

[erdOne]

You do something like this

import Mathlib

open Finset

variable {M G : Type*} [AddCancelCommMonoid M] [LinearOrder M] [IsOrderedAddMonoid M] 
    [LocallyFiniteOrder M] [AddCommGroup G] [LinearOrder G]
    [IsOrderedAddMonoid G] [LocallyFiniteOrder G]

lemma Finset.card_Ico_add_right [ExistsAddOfLE M] (a b c : M) :
    #(Ico (a + c) (b + c)) = #(Ico a b) := by
  have : (Ico (a + c) (b + c)) = (Ico a b).map (addRightEmbedding c) := by
    ext x
    simp only [mem_Ico, mem_map, addRightEmbedding_apply]
    constructor
    · rintro ⟨h₁, h₂⟩
      obtain ⟨d, rfl⟩ := exists_add_of_le h₁
      exact ⟨a + d, ⟨by simpa using h₁, by simpa [add_right_comm a c d] using h₂⟩,
        by simp_rw [add_assoc, add_comm]⟩
    · aesop
  simp [this]

lemma card_Ico_zero_add [ExistsAddOfLE M] (a b : M)
    (ha : 0 ≤ a) (hb : 0 ≤ b) :
    #(Ico 0 (a + b)) = #(Ico 0 a) + #(Ico 0 b) := by
  have : Ico 0 b ∪ Ico (0 + b) (a + b) = Ico 0 (a + b) := by
    simp [Ico_union_Ico, ha, hb, Left.add_nonneg ha hb]
  rw [← this, Finset.card_union, Finset.card_Ico_add_right]
  simp [add_comm]

variable (G) in
def LocallyFiniteOrder.addMonoidHom :
    G →+ ℤ where
  toFun a := #(Ico 0 a) - #(Ico 0 (-a))
  map_zero' := by simp
  map_add' a b := by
    wlog hab : a ≤ b generalizing a b
    · convert this b a (le_of_not_ge hab) using 1 <;> simp only [add_comm]
    obtain ha | ha := le_total 0 a <;> obtain hb | hb := le_total 0 b
    · have : -b ≤ a := by trans 0 <;> simp [ha, hb]
      simp [ha, hb, card_Ico_zero_add, this]
    · obtain rfl := hb.antisymm (ha.trans hab)
      obtain rfl := ha.antisymm hab
      simp
    · simp only [neg_add_rev, ha, Ico_eq_empty_of_le, card_empty, CharP.cast_eq_zero,
        zero_sub, Left.neg_nonpos_iff, hb, sub_zero]
      obtain ⟨b, rfl⟩ : ∃ r, b = r - a := ⟨a + b, by abel⟩
      simp only [add_sub_cancel, neg_sub, sub_add_eq_add_sub, add_neg_cancel, zero_sub]
      obtain hb' | hb' := le_total 0 b
      · simp [hb', neg_add_eq_sub, eq_sub_iff_add_eq, ← Nat.cast_add,
          ← card_Ico_zero_add, ha, ← sub_eq_add_neg]
      · simp [hb', neg_add_eq_sub, eq_sub_iff_add_eq, sub_eq_iff_eq_add,
          ← Nat.cast_add, ← card_Ico_zero_add, hb, sub_add_eq_add_sub]
    · have : ¬0 < a + b := by simpa using add_nonpos ha hb
      simp [ha, hb, card_Ico_zero_add, Ico_eq_empty, this]
  
variable (G) in
def LocallyFiniteOrder.orderAddMonoidHom :
    G →+o ℤ where
  __ := addMonoidHom G
  monotone' a b hab := by
    obtain ⟨b, rfl⟩ := add_left_surjective a b
    replace hab : 0 ≤ b := by simpa using hab
    suffices 0 ≤ addMonoidHom G b by simpa
    simp [addMonoidHom, hab]

lemma LocallyFiniteOrder.orderAddMonoidHom_injective :
    Function.Injective (orderAddMonoidHom G) := by
  rw [injective_iff_map_eq_zero]
  intro g H
  obtain hg | hg := le_total 0 g
  · exact hg.antisymm' (by simpa [orderAddMonoidHom, addMonoidHom, hg] using H)
  · exact hg.antisymm (by simpa [orderAddMonoidHom, addMonoidHom, hg] using H)

lemma LocallyFiniteOrder.orderAddMonoidHom_bijective [Nontrivial G] :
    Function.Bijective (orderAddMonoidHom G) := by
  refine ⟨orderAddMonoidHom_injective, ?_⟩
  suffices 1 ∈ (orderAddMonoidHom G).range by
    obtain ⟨x, hx⟩ := this
    exact fun a ↦ ⟨a • x, by simp_all⟩
  have ⟨a, ha⟩ := exists_zero_lt (α := G)
  obtain ⟨b, hb⟩ := exists_covBy_of_wellFoundedLT (α := Icc 0 a) (a := ⟨0, by simpa using ha.le⟩) 
    (fun H ↦ ha.not_ge (@H ⟨a, by simpa using ha.le⟩ ha.le))
  use b.1
  have : 0 ≤ b.1 := hb.1.le
  suffices Ico 0 b.1 = {0} by simpa [orderAddMonoidHom, addMonoidHom, this]
  ext x
  simp only [mem_Ico, mem_singleton]
  constructor
  · rintro ⟨h₁, h₂⟩
    by_contra hx'
    have := b.2
    simp only [Finset.mem_Icc] at this
    exact hb.2 (c := ⟨x, by simpa [h₁] using h₂.le.trans this.2⟩)
      (lt_of_le_of_ne h₁ (by simpa using Ne.symm hx')) h₂
  · rintro rfl
    simpa using hb.1