Construct ordered rings from rings with a specified positive cone. #
In this file we provide the structure RingCone
that encodes axioms of OrderedRing
and LinearOrderedRing
in terms of the subset of non-negative elements.
We also provide constructors that convert between cones in rings and the corresponding ordered rings.
class
RingConeClass
(S : Type u_1)
(R : outParam (Type u_2))
[Ring R]
[SetLike S R]
extends AddGroupConeClass S R, SubsemiringClass S R :
RingConeClass S R
says that S
is a type of cones in R
.
Instances
A (positive) cone in a ring is a subsemiring 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 ring into a partially ordered ring.
Instances For
Equations
- RingCone.instSetLike R = { coe := fun (C : RingCone R) => C.carrier, coe_injective' := ⋯ }
Construct a cone from the set of non-negative elements of a partially ordered ring.
Equations
- RingCone.nonneg T = { toSubsemiring := Subsemiring.nonneg T, eq_zero_of_mem_of_neg_mem' := ⋯ }
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
instance
RingCone.nonneg.isMaxCone
{T : Type u_2}
[Ring T]
[LinearOrder T]
[IsStrictOrderedRing T]
:
theorem
IsOrderedRing.mkOfCone
{S : Type u_1}
{R : Type u_2}
[Ring R]
[SetLike S R]
(C : S)
[RingConeClass S R]
:
Construct a partially ordered ring by designating a cone in a ring.