Equivalence between positive cones and order structures

Positive cones in an abelian group G correspond to ordered group structures on G. Positive cones in a ring R correspond to ordered ring structures on R. In each case, the cone corresponds to the set of non-negative elements. If the cone C satisfies C ∪ -C = ⊤, the induced order is total.

Main definitions

• AddCommGroup.isConePartialOrderEquiv and AddCommGroup.isConeLinearOrderEquiv: equivalence between (maximal) cones in an abelian group G and (linearly) ordered group structures on G.
• Ring.isConePartialOrderEquiv and Ring.isConeLinearOrderEquiv: equivalence between (maximal) cones in an ring R and (linearly) ordered ring structures on R.
• AddCommGroup.addSubmonoidPartialOrderEquiv and AddCommGroup.addSubmonoidLinearOrderEquiv: equivalence between submonoids H of an abelian group G (satisfying H ∪ -H = G) and (linearly) ordered group structures on R ⧸ H.supportAddSubgroup.
• Ring.subsemiringPartialOrderEquiv and Ring.subsemiringPartialOrderEquiv: equivalence between subsemirings S of a ring R (satisfying S ∪ -S = R) and (linearly) ordered ring structures on R ⧸ S.support.

@[reducible, inline]

abbrev PartialOrder.mkOfSubmonoid {G : Type u_1} [CommGroup G] (S : Submonoid G) [S.IsMulCone] : PartialOrder G

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

Equations

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

@[reducible, inline]

abbrev PartialOrder.mkOfAddSubmonoid {G : Type u_1} [AddCommGroup G] (S : AddSubmonoid G) [S.IsCone] : PartialOrder G

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

Equations

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

@[simp]

theorem PartialOrder.mkOfSubmonoid_le_iff {G : Type u_1} [CommGroup G] {S : Submonoid G} [S.IsMulCone] {a b : G} : a ≤ b ↔ b / a ∈ S

@[simp]

theorem PartialOrder.mkOfAddSubmonoid_le_iff {G : Type u_1} [AddCommGroup G] {S : AddSubmonoid G} [S.IsCone] {a b : G} : a ≤ b ↔ b - a ∈ S

theorem IsOrderedMonoid.mkOfSubmonoid {G : Type u_1} [CommGroup G] (S : Submonoid G) [S.IsMulCone] : IsOrderedMonoid G

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

theorem IsOrderedAddMonoid.mkOfAddSubmonoid {G : Type u_1} [AddCommGroup G] (S : AddSubmonoid G) [S.IsCone] : IsOrderedAddMonoid G

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

@[reducible, inline]

abbrev LinearOrder.mkOfSubmonoid {G : Type u_1} [CommGroup G] (S : Submonoid G) [S.IsMulCone] [S.HasMemOrInvMem] [DecidablePred fun (x : G) => x ∈ S] : 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]

abbrev LinearOrder.mkOfAddSubmonoid {G : Type u_1} [AddCommGroup G] (S : AddSubmonoid G) [S.IsCone] [S.HasMemOrNegMem] [DecidablePred fun (x : G) => x ∈ S] : 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.

noncomputable def CommGroup.isMulConePartialOrderEquiv (G : Type u_1) [CommGroup G] : { C : Submonoid G // C.IsMulCone } ≃ { o : PartialOrder G // IsOrderedMonoid G }

Equivalence between cones in an abelian group G and partially ordered group structures on G.

Equations

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

noncomputable def AddCommGroup.isConePartialOrderEquiv (G : Type u_1) [AddCommGroup G] : { C : AddSubmonoid G // C.IsCone } ≃ { o : PartialOrder G // IsOrderedAddMonoid G }

Equivalence between cones in an abelian group G and partially ordered group structures on G.

Equations

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

@[simp]

theorem CommGroup.isMulConePartialOrderEquiv_apply {G : Type u_1} [CommGroup G] (C : Submonoid G) (h : C.IsMulCone) : ↑((isMulConePartialOrderEquiv G) ⟨C, h⟩) = PartialOrder.mkOfSubmonoid C

@[simp]

theorem AddCommGroup.isConePartialOrderEquiv_apply {G : Type u_1} [AddCommGroup G] (C : AddSubmonoid G) (h : C.IsCone) : ↑((isConePartialOrderEquiv G) ⟨C, h⟩) = PartialOrder.mkOfAddSubmonoid C

@[simp]

theorem CommGroup.isMulConePartialOrderEquiv_symm_apply {G : Type u_1} [CommGroup G] (o : PartialOrder G) (h : IsOrderedMonoid G) : ↑((isMulConePartialOrderEquiv G).symm ⟨o, h⟩) = Submonoid.oneLE G

@[simp]

theorem AddCommGroup.isConePartialOrderEquiv_symm_apply {G : Type u_1} [AddCommGroup G] (o : PartialOrder G) (h : IsOrderedAddMonoid G) : ↑((isConePartialOrderEquiv G).symm ⟨o, h⟩) = AddSubmonoid.nonneg G

noncomputable def CommGroup.isMulConeLinearOrderEquiv (G : Type u_1) [CommGroup G] : { C : Submonoid G // C.IsMulCone ∧ C.HasMemOrInvMem } ≃ { o : LinearOrder G // IsOrderedMonoid G }

Equivalence between maximal cones in an abelian group G and linearly ordered group structures on G.

Equations

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

noncomputable def AddCommGroup.isConeLinearOrderEquiv (G : Type u_1) [AddCommGroup G] : { C : AddSubmonoid G // C.IsCone ∧ C.HasMemOrNegMem } ≃ { o : LinearOrder G // IsOrderedAddMonoid G }

Equivalence between maximal cones in an abelian group G and linearly ordered group structures on G.

Equations

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

@[simp]

theorem CommGroup.isMulConeLinearOrderEquiv_apply {G : Type u_1} [CommGroup G] (C : Submonoid G) (h : C.IsMulCone ∧ C.HasMemOrInvMem) : ↑((isMulConeLinearOrderEquiv G) ⟨C, h⟩) = have this := ⋯; have this_1 := ⋯; LinearOrder.mkOfSubmonoid C

@[simp]

theorem AddCommGroup.isConeLinearOrderEquiv_apply {G : Type u_1} [AddCommGroup G] (C : AddSubmonoid G) (h : C.IsCone ∧ C.HasMemOrNegMem) : ↑((isConeLinearOrderEquiv G) ⟨C, h⟩) = have this := ⋯; have this_1 := ⋯; LinearOrder.mkOfAddSubmonoid C

@[simp]

theorem CommGroup.isMulConeLinearOrderEquiv_symm_apply {G : Type u_1} [CommGroup G] (l : LinearOrder G) (h : IsOrderedMonoid G) : ↑((isMulConeLinearOrderEquiv G).symm ⟨l, h⟩) = Submonoid.oneLE G

@[simp]

theorem AddCommGroup.isConeLinearOrderEquiv_symm_apply {G : Type u_1} [AddCommGroup G] (l : LinearOrder G) (h : IsOrderedAddMonoid G) : ↑((isConeLinearOrderEquiv G).symm ⟨l, h⟩) = AddSubmonoid.nonneg G

theorem IsOrderedRing.mkOfSubsemiring {R : Type u_2} [Ring R] (S : Subsemiring R) [S.toAddSubmonoid.IsCone] : IsOrderedRing R

Construct an ordered ring by designating a cone in a ring.

noncomputable def Ring.isConePartialOrderEquiv (R : Type u_2) [Ring R] : { C : Subsemiring R // C.toAddSubmonoid.IsCone } ≃ { o : PartialOrder R // IsOrderedRing R }

Equivalence between cones in a ring R and partially ordered ring structures on R.

Equations

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

@[simp]

theorem Ring.isConePartialOrderEquiv_apply {R : Type u_2} [Ring R] (C : Subsemiring R) (h : C.toAddSubmonoid.IsCone) : ↑((isConePartialOrderEquiv R) ⟨C, h⟩) = PartialOrder.mkOfAddSubmonoid C.toAddSubmonoid

@[simp]

theorem Ring.isConePartialOrderEquiv_symm_apply {R : Type u_2} [Ring R] (o : PartialOrder R) (h : IsOrderedRing R) : ↑((isConePartialOrderEquiv R).symm ⟨o, h⟩) = Subsemiring.nonneg R

noncomputable def Ring.isConeLinearOrderEquiv (R : Type u_2) [Ring R] : { C : Subsemiring R // C.toAddSubmonoid.IsCone ∧ C.toAddSubmonoid.HasMemOrNegMem } ≃ { o : LinearOrder R // IsOrderedRing R }

Equivalence between maximal cones in a ring R and linearly ordered ring structures on R.

Equations

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

@[simp]

theorem Ring.isConeLinearOrderEquiv_apply {R : Type u_2} [Ring R] (C : Subsemiring R) (h : C.toAddSubmonoid.IsCone ∧ C.toAddSubmonoid.HasMemOrNegMem) : ↑((isConeLinearOrderEquiv R) ⟨C, h⟩) = have this := ⋯; have this_1 := ⋯; LinearOrder.mkOfAddSubmonoid C.toAddSubmonoid

@[simp]

theorem Ring.isConeLinearOrderEquiv_symm_apply {R : Type u_2} [Ring R] (o : LinearOrder R) (h : IsOrderedRing R) : ↑((isConeLinearOrderEquiv R).symm ⟨o, h⟩) = Subsemiring.nonneg R