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 : Type u_2) [AddCommGroup G] [SetLike S G] extends AddSubmonoidClass : Prop

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

• add_mem : ∀ {s : S} {a b : G}, a ∈ s → b ∈ s → a + b ∈ s
• zero_mem : ∀ (s : S), 0 ∈ s
• eq_zero_of_mem_of_neg_mem : ∀ {C : S} {a : G}, a ∈ C → -a ∈ C → a = 0

theorem AddGroupConeClass.eq_zero_of_mem_of_neg_mem {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [self : AddGroupConeClass S G] {C : S} {a : G} : a ∈ C → -a ∈ C → a = 0

class GroupConeClass (S : Type u_1) (G : Type u_2) [CommGroup G] [SetLike S G] extends SubmonoidClass : Prop

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

• mul_mem : ∀ {s : S} {a b : G}, a ∈ s → b ∈ s → a * b ∈ s
• one_mem : ∀ (s : S), 1 ∈ s
• eq_one_of_mem_of_inv_mem : ∀ {C : S} {a : G}, a ∈ C → a⁻¹ ∈ C → a = 1

theorem GroupConeClass.eq_one_of_mem_of_inv_mem {S : Type u_1} {G : Type u_2} [CommGroup G] [SetLike S G] [self : GroupConeClass S G] {C : S} {a : G} : a ∈ C → a⁻¹ ∈ C → a = 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.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• eq_zero_of_mem_of_neg_mem' : ∀ {a : G}, a ∈ self.carrier → -a ∈ self.carrier → a = 0

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.carrier → a = 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.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• eq_one_of_mem_of_inv_mem' : ∀ {a : G}, a ∈ self.carrier → a⁻¹ ∈ self.carrier → a = 1

theorem GroupCone.eq_one_of_mem_of_inv_mem' {G : Type u_1} [CommGroup G] (self : GroupCone G) {a : G} : a ∈ self.carrier → a⁻¹ ∈ self.carrier → a = 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

instance AddGroupCone.instSetLike (G : Type u_1) [AddCommGroup G] : SetLike (AddGroupCone G) G

Equations

• AddGroupCone.instSetLike G = { coe := fun (C : AddGroupCone G) => C.carrier, coe_injective' := ⋯ }

instance GroupCone.instSetLike (G : Type u_1) [CommGroup G] : SetLike (GroupCone G) G

Equations

• GroupCone.instSetLike G = { coe := fun (C : GroupCone G) => C.carrier, coe_injective' := ⋯ }

instance AddGroupCone.instAddGroupConeClass (G : Type u_1) [AddCommGroup G] : AddGroupConeClass (AddGroupCone G) G

Equations

• ⋯ = ⋯

instance GroupCone.instGroupConeClass (G : Type u_1) [CommGroup G] : GroupConeClass (GroupCone G) G

Equations

• ⋯ = ⋯

class IsMaxCone {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] (C : S) : Prop

Typeclass for maximal additive cones.

• mem_or_neg_mem : ∀ (a : G), a ∈ C ∨ -a ∈ C

theorem IsMaxCone.mem_or_neg_mem {S : Type u_1} {G : Type u_2} [AddCommGroup G] [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) : Prop

Typeclass for maximal multiplicative cones.

• mem_or_inv_mem : ∀ (a : G), a ∈ C ∨ a⁻¹ ∈ C

theorem IsMaxMulCone.mem_or_inv_mem {S : Type u_1} {G : Type u_2} [CommGroup G] [SetLike S G] {C : S} [self : IsMaxMulCone C] (a : G) : a ∈ C ∨ a⁻¹ ∈ C

def AddGroupCone.nonneg (H : Type u_1) [OrderedAddCommGroup H] : AddGroupCone H

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

Equations

• AddGroupCone.nonneg H = { toAddSubmonoid := AddSubmonoid.nonneg H, eq_zero_of_mem_of_neg_mem' := ⋯ }

theorem AddGroupCone.nonneg.proof_1 (H : Type u_1) [OrderedAddCommGroup H] {a : H} : a ∈ (AddSubmonoid.nonneg H).carrier → -a ∈ (AddSubmonoid.nonneg H).carrier → a = 0

def GroupCone.oneLE (H : Type u_1) [OrderedCommGroup H] : GroupCone H

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

Equations

• GroupCone.oneLE H = { toSubmonoid := Submonoid.oneLE H, eq_one_of_mem_of_inv_mem' := ⋯ }

@[simp]

theorem AddGroupCone.nonneg_toAddSubmonoid {H : Type u_1} [OrderedAddCommGroup H] : (AddGroupCone.nonneg H).toAddSubmonoid = AddSubmonoid.nonneg H

@[simp]

theorem GroupCone.oneLE_toSubmonoid {H : Type u_1} [OrderedCommGroup H] : (GroupCone.oneLE H).toSubmonoid = Submonoid.oneLE H

@[simp]

theorem AddGroupCone.mem_nonneg {H : Type u_1} [OrderedAddCommGroup H] {a : H} : a ∈ AddGroupCone.nonneg H ↔ 0 ≤ a

@[simp]

theorem GroupCone.mem_oneLE {H : Type u_1} [OrderedCommGroup H] {a : H} : a ∈ GroupCone.oneLE H ↔ 1 ≤ a

@[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}

instance AddGroupCone.nonneg.isMaxCone {H : Type u_2} [LinearOrderedAddCommGroup H] : IsMaxCone (AddGroupCone.nonneg H)

Equations

• ⋯ = ⋯

instance GroupCone.oneLE.isMaxMulCone {H : Type u_2} [LinearOrderedCommGroup H] : IsMaxMulCone (GroupCone.oneLE H)

Equations

• ⋯ = ⋯

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]

def OrderedAddCommGroup.mkOfCone {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] (C : S) [AddGroupConeClass S G] : OrderedAddCommGroup G

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

Equations

• OrderedAddCommGroup.mkOfCone C = OrderedAddCommGroup.mk ⋯

@[reducible]

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

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

Equations

• OrderedCommGroup.mkOfCone C = OrderedCommGroup.mk ⋯

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) : LinearOrderedAddCommGroup G

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

Equations

• LinearOrderedAddCommGroup.mkOfCone C dec = LinearOrderedAddCommGroup.mk ⋯ (fun (a b : G) => dec (b - a)) decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯

@[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) : LinearOrderedCommGroup G

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

Equations

• LinearOrderedCommGroup.mkOfCone C dec = LinearOrderedCommGroup.mk ⋯ (fun (a b : G) => dec (b / a)) decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯