Ring orderings #
Let R
be a commutative ring. A preordering on R
is a subset closed under
addition and multiplication that contains all squares, but not -1
.
The support of a preordering P
is the set of elements x
such that both x
and -x
lie in P
.
An ordering O
on R
is a preordering such that
O
contains eitherx
or-x
for eachx
inR
and- the support of
O
is a prime ideal.
We define preorderings, supports and orderings.
A ring preordering can intuitively be viewed as a set of "non-negative" ring elements.
Indeed, an ordering O
with support p
induces a linear order on R⧸p
making it
into an ordered ring, and vice versa.
References #
Preorderings #
A preordering on a ring R
is a subsemiring of R
containing all squares,
but not containing -1
.
- neg_one_notMem' : -1 ∉ (↑self).carrier
Instances For
Equations
- RingPreordering.instSetLike R = { coe := fun (P : RingPreordering R) => (↑P).carrier, coe_injective' := ⋯ }
Copy of a preordering with a new carrier
equal to the old one. Useful to fix definitional
equalities.
Equations
Instances For
Support #
The support of a ring preordering P
in a commutative ring R
is
the set of elements x
in R
such that both x
and -x
lie in P
.
Equations
Instances For
Typeclass to track whether the support of a preordering forms an ideal.
Instances
The support of a ring preordering P
in a commutative ring R
is
the set of elements x
in R
such that both x
and -x
lie in P
.
Equations
- P.support = { toAddSubmonoid := P.supportAddSubgroup.toAddSubmonoid, smul_mem' := ⋯ }
Instances For
An ordering O
on a ring R
is a preordering such that
O
contains eitherx
or-x
for eachx
inR
and- the support of
O
is a prime ideal.