Documentation

Mathlib.Algebra.Order.Ring.Ordering.Defs

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

  1. O contains either x or -x for each x in R and
  2. 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 #

structure RingPreordering (R : Type u_1) [CommRing R] extends Subsemiring R :
Type u_1

A preordering on a ring R is a subsemiring of R containing all squares, but not containing -1.

Instances For
    theorem RingPreordering.ext {R : Type u_1} {inst✝ : CommRing R} {x y : RingPreordering R} (carrier : (↑x).carrier = (↑y).carrier) :
    x = y
    theorem RingPreordering.ext_iff {R : Type u_1} {inst✝ : CommRing R} {x y : RingPreordering R} :
    x = y (↑x).carrier = (↑y).carrier
    Equations
    theorem RingPreordering.mem_of_isSquare {R : Type u_1} [CommRing R] (P : RingPreordering R) {x : R} (hx : IsSquare x) :
    x P
    @[simp]
    theorem RingPreordering.mul_self_mem {R : Type u_1} [CommRing R] (P : RingPreordering R) (x : R) :
    x * x P
    @[simp]
    theorem RingPreordering.pow_two_mem {R : Type u_1} [CommRing R] (P : RingPreordering R) (x : R) :
    x ^ 2 P
    theorem RingPreordering.neg_one_notMem {R : Type u_1} [CommRing R] (P : RingPreordering R) :
    -1P
    @[simp]
    theorem RingPreordering.toSubsemiring_inj {R : Type u_1} [CommRing R] {P₁ P₂ : RingPreordering R} :
    P₁ = P₂ P₁ = P₂
    @[simp]
    theorem RingPreordering.mem_toSubsemiring {R : Type u_1} [CommRing R] {P : RingPreordering R} {x : R} :
    x P x P
    @[simp]
    theorem RingPreordering.coe_toSubsemiring {R : Type u_1} [CommRing R] (P : RingPreordering R) :
    P = P
    @[simp]
    theorem RingPreordering.mem_mk {R : Type u_1} [CommRing R] {toSubsemiring : Subsemiring R} (mem_of_isSquare : ∀ {x : R}, IsSquare xx toSubsemiring.carrier) (neg_one_notMem : -1toSubsemiring.carrier) {x : R} :
    x { toSubsemiring := toSubsemiring, mem_of_isSquare' := mem_of_isSquare, neg_one_notMem' := neg_one_notMem } x toSubsemiring
    @[simp]
    theorem RingPreordering.coe_set_mk {R : Type u_1} [CommRing R] (toSubsemiring : Subsemiring R) (mem_of_isSquare : ∀ {x : R}, IsSquare xx toSubsemiring.carrier) (neg_one_notMem : -1toSubsemiring.carrier) :
    { toSubsemiring := toSubsemiring, mem_of_isSquare' := mem_of_isSquare, neg_one_notMem' := neg_one_notMem } = toSubsemiring
    def RingPreordering.copy {R : Type u_1} [CommRing R] (P : RingPreordering R) (S : Set R) (hS : S = P) :

    Copy of a preordering with a new carrier equal to the old one. Useful to fix definitional equalities.

    Equations
    • P.copy S hS = { carrier := S, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , mem_of_isSquare' := , neg_one_notMem' := }
    Instances For
      @[simp]
      theorem RingPreordering.coe_copy {R : Type u_1} [CommRing R] (P : RingPreordering R) (S : Set R) (hS : S = P) :
      (P.copy S hS) = S
      @[simp]
      theorem RingPreordering.mem_copy {R : Type u_1} [CommRing R] (P : RingPreordering R) (S : Set R) (hS : S = P) {x : R} :
      x P.copy S hS x S
      theorem RingPreordering.copy_eq {R : Type u_1} [CommRing R] (P : RingPreordering R) (S : Set R) (hS : S = P) :
      (P.copy S hS) = S

      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
          theorem RingPreordering.hasIdealSupport_iff {R : Type u_1} [CommRing R] {P : RingPreordering R} :
          P.HasIdealSupport ∀ (x a : R), a P-a Px * a P -(x * a) P

          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

            An ordering O on a ring R is a preordering such that

            1. O contains either x or -x for each x in R and
            2. the support of O is a prime ideal.
            Instances