Documentation

Mathlib.Algebra.Order.Ring.Cone

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 , SubmonoidClass :

RingConeClass S R says that S is a type of cones in R.

    Instances
      structure RingCone (R : Type u_1) [Ring R] extends Subsemiring :
      Type u_1

      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.

      • carrier : Set R
      • mul_mem' : ∀ {a b : R}, a self.carrierb self.carriera * b self.carrier
      • one_mem' : 1 self.carrier
      • add_mem' : ∀ {a b : R}, a self.carrierb self.carriera + b self.carrier
      • zero_mem' : 0 self.carrier
      • eq_zero_of_mem_of_neg_mem' : ∀ {a : R}, a self.carrier-a self.carriera = 0
      Instances For
        @[reducible]
        abbrev RingCone.toAddGroupCone {R : Type u_1} [Ring R] (self : RingCone R) :

        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
          instance RingCone.instSetLike (R : Type u_1) [Ring R] :
          Equations
          Equations
          • =

          Construct a cone from the set of non-negative elements of a partially ordered ring.

          Equations
          Instances For
            @[simp]
            @[simp]
            theorem RingCone.mem_nonneg {T : Type u_1} [OrderedRing T] {a : T} :
            @[simp]
            theorem RingCone.coe_nonneg {T : Type u_1} [OrderedRing T] :
            (RingCone.nonneg T) = {x : T | 0 x}
            @[reducible]
            def OrderedRing.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. Warning: using this def as a constructor in an instance can lead to diamonds due to non-customisable field: lt.

            Equations
            Instances For
              @[reducible]
              def LinearOrderedRing.mkOfCone {S : Type u_1} {R : Type u_2} [Ring R] [SetLike S R] (C : S) [IsDomain R] [RingConeClass S R] [IsMaxCone C] (dec : DecidablePred fun (x : R) => x C) :

              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
              Instances For