The quotient of an ordered group by a convex subgroup

A subgroup of a linearly ordered abelian group that is order-connected as a set is convex, and the quotient by it inherits a linear order: one coset lies below another when some representative of the first lies below some representative of the second. Convexity is exactly what makes that relation antisymmetric, because an element trapped between zero and a subgroup element belongs to the subgroup.

The projection is monotone and reflects the strict order (mk_le_mk, lt_of_mk_lt_mk). Those two facts are what let order-theoretic hypotheses be transported to the quotient — filling cuts, in the intended application, where the quotient is taken to gain a small coinitial family of positive elements that the group itself lacks.

class ConwayRefinement.Standalone.Hahn.ConvexQuotient.IsConvex {G : Type u} [AddCommGroup G] [LinearOrder G] (H : AddSubgroup G) : Prop

A subgroup of an ordered group is convex when it is order-connected.

• ordConnected : (↑H).OrdConnected

  The carrier of a convex subgroup is order-connected.

theorem ConwayRefinement.Standalone.Hahn.ConvexQuotient.mem_of_nonneg_of_le {G : Type u} [AddCommGroup G] [LinearOrder G] (H : AddSubgroup G) [IsConvex H] {x y : G} (hx : 0 ≤ x) (hxy : x ≤ y) (hy : y ∈ H) : x ∈ H

A nonnegative element below an element of a convex subgroup lies in the subgroup.

@[instance_reducible]

instance ConwayRefinement.Standalone.Hahn.ConvexQuotient.instLE {G : Type u} [AddCommGroup G] [LinearOrder G] {H : AddSubgroup G} : LE (G ⧸ H)

One coset lies below another when some representative of the first lies below some representative of the second.

Equations

• ConwayRefinement.Standalone.Hahn.ConvexQuotient.instLE = { le := fun (x y : G ⧸ H) => ∃ (a : G) (b : G), ↑a = x ∧ ↑b = y ∧ a ≤ b }

theorem ConwayRefinement.Standalone.Hahn.ConvexQuotient.mk_le_mk_iff {G : Type u} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : AddSubgroup G} [IsConvex H] {a b : G} : ↑a ≤ ↑b ↔ a ≤ b ∨ b - a ∈ H

Comparing cosets. One coset lies below another exactly when the chosen representatives are already comparable or differ by a subgroup element. Convexity supplies the forward direction: were the representatives reversed, their difference would be trapped between zero and the subgroup element relating the two choices.

theorem ConwayRefinement.Standalone.Hahn.ConvexQuotient.mk_le_mk {G : Type u} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : AddSubgroup G} [IsConvex H] {a b : G} (h : a ≤ b) : ↑a ≤ ↑b

The projection is monotone.

@[instance_reducible]

noncomputable instance ConwayRefinement.Standalone.Hahn.ConvexQuotient.instLinearOrder {G : Type u} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : AddSubgroup G} [IsConvex H] : LinearOrder (G ⧸ H)

Equations

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

instance ConwayRefinement.Standalone.Hahn.ConvexQuotient.instIsOrderedAddMonoid {G : Type u} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : AddSubgroup G} [IsConvex H] : IsOrderedAddMonoid (G ⧸ H)

theorem ConwayRefinement.Standalone.Hahn.ConvexQuotient.lt_of_mk_lt_mk {G : Type u} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : AddSubgroup G} [IsConvex H] {a b : G} (h : ↑a < ↑b) : a < b

The projection reflects the strict order. Two representatives whose cosets are strictly comparable are themselves strictly comparable.

theorem ConwayRefinement.Standalone.Hahn.ConvexQuotient.mk_lt_mk_iff {G : Type u} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : AddSubgroup G} [IsConvex H] {a b : G} : ↑a < ↑b ↔ a < b ∧ b - a ∉ H

One coset lies strictly below another exactly when the representatives do and their difference escapes the subgroup.

theorem ConwayRefinement.Standalone.Hahn.ConvexQuotient.exists_half_of_pos {G : Type u} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : AddSubgroup G} [IsConvex H] (hG : ∀ (x : G), 0 < x → ∃ (y : G), 0 < y ∧ y + y = x) {c : G ⧸ H} (hc : 0 < c) : ∃ (d : G ⧸ H), 0 < d ∧ d + d ≤ c

Halving descends to the quotient. If every positive element of G is twice a positive element, the same holds in the quotient: a representative's half stays outside the subgroup, since otherwise the representative itself would lie inside it.