closure_equiv_closure — Mathlib

English

In two linearly ordered groups, the closure of an element in one group is order-isomorphic to the closure of an element in the other group, provided a compatibility condition on the element (x = 1 ⇔ y = 1).

Русский

В двух упорядоченных группах замыкание элемента одной группы изоморфно по порядку замыканию элемента другой группы при совместимости x = 1 ⇔ y = 1.

LaTeX

$$$ closure(\{x\}) \cong_o closure(\{y\}) \text{ for } x = 1 \leftrightarrow y = 1. $$$

Lean4

/-- In two linearly ordered groups, the closure of an element of one group
is isomorphic (and order-isomorphic) to the closure of an element in the other group. -/
@[to_additive /-- In two linearly ordered additive groups, the closure of an element of one group
    is isomorphic (and order-isomorphic) to the closure of an element in the other group. -/
    ]
noncomputable def closure_equiv_closure {G G' : Type*} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [CommGroup G']
    [LinearOrder G'] [IsOrderedMonoid G'] (x : G) (y : G') (hxy : x = 1 ↔ y = 1) :
    closure ({ x } : Set G) ≃*o closure ({ y } : Set G') :=
  if hx : x = 1 then
    by
    refine ⟨⟨⟨fun _ ↦ ⟨1, by simp [hxy.mp hx]⟩, fun _ ↦ ⟨1, by simp [hx]⟩, ?_, ?_⟩, ?_⟩, ?_⟩
    · intro ⟨a, ha⟩
      simpa [hx, closure_singleton_one, eq_comm] using ha
    · intro ⟨a, ha⟩
      simpa [hxy.mp hx, closure_singleton_one, eq_comm] using ha
    · intros
      simp
    · intro ⟨a, ha⟩ ⟨b, hb⟩
      simp only [hx, closure_singleton_one, mem_bot] at ha hb
      simp [ha, hb]
  else by
    set x' := max x x⁻¹ with hx'
    have xpos : 1 < x' := by simp [hx', eq_comm, hx]
    set y' := max y y⁻¹ with hy'
    have ypos : 1 < y' := by simp [hy', eq_comm, ← hxy, hx]
    have hxc : closure { x } = closure { x' } := by rcases max_cases x x⁻¹ with H | H <;> simp [hx', H.left]
    have hyc : closure { y } = closure { y' } := by rcases max_cases y y⁻¹ with H | H <;> simp [hy', H.left]
    refine
      ⟨⟨⟨fun a ↦ ⟨y' ^ ((mem_closure_singleton).mp (by simpa [hxc] using a.prop)).choose, ?_⟩, fun a ↦
            ⟨x' ^ ((mem_closure_singleton).mp (by simpa [hyc] using a.prop)).choose, ?_⟩, ?_, ?_⟩,
          ?_⟩,
        ?_⟩
    · rw [hyc, mem_closure_singleton]
      exact ⟨_, rfl⟩
    · rw [hxc, mem_closure_singleton]
      exact ⟨_, rfl⟩
    · intro a
      generalize_proofs A B C D
      rw [Subtype.ext_iff, ← (C a).choose_spec, zpow_right_inj xpos, ← zpow_right_inj ypos, (A ⟨_, D a⟩).choose_spec]
    · intro a
      generalize_proofs A B C D
      rw [Subtype.ext_iff, ← (C a).choose_spec, zpow_right_inj ypos, ← zpow_right_inj xpos, (A ⟨_, D a⟩).choose_spec]
    · intro a b
      generalize_proofs A B C D E F
      simp only [coe_mul, MulMemClass.mk_mul_mk, Subtype.ext_iff]
      rw [← zpow_add, zpow_right_inj ypos, ← zpow_right_inj xpos, zpow_add, (A a).choose_spec, (A b).choose_spec,
        (A (a * b)).choose_spec]
      simp
    · intro a b
      simp only [Subtype.mk_le_mk]
      generalize_proofs A B C D
      simp [zpow_le_zpow_iff_right ypos, ← zpow_le_zpow_iff_right xpos, A.choose_spec, B.choose_spec]

Похожие утверждения