Archimedean groups are either discrete or densely ordere

This file proves a few additional facts about linearly ordered additive groups which satisfy the Archimedean property -- they are either order-isomorphic and additvely isomorphic to the integers, or they are densely ordered.

They are placed here in a separate file (rather than incorporated as a continuation of GroupTheory.Archimedean) because they rely on some imports from pointwise lemmas.

theorem AddSubgroup.mem_closure_singleton_iff_existsUnique_zsmul {G : Type u_1} [LinearOrderedAddCommGroup G] {a : G} {b : G} (ha : a ≠ 0) : b ∈ AddSubgroup.closure {a} ↔ ∃! k : ℤ, k • a = b

The additive subgroup generated by an element of an additive group equals the set of integer multiples of the element, such that each multiple is a unique element. This is the stronger version of AddSubgroup.mem_closure_singleton.

theorem Subgroup.mem_closure_singleton_iff_existsUnique_zpow {G : Type u_1} [LinearOrderedCommGroup G] {a : G} {b : G} (ha : a ≠ 1) : b ∈ Subgroup.closure {a} ↔ ∃! k : ℤ, a ^ k = b

The subgroup generated by an element of a group equals the set of integer powers of the element, such that each power is a unique element. This is the stronger version of Subgroup.mem_closure_singleton.

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_17 {G : Type u_1} {G' : Type u_2} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (xpos : 0 < max x (-x)) (ypos : 0 < max y (-y)) (hxc : AddSubgroup.closure {x} = AddSubgroup.closure {max x (-x)}) (hyc : AddSubgroup.closure {y} = AddSubgroup.closure {max y (-y)}) (a : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) (b : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) : { toFun := fun (a : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) => ⟨⋯.choose • max y (-y), ⋯⟩, invFun := fun (a : { x : G' // x ∈ AddSubgroup.closure {y} }) => ⟨⋯.choose • max x (-x), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun (a + b) = { toFun := fun (a : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) => ⟨⋯.choose • max y (-y), ⋯⟩, invFun := fun (a : { x : G' // x ∈ AddSubgroup.closure {y} }) => ⟨⋯.choose • max x (-x), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun a + { toFun := fun (a : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) => ⟨⋯.choose • max y (-y), ⋯⟩, invFun := fun (a : { x : G' // x ∈ AddSubgroup.closure {y} }) => ⟨⋯.choose • max x (-x), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun b

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_7 {G : Type u_1} [LinearOrderedAddCommGroup G] (x : G) (hx : ¬x = 0) (hx' : max x (-x) = max x (-x)) : 0 < max x (-x)

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_3 {G : Type u_1} {G' : Type u_2} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (hxy : x = 0 ↔ y = 0) (hx : x = 0) : ∀ (h : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }), (fun (x_1 : { x : G' // x ∈ AddSubgroup.closure {y} }) => ⟨0, ⋯⟩) ((fun (x_1 : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) => ⟨0, ⋯⟩) h) = h

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_1 {G : Type u_2} {G' : Type u_1} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (hxy : x = 0 ↔ y = 0) (hx : x = 0) : 0 ∈ AddSubgroup.closure {y}

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_18 {G : Type u_1} {G' : Type u_2} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (xpos : 0 < max x (-x)) (ypos : 0 < max y (-y)) (hxc : AddSubgroup.closure {x} = AddSubgroup.closure {max x (-x)}) (hyc : AddSubgroup.closure {y} = AddSubgroup.closure {max y (-y)}) {a : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }} {b : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }} : { toFun := fun (a : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) => ⟨⋯.choose • max y (-y), ⋯⟩, invFun := fun (a : { x : G' // x ∈ AddSubgroup.closure {y} }) => ⟨⋯.choose • max x (-x), ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }.toFun a ≤ { toFun := fun (a : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) => ⟨⋯.choose • max y (-y), ⋯⟩, invFun := fun (a : { x : G' // x ∈ AddSubgroup.closure {y} }) => ⟨⋯.choose • max x (-x), ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }.toFun b ↔ a ≤ b

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_12 {G : Type u_2} {G' : Type u_1} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (hxc : AddSubgroup.closure {x} = AddSubgroup.closure {max x (-x)}) (hyc : AddSubgroup.closure {y} = AddSubgroup.closure {max y (-y)}) (a : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) : ⋯.choose • max y (-y) ∈ AddSubgroup.closure {y}

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_14 {G : Type u_1} {G' : Type u_2} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (hxc : AddSubgroup.closure {x} = AddSubgroup.closure {max x (-x)}) (hyc : AddSubgroup.closure {y} = AddSubgroup.closure {max y (-y)}) (a : { x : G' // x ∈ AddSubgroup.closure {y} }) : ⋯.choose • max x (-x) ∈ AddSubgroup.closure {x}

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_15 {G : Type u_1} {G' : Type u_2} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (xpos : 0 < max x (-x)) (ypos : 0 < max y (-y)) (hxc : AddSubgroup.closure {x} = AddSubgroup.closure {max x (-x)}) (hyc : AddSubgroup.closure {y} = AddSubgroup.closure {max y (-y)}) (a : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) : (fun (a : { x : G' // x ∈ AddSubgroup.closure {y} }) => ⟨⋯.choose • max x (-x), ⋯⟩) ((fun (a : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) => ⟨⋯.choose • max y (-y), ⋯⟩) a) = a

noncomputable def LinearOrderedAddCommGroup.closure_equiv_closure {G : Type u_1} {G' : Type u_2} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (hxy : x = 0 ↔ y = 0) : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} } ≃+o { x : G' // x ∈ AddSubgroup.closure {y} }

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.

Equations

• One or more equations did not get rendered due to their size.

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_8 {G : Type u_2} {G' : Type u_1} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (hxy : x = 0 ↔ y = 0) (hx : ¬x = 0) (hy' : max y (-y) = max y (-y)) : 0 < max y (-y)

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_11 {G : Type u_1} [LinearOrderedAddCommGroup G] (x : G) (hxc : AddSubgroup.closure {x} = AddSubgroup.closure {max x (-x)}) (a : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) : ∃ (n : ℤ), n • max x (-x) = ↑a

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_16 {G : Type u_2} {G' : Type u_1} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (xpos : 0 < max x (-x)) (ypos : 0 < max y (-y)) (hxc : AddSubgroup.closure {x} = AddSubgroup.closure {max x (-x)}) (hyc : AddSubgroup.closure {y} = AddSubgroup.closure {max y (-y)}) (a : { x : G' // x ∈ AddSubgroup.closure {y} }) : (fun (a : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) => ⟨⋯.choose • max y (-y), ⋯⟩) ((fun (a : { x : G' // x ∈ AddSubgroup.closure {y} }) => ⟨⋯.choose • max x (-x), ⋯⟩) a) = a

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_13 {G' : Type u_1} [LinearOrderedAddCommGroup G'] (y : G') (hyc : AddSubgroup.closure {y} = AddSubgroup.closure {max y (-y)}) (a : { x : G' // x ∈ AddSubgroup.closure {y} }) : ∃ (n : ℤ), n • max y (-y) = ↑a

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_6 {G : Type u_1} {G' : Type u_2} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (hxy : x = 0 ↔ y = 0) (hx : x = 0) : ∀ {h : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }} {b : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }}, { toFun := fun (x_1 : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) => ⟨0, ⋯⟩, invFun := fun (x_1 : { x : G' // x ∈ AddSubgroup.closure {y} }) => ⟨0, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }.toFun h ≤ { toFun := fun (x_1 : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) => ⟨0, ⋯⟩, invFun := fun (x_1 : { x : G' // x ∈ AddSubgroup.closure {y} }) => ⟨0, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }.toFun b ↔ h ≤ b

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_2 {G : Type u_1} [LinearOrderedAddCommGroup G] (x : G) (hx : x = 0) : 0 ∈ AddSubgroup.closure {x}

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_5 {G : Type u_1} {G' : Type u_2} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (hxy : x = 0 ↔ y = 0) (hx : x = 0) : { x_2 : G // x_2 ∈ AddSubgroup.closure {x} } → { x_2 : G // x_2 ∈ AddSubgroup.closure {x} } → ⟨0, ⋯⟩ = ⟨0 + 0, ⋯⟩

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_10 {G' : Type u_1} [LinearOrderedAddCommGroup G'] (y : G') (hy' : max y (-y) = max y (-y)) : AddSubgroup.closure {y} = AddSubgroup.closure {max y (-y)}

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_4 {G : Type u_2} {G' : Type u_1} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (hxy : x = 0 ↔ y = 0) (hx : x = 0) : ∀ (h : { x : G' // x ∈ AddSubgroup.closure {y} }), (fun (x_1 : { x_1 : G // x_1 ∈ AddSubgroup.closure {x} }) => ⟨0, ⋯⟩) ((fun (x_1 : { x : G' // x ∈ AddSubgroup.closure {y} }) => ⟨0, ⋯⟩) h) = h

theorem LinearOrderedAddCommGroup.closure_equiv_closure.proof_9 {G : Type u_1} [LinearOrderedAddCommGroup G] (x : G) (hx' : max x (-x) = max x (-x)) : AddSubgroup.closure {x} = AddSubgroup.closure {max x (-x)}

noncomputable def LinearOrderedCommGroup.closure_equiv_closure {G : Type u_1} {G' : Type u_2} [LinearOrderedCommGroup G] [LinearOrderedCommGroup G'] (x : G) (y : G') (hxy : x = 1 ↔ y = 1) : { x_1 : G // x_1 ∈ Subgroup.closure {x} } ≃*o { x : G' // x ∈ Subgroup.closure {y} }

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.

Equations

• One or more equations did not get rendered due to their size.

theorem AddSubgroup.isLeast_of_closure_iff_eq_abs {G : Type u_1} [LinearOrderedAddCommGroup G] [Archimedean G] {a : G} {b : G} : IsLeast {y : G | y ∈ AddSubgroup.closure {a} ∧ 0 < y} b ↔ b = |a| ∧ 0 < b

theorem Subgroup.isLeast_of_closure_iff_eq_mabs {G : Type u_1} [LinearOrderedCommGroup G] [MulArchimedean G] {a : G} {b : G} : IsLeast {y : G | y ∈ Subgroup.closure {a} ∧ 1 < y} b ↔ b = mabs a ∧ 1 < b

noncomputable def LinearOrderedAddCommGroup.int_orderAddMonoidIso_of_isLeast_pos {G : Type u_2} [LinearOrderedAddCommGroup G] [Archimedean G] {x : G} (h : IsLeast {y : G | 0 < y} x) : G ≃+o ℤ

If an element of a linearly ordered archimedean additive group is the least positive element, then the whole group is isomorphic (and order-isomorphic) to the integers.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LinearOrderedCommGroup.multiplicative_int_orderMonoidIso_of_isLeast_one_lt {G : Type u_1} [LinearOrderedCommGroup G] [MulArchimedean G] {x : G} (h : IsLeast {y : G | 1 < y} x) : G ≃*o Multiplicative ℤ

If an element of a linearly ordered mul-archimedean group is the least element greater than 1, then the whole group is isomorphic (and order-isomorphic) to the multiplicative integers.

Equations

• One or more equations did not get rendered due to their size.

theorem LinearOrderedAddCommGroup.discrete_or_denselyOrdered (G : Type u_2) [LinearOrderedAddCommGroup G] [Archimedean G] : Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Any linearly ordered archimedean additive group is either isomorphic (and order-isomorphic) to the integers, or is densely ordered.

theorem LinearOrderedCommGroup.discrete_or_denselyOrdered (G : Type u_1) [LinearOrderedCommGroup G] [MulArchimedean G] : Nonempty (G ≃*o Multiplicative ℤ) ∨ DenselyOrdered G

Any linearly ordered mul-archimedean group is either isomorphic (and order-isomorphic) to the multiplicative integers, or is densely ordered.