Documentation

Mathlib.GroupTheory.ArchimedeanDensely

Archimedean groups are either discrete or densely ordered #

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 : (AddSubgroup.closure {x})) (b : (AddSubgroup.closure {x})) :
{ toFun := fun (a : (AddSubgroup.closure {x})) => .choose max y (-y), , invFun := fun (a : (AddSubgroup.closure {y})) => .choose max x (-x), , left_inv := , right_inv := }.toFun (a + b) = { toFun := fun (a : (AddSubgroup.closure {x})) => .choose max y (-y), , invFun := fun (a : (AddSubgroup.closure {y})) => .choose max x (-x), , left_inv := , right_inv := }.toFun a + { toFun := fun (a : (AddSubgroup.closure {x})) => .choose max y (-y), , invFun := fun (a : (AddSubgroup.closure {y})) => .choose max x (-x), , left_inv := , right_inv := }.toFun b
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 : (AddSubgroup.closure {x})), (fun (x_1 : (AddSubgroup.closure {y})) => 0, ) ((fun (x_1 : (AddSubgroup.closure {x})) => 0, ) h) = h
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_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) :
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 : (AddSubgroup.closure {x})} {b : (AddSubgroup.closure {x})} :
{ toFun := fun (a : (AddSubgroup.closure {x})) => .choose max y (-y), , invFun := fun (a : (AddSubgroup.closure {y})) => .choose max x (-x), , left_inv := , right_inv := , map_add' := }.toFun a { toFun := fun (a : (AddSubgroup.closure {x})) => .choose max y (-y), , invFun := fun (a : (AddSubgroup.closure {y})) => .choose max x (-x), , left_inv := , right_inv := , map_add' := }.toFun b a b
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 : (AddSubgroup.closure {x})) :
(fun (a : (AddSubgroup.closure {y})) => .choose max x (-x), ) ((fun (a : (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) :

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.
Instances For
    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 : (AddSubgroup.closure {y})) :
    (fun (a : (AddSubgroup.closure {x})) => .choose max y (-y), ) ((fun (a : (AddSubgroup.closure {y})) => .choose max x (-x), ) a) = a
    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_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) :
    (AddSubgroup.closure {x})(AddSubgroup.closure {x})0, = 0 + 0,
    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 : (AddSubgroup.closure {x})} {b : (AddSubgroup.closure {x})}, { toFun := fun (x_1 : (AddSubgroup.closure {x})) => 0, , invFun := fun (x_1 : (AddSubgroup.closure {y})) => 0, , left_inv := , right_inv := , map_add' := }.toFun h { toFun := fun (x_1 : (AddSubgroup.closure {x})) => 0, , invFun := fun (x_1 : (AddSubgroup.closure {y})) => 0, , left_inv := , right_inv := , map_add' := }.toFun b h b
    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 : (AddSubgroup.closure {y})), (fun (x_1 : (AddSubgroup.closure {x})) => 0, ) ((fun (x_1 : (AddSubgroup.closure {y})) => 0, ) h) = h
    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) :

    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.
    Instances For
      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

      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.
      Instances For

        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.
        Instances For

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

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

          Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is either isomorphic (and order-isomorphic) to ℤₘ₀, or is densely ordered.