Construct ordered groups from groups with a specified positive cone.

We demonstrate the equivalence between order structures on a group G and positive cones: submonoids M of G such that M ∩ -M = 0.

theorem Submonoid.IsMulPointed.oneLE (G : Type u_1) [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] : (oneLE G).IsMulPointed

theorem AddSubmonoid.IsPointed.nonneg (G : Type u_1) [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] : (nonneg G).IsPointed

theorem Submonoid.IsMulSpanning.oneLE (G : Type u_1) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] : (oneLE G).IsMulSpanning

theorem AddSubmonoid.IsSpanning.nonneg (G : Type u_1) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] : (nonneg G).IsSpanning

@[implicit_reducible]

def PartialOrder.ofSubmonoid {G : Type u_1} [CommGroup G] {M : Submonoid G} (hM : M.IsMulPointed) : PartialOrder G

Construct a partial order by designating a submonoid with zero support in an abelian group.

Equations

• PartialOrder.ofSubmonoid hM = { le := fun (a b : G) => b / a ∈ M, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[implicit_reducible]

def PartialOrder.ofAddSubmonoid {G : Type u_1} [AddCommGroup G] {M : AddSubmonoid G} (hM : M.IsPointed) : PartialOrder G

Construct a partial order by designating a submonoid with zero support in an abelian group.

Equations

• PartialOrder.ofAddSubmonoid hM = { le := fun (a b : G) => b - a ∈ M, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[simp]

theorem PartialOrder.ofSubmonoid_le_iff {G : Type u_1} [CommGroup G] {M : Submonoid G} {hM : M.IsMulPointed} {a b : G} : a ≤ b ↔ b / a ∈ M

@[simp]

theorem PartialOrder.ofAddSubmonoid_le_iff {G : Type u_1} [AddCommGroup G] {M : AddSubmonoid G} {hM : M.IsPointed} {a b : G} : a ≤ b ↔ b - a ∈ M

theorem IsOrderedMonoid.ofSubmonoid {G : Type u_1} [CommGroup G] {M : Submonoid G} (hM : M.IsMulPointed) : IsOrderedMonoid G

theorem IsOrderedAddMonoid.ofAddSubmonoid {G : Type u_1} [AddCommGroup G] {M : AddSubmonoid G} (hM : M.IsPointed) : IsOrderedAddMonoid G

@[implicit_reducible]

def LinearOrder.ofSubmonoid {G : Type u_1} [CommGroup G] {M : Submonoid G} (hM : M.IsMulPointed) (hMs : M.IsMulSpanning) [dec : DecidablePred fun (x : G) => x ∈ M] : LinearOrder G

Construct a linear order by designating a maximal submonoid with zero support in an abelian group.

Equations

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

@[implicit_reducible]

def LinearOrder.ofAddSubmonoid {G : Type u_1} [AddCommGroup G] {M : AddSubmonoid G} (hM : M.IsPointed) (hMs : M.IsSpanning) [dec : DecidablePred fun (x : G) => x ∈ M] : LinearOrder G

Construct a linear order by designating a maximal submonoid with zero support in an abelian group.

Equations

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

@[deprecated AddSubmonoid.IsPointed (since := "2026-10-28")]

class AddGroupConeClass (S : Type u_2) (G : outParam (Type u_3)) [AddCommGroup G] [SetLike S G] extends AddSubmonoidClass S G : Prop

AddGroupConeClass S G says that S is a type of cones in G.

• add_mem {s : S} {a b : G} : a ∈ s → b ∈ s → a + b ∈ s
• zero_mem (s : S) : 0 ∈ s
• eq_zero_of_mem_of_neg_mem {C : S} {a : G} : a ∈ C → -a ∈ C → a = 0

@[deprecated Submonoid.IsMulPointed (since := "2026-10-28")]

class GroupConeClass (S : Type u_2) (G : outParam (Type u_3)) [CommGroup G] [SetLike S G] extends SubmonoidClass S G : Prop

GroupConeClass S G says that S is a type of cones in G.

• mul_mem {s : S} {a b : G} : a ∈ s → b ∈ s → a * b ∈ s
• one_mem (s : S) : 1 ∈ s
• eq_one_of_mem_of_inv_mem {C : S} {a : G} : a ∈ C → a⁻¹ ∈ C → a = 1

@[deprecated AddSubmonoid.IsPointed (since := "2026-10-28")]

structure AddGroupCone (G : Type u_2) [AddCommGroup G] extends AddSubmonoid G : Type u_2

A (positive) cone in an abelian group is a submonoid that does not contain both a and -a for any nonzero a. This is equivalent to being the set of non-negative elements of some order making the group into a partially ordered group.

• carrier : Set G
• add_mem' {a b : G} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• eq_zero_of_mem_of_neg_mem' {a : G} : a ∈ self.carrier → -a ∈ self.carrier → a = 0

@[deprecated Submonoid.IsMulPointed (since := "2026-10-28")]

structure GroupCone (G : Type u_2) [CommGroup G] extends Submonoid G : Type u_2

A (positive) cone in an abelian group is a submonoid that does not contain both a and a⁻¹ for any non-identity a. This is equivalent to being the set of elements that are at least 1 in some order making the group into a partially ordered group.

• carrier : Set G
• mul_mem' {a b : G} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• eq_one_of_mem_of_inv_mem' {a : G} : a ∈ self.carrier → a⁻¹ ∈ self.carrier → a = 1

@[instance_reducible, deprecated "no replacement" (since := "2026-10-28")]

instance GroupCone.instSetLike (G : Type u_2) [CommGroup G] : SetLike (GroupCone G) G

Equations

• GroupCone.instSetLike G = { coe := fun (C : GroupCone G) => C.carrier, coe_injective := ⋯ }

@[instance_reducible, deprecated "no replacement" (since := "2026-10-28")]

instance AddGroupCone.instSetLike (G : Type u_2) [AddCommGroup G] : SetLike (AddGroupCone G) G

Equations

• AddGroupCone.instSetLike G = { coe := fun (C : AddGroupCone G) => C.carrier, coe_injective := ⋯ }

@[instance_reducible, deprecated "no replacement" (since := "2026-10-28")]

instance instPartialOrderGroupCone (G : Type u_2) [CommGroup G] : PartialOrder (GroupCone G)

Equations

• instPartialOrderGroupCone G = PartialOrder.ofSetLike (GroupCone G)

@[instance_reducible, deprecated "no replacement" (since := "2026-10-28")]

instance instPartialOrderAddGroupCone (G : Type u_2) [AddCommGroup G] : PartialOrder (AddGroupCone G)

Equations

• instPartialOrderAddGroupCone G = PartialOrder.ofSetLike (AddGroupCone G)

@[deprecated "no replacement" (since := "2026-10-28")]

instance GroupCone.instGroupConeClass (G : Type u_2) [CommGroup G] : GroupConeClass (GroupCone G) G

@[deprecated "no replacement" (since := "2026-10-28")]

instance AddGroupCone.instAddGroupConeClass (G : Type u_2) [AddCommGroup G] : AddGroupConeClass (AddGroupCone G) G

@[deprecated Submonoid.IsMulPointed.oneLE (since := "2026-10-28")]

def GroupCone.oneLE (H : Type u_2) [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] : GroupCone H

The cone of elements that are at least 1.

Equations

• GroupCone.oneLE H = { toSubmonoid := Submonoid.oneLE H, eq_one_of_mem_of_inv_mem' := ⋯ }

@[deprecated AddSubmonoid.IsPointed.nonneg (since := "2026-10-28")]

def AddGroupCone.nonneg (H : Type u_2) [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] : AddGroupCone H

The cone of non-negative elements.

Equations

• AddGroupCone.nonneg H = { toAddSubmonoid := AddSubmonoid.nonneg H, eq_zero_of_mem_of_neg_mem' := ⋯ }

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem GroupCone.oneLE_toSubmonoid {H : Type u_2} [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] : (oneLE H).toSubmonoid = Submonoid.oneLE H

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem AddGroupCone.nonneg_toAddSubmonoid {H : Type u_2} [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] : (nonneg H).toAddSubmonoid = AddSubmonoid.nonneg H

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem GroupCone.mem_oneLE {H : Type u_2} [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] {a : H} : a ∈ oneLE H ↔ 1 ≤ a

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem AddGroupCone.mem_nonneg {H : Type u_2} [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {a : H} : a ∈ nonneg H ↔ 0 ≤ a

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem GroupCone.coe_oneLE {H : Type u_2} [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] : ↑(oneLE H) = {x : H | 1 ≤ x}

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem AddGroupCone.coe_nonneg {H : Type u_2} [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] : ↑(nonneg H) = {x : H | 0 ≤ x}

@[deprecated Submonoid.IsMulSpanning.oneLE (since := "2026-10-28")]

instance GroupCone.oneLE.hasMemOrInvMem {H : Type u_3} [CommGroup H] [LinearOrder H] [IsOrderedMonoid H] : HasMemOrInvMem (oneLE H)

@[deprecated AddSubmonoid.IsSpanning.nonneg (since := "2026-10-28")]

instance AddGroupCone.nonneg.hasMemOrNegMem {H : Type u_3} [AddCommGroup H] [LinearOrder H] [IsOrderedAddMonoid H] : HasMemOrNegMem (nonneg H)

@[reducible, inline, deprecated PartialOrder.ofSubmonoid (since := "2026-10-28")]

abbrev PartialOrder.mkOfGroupCone {S : Type u_2} {G : Type u_3} [CommGroup G] [SetLike S G] (C : S) [GroupConeClass S G] : PartialOrder G

Construct a partial order by designating a cone in an abelian group.

Equations

• PartialOrder.mkOfGroupCone C = { le := fun (a b : G) => b / a ∈ C, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[reducible, inline, deprecated PartialOrder.ofAddSubmonoid (since := "2026-10-28")]

abbrev PartialOrder.mkOfAddGroupCone {S : Type u_2} {G : Type u_3} [AddCommGroup G] [SetLike S G] (C : S) [AddGroupConeClass S G] : PartialOrder G

Construct a partial order by designating a cone in an abelian group.

Equations

• PartialOrder.mkOfAddGroupCone C = { le := fun (a b : G) => b - a ∈ C, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[deprecated PartialOrder.ofSubmonoid_le_iff (since := "2026-10-28")]

theorem PartialOrder.mkOfGroupCone_le_iff {S : Type u_4} {G : Type u_5} [CommGroup G] [SetLike S G] [GroupConeClass S G] {C : S} {a b : G} : a ≤ b ↔ b / a ∈ C

@[deprecated PartialOrder.ofAddSubmonoid_le_iff (since := "2026-10-28")]

theorem PartialOrder.mkOfAddGroupCone_le_iff {S : Type u_4} {G : Type u_5} [AddCommGroup G] [SetLike S G] [AddGroupConeClass S G] {C : S} {a b : G} : a ≤ b ↔ b - a ∈ C

@[reducible, inline, deprecated LinearOrder.ofSubmonoid (since := "2026-10-28")]

abbrev LinearOrder.mkOfGroupCone {S : Type u_2} {G : Type u_3} [CommGroup G] [SetLike S G] (C : S) [GroupConeClass S G] [HasMemOrInvMem C] [DecidablePred fun (x : G) => x ∈ C] : LinearOrder G

Construct a linear order by designating a maximal cone in an abelian group.

Equations

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

@[reducible, inline, deprecated LinearOrder.ofAddSubmonoid (since := "2026-10-28")]

abbrev LinearOrder.mkOfAddGroupCone {S : Type u_2} {G : Type u_3} [AddCommGroup G] [SetLike S G] (C : S) [AddGroupConeClass S G] [HasMemOrNegMem C] [DecidablePred fun (x : G) => x ∈ C] : LinearOrder G

Construct a linear order by designating a maximal cone in an abelian group.

Equations

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

@[deprecated IsOrderedMonoid.ofSubmonoid (since := "2026-10-28")]

theorem IsOrderedMonoid.mkOfCone {S : Type u_2} {G : Type u_3} [CommGroup G] [SetLike S G] (C : S) [GroupConeClass S G] : have x := PartialOrder.mkOfGroupCone C; IsOrderedMonoid G

Construct a partially ordered abelian group by designating a cone in an abelian group.

@[deprecated IsOrderedAddMonoid.ofAddSubmonoid (since := "2026-10-28")]

theorem IsOrderedAddMonoid.mkOfCone {S : Type u_2} {G : Type u_3} [AddCommGroup G] [SetLike S G] (C : S) [AddGroupConeClass S G] : have x := PartialOrder.mkOfAddGroupCone C; IsOrderedAddMonoid G

Construct a partially ordered abelian group by designating a cone in an abelian group.