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.
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
Interpret a cone in a ring as a cone in the underlying additive group.
Equations
- self.toAddGroupCone = { carrier := self.carrier, add_mem' := ⋯, zero_mem' := ⋯, eq_zero_of_mem_of_neg_mem' := ⋯ }
Instances For
Equations
- RingCone.instSetLike R = { coe := fun (C : RingCone R) => C.carrier, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
Construct a partially ordered ring by designating a cone in a ring.
Warning: using this def as a constructor in an instance can lead to diamonds
due to non-customisable field: lt
.
Equations
- OrderedRing.mkOfCone C = OrderedRing.mk ⋯ ⋯ ⋯
Instances For
Construct a linearly ordered domain by designating a maximal cone in a domain.
Warning: using this def as a constructor in an instance can lead to diamonds
due to non-customisable fields: lt
, decidableLT
, decidableEq
, compare
.
Equations
- LinearOrderedRing.mkOfCone C dec = LinearOrderedRing.mk ⋯ (fun (a b : R) => dec (b - a)) decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯