Documentation

Mathlib.Algebra.Order.Group.Cone

Construct ordered groups from groups with a specified positive cone. #

In this file we provide the structure GroupCone and the predicate IsMaxCone that encode axioms of OrderedCommGroup and LinearOrderedCommGroup in terms of the subset of non-negative elements.

We also provide constructors that convert between cones in groups and the corresponding ordered groups.

class AddGroupConeClass (S : Type u_1) (G : outParam (Type u_2)) [AddCommGroup G] [SetLike S G] extends AddSubmonoidClass :

AddGroupConeClass S G says that S is a type of cones in G.

  • add_mem : ∀ {s : S} {a b : G}, a sb sa + b s
  • zero_mem : ∀ (s : S), 0 s
  • eq_zero_of_mem_of_neg_mem : ∀ {C : S} {a : G}, a C-a Ca = 0
Instances
    theorem AddGroupConeClass.eq_zero_of_mem_of_neg_mem {S : Type u_1} {G : outParam (Type u_2)} :
    ∀ {inst : AddCommGroup G} {inst_1 : SetLike S G} [self : AddGroupConeClass S G] {C : S} {a : G}, a C-a Ca = 0
    class GroupConeClass (S : Type u_1) (G : Type u_2) [CommGroup G] [SetLike S G] extends SubmonoidClass :

    GroupConeClass S G says that S is a type of cones in G.

    • mul_mem : ∀ {s : S} {a b : G}, a sb sa * b s
    • one_mem : ∀ (s : S), 1 s
    • eq_one_of_mem_of_inv_mem : ∀ {C : S} {a : G}, a Ca⁻¹ Ca = 1
    Instances
      theorem GroupConeClass.eq_one_of_mem_of_inv_mem {S : Type u_1} {G : Type u_2} :
      ∀ {inst : CommGroup G} {inst_1 : SetLike S G} [self : GroupConeClass S G] {C : S} {a : G}, a Ca⁻¹ Ca = 1
      structure AddGroupCone (G : Type u_1) [AddCommGroup G] extends AddSubmonoid :
      Type u_1

      A (positive) cone in an abelian group is a submonoid 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 group into a partially ordered group.

      • carrier : Set G
      • add_mem' : ∀ {a b : G}, a self.carrierb self.carriera + b self.carrier
      • zero_mem' : 0 self.carrier
      • eq_zero_of_mem_of_neg_mem' : ∀ {a : G}, a self.carrier-a self.carriera = 0
      Instances For
        theorem AddGroupCone.eq_zero_of_mem_of_neg_mem' {G : Type u_1} [AddCommGroup G] (self : AddGroupCone G) {a : G} :
        a self.carrier-a self.carriera = 0
        structure GroupCone (G : Type u_1) [CommGroup G] extends Submonoid :
        Type u_1

        A (positive) cone in an abelian group is a submonoid that does not contain both a and a⁻¹ for any non-identity a. This is equivalent to being the set of elements that are at least 1 in some order making the group into a partially ordered group.

        • carrier : Set G
        • mul_mem' : ∀ {a b : G}, a self.carrierb self.carriera * b self.carrier
        • one_mem' : 1 self.carrier
        • eq_one_of_mem_of_inv_mem' : ∀ {a : G}, a self.carriera⁻¹ self.carriera = 1
        Instances For
          theorem GroupCone.eq_one_of_mem_of_inv_mem' {G : Type u_1} [CommGroup G] (self : GroupCone G) {a : G} :
          a self.carriera⁻¹ self.carriera = 1
          theorem AddGroupCone.instSetLike.proof_1 (G : Type u_1) [AddCommGroup G] (p : AddGroupCone G) (q : AddGroupCone G) (h : (fun (C : AddGroupCone G) => C.carrier) p = (fun (C : AddGroupCone G) => C.carrier) q) :
          p = q
          Equations
          instance GroupCone.instSetLike (G : Type u_1) [CommGroup G] :
          Equations
          Equations
          • =
          class IsMaxCone {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] (C : S) :

          Typeclass for maximal additive cones.

          • mem_or_neg_mem : ∀ (a : G), a C -a C
          Instances
            theorem IsMaxCone.mem_or_neg_mem {S : Type u_1} {G : Type u_2} :
            ∀ {inst : AddCommGroup G} {inst_1 : SetLike S G} {C : S} [self : IsMaxCone C] (a : G), a C -a C
            class IsMaxMulCone {S : Type u_1} {G : Type u_2} [CommGroup G] [SetLike S G] (C : S) :

            Typeclass for maximal multiplicative cones.

            Instances
              theorem IsMaxMulCone.mem_or_inv_mem {S : Type u_1} {G : Type u_2} :
              ∀ {inst : CommGroup G} {inst_1 : SetLike S G} {C : S} [self : IsMaxMulCone C] (a : G), a C a⁻¹ C

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

              Equations
              Instances For
                theorem AddGroupCone.nonneg.proof_1 (H : Type u_1) [OrderedAddCommGroup H] {a : H} :
                a (AddSubmonoid.nonneg H).carrier-a (AddSubmonoid.nonneg H).carriera = 0

                Construct a cone from the set of elements of a partially ordered abelian group that are at least 1.

                Equations
                Instances For
                  @[simp]
                  theorem GroupCone.mem_oneLE {H : Type u_1} [OrderedCommGroup H] {a : H} :
                  @[simp]
                  theorem AddGroupCone.coe_nonneg {H : Type u_1} [OrderedAddCommGroup H] :
                  (AddGroupCone.nonneg H) = {x : H | 0 x}
                  @[simp]
                  theorem GroupCone.coe_oneLE {H : Type u_1} [OrderedCommGroup H] :
                  (GroupCone.oneLE H) = {x : H | 1 x}
                  theorem OrderedAddCommGroup.mkOfCone.proof_2 {S : Type u_2} {G : Type u_1} [AddCommGroup G] [SetLike S G] (C : S) [AddGroupConeClass S G] (a : G) (b : G) (c : G) (nab : a b) (nbc : b c) :
                  a c
                  theorem OrderedAddCommGroup.mkOfCone.proof_3 {S : Type u_2} {G : Type u_1} [AddCommGroup G] [SetLike S G] (C : S) :
                  ∀ (a b : G), a < b a < b
                  theorem OrderedAddCommGroup.mkOfCone.proof_1 {S : Type u_2} {G : Type u_1} [AddCommGroup G] [SetLike S G] (C : S) [AddGroupConeClass S G] (a : G) :
                  a - a C
                  theorem OrderedAddCommGroup.mkOfCone.proof_5 {S : Type u_2} {G : Type u_1} [AddCommGroup G] [SetLike S G] (C : S) [AddGroupConeClass S G] (a : G) (b : G) (nab : a b) (c : G) :
                  c + a c + b
                  theorem OrderedAddCommGroup.mkOfCone.proof_4 {S : Type u_2} {G : Type u_1} [AddCommGroup G] [SetLike S G] (C : S) [AddGroupConeClass S G] (a : G) (b : G) (nab : a b) (nba : b a) :
                  a = b
                  @[reducible]

                  Construct a partially ordered abelian group by designating a cone in an abelian group.

                  Equations
                  Instances For
                    @[reducible]
                    def OrderedCommGroup.mkOfCone {S : Type u_1} {G : Type u_2} [CommGroup G] [SetLike S G] (C : S) [GroupConeClass S G] :

                    Construct a partially ordered abelian group by designating a cone in an abelian group.

                    Equations
                    Instances For
                      theorem LinearOrderedAddCommGroup.mkOfCone.proof_2 {S : Type u_2} {G : Type u_1} [AddCommGroup G] [SetLike S G] (C : S) [AddGroupConeClass S G] (dec : DecidablePred fun (x : G) => x C) :
                      ∀ (a b : G), min a b = min a b
                      theorem LinearOrderedAddCommGroup.mkOfCone.proof_4 {S : Type u_2} {G : Type u_1} [AddCommGroup G] [SetLike S G] (C : S) [AddGroupConeClass S G] (dec : DecidablePred fun (x : G) => x C) :
                      ∀ (a b : G), compare a b = compare a b
                      theorem LinearOrderedAddCommGroup.mkOfCone.proof_1 {S : Type u_2} {G : Type u_1} [AddCommGroup G] [SetLike S G] (C : S) [AddGroupConeClass S G] [IsMaxCone C] (a : G) (b : G) :
                      a b b a
                      theorem LinearOrderedAddCommGroup.mkOfCone.proof_3 {S : Type u_2} {G : Type u_1} [AddCommGroup G] [SetLike S G] (C : S) [AddGroupConeClass S G] (dec : DecidablePred fun (x : G) => x C) :
                      ∀ (a b : G), max a b = max a b
                      @[reducible]
                      def LinearOrderedAddCommGroup.mkOfCone {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] (C : S) [AddGroupConeClass S G] [IsMaxCone C] (dec : DecidablePred fun (x : G) => x C) :

                      Construct a linearly ordered abelian group by designating a maximal cone in an abelian group.

                      Equations
                      Instances For
                        @[reducible]
                        def LinearOrderedCommGroup.mkOfCone {S : Type u_1} {G : Type u_2} [CommGroup G] [SetLike S G] (C : S) [GroupConeClass S G] [IsMaxMulCone C] (dec : DecidablePred fun (x : G) => x C) :

                        Construct a linearly ordered abelian group by designating a maximal cone in an abelian group.

                        Equations
                        Instances For