Documentation

RealClosedField.Algebra.Order.Cone.Defs

Positive cones #

A positive cone in an (additive) group G is a submonoid C with zero support (i.e. C ∩ -C = 0).

A positive cone in a ring R is a subsemiring C with zero (additive) support. We re-use the predicate from the group case.

Positive cones correspond to ordered group structures: see Algebra.Order.Cone.Order.

Main definitions #

source
class AddSubmonoid.IsCone {G : Type u_1} [AddGroup G] (M : AddSubmonoid G) :
Prop

Typeclass for submonoids with zero support.

  • eq_zero_of_mem_of_neg_mem {x : G} (hx₁ : x ∈ M) (hx₂ : -x ∈ M) : x = 0
Instances
    source
    class Submonoid.IsMulCone {G : Type u_1} [Group G] (M : Submonoid G) :
    Prop

    Typeclass for submonoids with zero support.

    • eq_one_of_mem_of_inv_mem {x : G} (hx₁ : x ∈ M) (hx₂ : x⁻¹ ∈ M) : x = 1
    Instances
      source
      theorem Submonoid.eq_one_of_mem_of_inv_mem₂ {G : Type u_1} {inst✝ : Group G} {M : Submonoid G} [self : M.IsMulCone] {x : G} (hx₁ : x ∈ M) (hx₂ : x⁻¹ ∈ M) :
      x = 1

      Alias of Submonoid.IsMulCone.eq_one_of_mem_of_inv_mem.

      source
      theorem AddSubmonoid.eq_zero_of_mem_of_neg_mem₂ {G : Type u_1} {inst✝ : AddGroup G} {M : AddSubmonoid G} [self : M.IsCone] {x : G} (hx₁ : x ∈ M) (hx₂ : -x ∈ M) :
      x = 0
      source
      @[simp]
      theorem Submonoid.supportSubgroup_eq_bot {G : Type u_1} [Group G] (M : Submonoid G) [M.IsMulCone] :
      M.supportSubgroup = ⊥
      source
      @[simp]
      theorem AddSubmonoid.supportAddSubgroup_eq_bot {G : Type u_1} [AddGroup G] (M : AddSubmonoid G) [M.IsCone] :
      M.supportAddSubgroup = ⊥
      source
      instance Submonoid.instIsMulConeOneLE (G : Type u_1) [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] :
      (oneLE G).IsMulCone
      source
      instance AddSubmonoid.instIsAddConeNonneg (G : Type u_1) [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] :
      (nonneg G).IsCone
      source
      instance Submonoid.instHasMemOrInvMemOneLE (G : Type u_1) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] :
      (oneLE G).HasMemOrInvMem
      source
      instance AddSubmonoid.instHasMemOrNegMemNonneg (G : Type u_1) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] :
      (nonneg G).HasMemOrNegMem
      source
      instance AddSubmonoid.instHasIdealSupportOfIsCone {R : Type u_1} [Ring R] (M : AddSubmonoid R) [M.IsCone] :
      M.HasIdealSupport
      source
      @[simp]
      theorem AddSubmonoid.support_eq_bot {R : Type u_1} [Ring R] (M : AddSubmonoid R) [M.IsCone] :
      M.support = ⊥
      source
      theorem AddSubmonoid.IsCone.of_support_eq_bot {R : Type u_1} [Ring R] (M : AddSubmonoid R) [M.HasIdealSupport] (h : M.support = ⊥) :
      M.IsCone
      source
      theorem AddSubmonoid.IsCone.maximal {R : Type u_1} [Ring R] (M : AddSubmonoid R) [M.IsCone] [M.HasMemOrNegMem] :
      Maximal IsCone M
      source
      theorem Subsemiring.IsCone.neg_one_notMem {R : Type u_1} [Ring R] (C : Subsemiring R) [Nontrivial R] [C.toAddSubmonoid.IsCone] :
      -1 ∉ C
      source
      instance Subsemiring.instHasMemOrNegMemToAddSubmonoidNonneg {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] :
      (nonneg R).toAddSubmonoid.HasMemOrNegMem
      source
      instance Subsemiring.instIsConeToAddSubmonoidNonneg {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] :
      (nonneg R).toAddSubmonoid.IsCone