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.
AddGroupConeClass S G
says that S
is a type of cones in G
.
- zero_mem : ∀ (s : S), 0 ∈ s
Instances
GroupConeClass S G
says that S
is a type of cones in G
.
- one_mem : ∀ (s : S), 1 ∈ s
Instances
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.
Instances For
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.
Instances For
Equations
- AddGroupCone.instSetLike G = { coe := fun (C : AddGroupCone G) => C.carrier, coe_injective' := ⋯ }
Equations
- GroupCone.instSetLike G = { coe := fun (C : GroupCone G) => C.carrier, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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' := ⋯ }
Instances For
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' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Construct a partially ordered abelian group by designating a cone in an abelian group.
Equations
Instances For
Construct a partially ordered abelian group by designating a cone in an abelian group.
Equations
Instances For
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 ⋯ ⋯ ⋯
Instances For
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 ⋯ ⋯ ⋯