Extension_Theorem_for_Total_Orderings

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Extension_Theorem_for_Total_Orderings is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Let the following conditions be fulfilled $(1):\quad$ Let $\struct {S, \circ, \preceq}$ be a totally ordered commutative semigroup $(2):\quad$ Let all the elements of $\struct {S, \circ, \preceq}$ be cancellable $(3):\quad$ Let $\struct {T, \circ}$ be an inverse completion of $\struct {S, \circ}$. Then $(1):\quad$ The relation $\preceq'$ on $T$ satisfying $\forall x_1, x_2, y_1, y_2 \in S: x_1 \circ \paren {y_1}^{-1} \preceq' x_2 \circ \paren {y_2}^{-1} \iff x_1 \circ y_2 \preceq x_2 \circ y_1$ is a well-defined relation $(2):\quad$ $\preceq'$ is the only total ordering on $T$ compatible with $\circ$ $(3):\quad$ $\preceq'$ is the only total ordering on $T$ that induces the given ordering $\preceq$ on $S$.

Why this node was retired

The posted statement is

theorem Extension_Theorem_for_Total_Orderings {S : Type _} [CommMonoid S] [LinearOrder S] [CovariantClass S S (· * ·) (· ≤ ·)] {G : Type _} [CommGroup G] (f : S →* G) (hf : Function.Injective f) : ∃ le' : LinearOrder G, True := by sorry

The goal is ∃ le' : LinearOrder G, True, which asserts only that G admits some linear order — true of any type by choice. Neither compatibility with the group operation nor the requirement that the order extend the given order on S along f appears.

What a faithful statement would require

The order on G must be required to be translation-invariant and to restrict along f to the given order on S.

No corrected replacement node exists yet.