Unique products and related notions #
A group G
has unique products if for any two non-empty finite subsets A, B ⊆ G
, there is an
element g ∈ A * B
that can be written uniquely as a product of an element of A
and an element
of B
. We call the formalization this property UniqueProds
. Since the condition requires no
property of the group operation, we define it for a Type simply satisfying Mul
. We also
introduce the analogous "additive" companion, UniqueSums
, and link the two so that to_additive
converts UniqueProds
into UniqueSums
.
A common way of proving that a group satisfies the UniqueProds/Sums
property is by assuming
the existence of some kind of ordering on the group that is well-behaved with respect to the
group operation and showing that minima/maxima are the "unique products/sums".
However, the order is just a convenience and is not part of the UniqueProds/Sums
setup.
Here you can see several examples of Types that have UniqueSums/Prods
(inferInstance
uses Covariant.to_uniqueProds_left
and Covariant.to_uniqueSums_left
).
import Mathlib.Data.Real.Basic
import Mathlib.Data.PNat.Basic
import Mathlib.Algebra.Group.UniqueProds.Basic
example : UniqueSums ℕ := inferInstance
example : UniqueSums ℕ+ := inferInstance
example : UniqueSums ℤ := inferInstance
example : UniqueSums ℚ := inferInstance
example : UniqueSums ℝ := inferInstance
example : UniqueProds ℕ+ := inferInstance
Use in (Add)MonoidAlgebra
s #
UniqueProds/Sums
allow to decouple certain arguments about (Add)MonoidAlgebra
s into an argument
about the grading type and then a generic statement of the form "look at the coefficient of the
'unique product/sum'".
The file Algebra/MonoidAlgebra/NoZeroDivisors
contains several examples of this use.
Alias of UniqueAdd.of_card_le_one
.
Alias of UniqueAdd.iff_card_le_one
.
UniqueAdd
is preserved by inverse images under injective, additive maps.
UniqueMul
is preserved by inverse images under injective, multiplicative maps.
UniqueAdd
is preserved under additive maps that are injective.
See UniqueAdd.addHom_map_iff
for a version with swapped bundling.
Unique_Mul
is preserved under multiplicative maps that are injective.
See UniqueMul.mulHom_map_iff
for a version with swapped bundling.
UniqueAdd
is preserved under embeddings that are additive.
See UniqueAdd.addHom_image_iff
for a version with swapped bundling.
UniqueMul
is preserved under embeddings that are multiplicative.
See UniqueMul.mulHom_image_iff
for a version with swapped bundling.
Let G
be a Type with addition. UniqueSums G
asserts that any two non-empty
finite subsets of G
have the UniqueAdd
property, with respect to some element of their
sum A + B
.
- uniqueAdd_of_nonempty : ∀ {A B : Finset G}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueAdd A B a0 b0
For
A B
two nonempty finite sets, there always exista0 ∈ A, b0 ∈ B
such thatUniqueAdd A B a0 b0
Instances
For A B
two nonempty finite sets, there always exist a0 ∈ A, b0 ∈ B
such that
UniqueAdd A B a0 b0
Let G
be a Type with multiplication. UniqueProds G
asserts that any two non-empty
finite subsets of G
have the UniqueMul
property, with respect to some element of their
product A * B
.
- uniqueMul_of_nonempty : ∀ {A B : Finset G}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
For
A B
two nonempty finite sets, there always exista0 ∈ A, b0 ∈ B
such thatUniqueMul A B a0 b0
Instances
For A B
two nonempty finite sets, there always exist a0 ∈ A, b0 ∈ B
such that
UniqueMul A B a0 b0
Let G
be a Type with addition. TwoUniqueSums G
asserts that any two non-empty
finite subsets of G
, at least one of which is not a singleton, possesses at least two pairs
of elements satisfying the UniqueAdd
property.
- uniqueAdd_of_one_lt_card : ∀ {A B : Finset G}, 1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueAdd A B p1.1 p1.2 ∧ UniqueAdd A B p2.1 p2.2
For
A B
two finite sets whose product has cardinality at least 2, we can find at least two unique pairs.
Instances
For A B
two finite sets whose product has cardinality at least 2,
we can find at least two unique pairs.
Let G
be a Type with multiplication. TwoUniqueProds G
asserts that any two non-empty
finite subsets of G
, at least one of which is not a singleton, possesses at least two pairs
of elements satisfying the UniqueMul
property.
- uniqueMul_of_one_lt_card : ∀ {A B : Finset G}, 1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
For
A B
two finite sets whose product has cardinality at least 2, we can find at least two unique pairs.
Instances
For A B
two finite sets whose product has cardinality at least 2,
we can find at least two unique pairs.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
UniqueSums
is preserved under additive equivalences.
UniqueProd
is preserved under multiplicative equivalences.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Two theorems in Andrzej Strojnowski, A note on u.p. groups
UniqueProds G
says that for any two nonempty Finset
s A
and B
in G
, A × B
contains a unique pair with the UniqueMul
property. Strojnowski showed that if G
is
a group, then we only need to check this when A = B
.
Here we generalize the result to cancellative semigroups.
Non-cancellative counterexample: the AddMonoid {0,1} with 1+1=1.
If a group has UniqueProds
, then it actually has TwoUniqueProds
.
For an example of a semigroup G
embeddable into a group that has UniqueProds
but not TwoUniqueProds
, see Example 10.13 in
J. Okniński, Semigroup Algebras.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
TwoUniqueSums
is preserved under additive equivalences.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
This instance asserts that if G
has a right-cancellative addition, a linear order,
and addition is strictly monotone w.r.t. the second argument, then G
has TwoUniqueSums
.
Equations
- ⋯ = ⋯
This instance asserts that if G
has a right-cancellative multiplication, a linear order, and
multiplication is strictly monotone w.r.t. the second argument, then G
has TwoUniqueProds
.
Equations
- ⋯ = ⋯
This instance asserts that if G
has a left-cancellative addition, a linear order, and
addition is strictly monotone w.r.t. the first argument, then G
has TwoUniqueSums
.
Equations
- ⋯ = ⋯
This instance asserts that if G
has a left-cancellative multiplication, a linear order, and
multiplication is strictly monotone w.r.t. the first argument, then G
has TwoUniqueProds
.
Equations
- ⋯ = ⋯
Alias of UniqueProds.of_injective_mulHom
.
Alias of UniqueSums.of_injective_addHom
.
Alias of MulEquiv.uniqueProds_iff
.
UniqueProd
is preserved under multiplicative equivalences.
Alias of AddEquiv.uniqueSums_iff
.
UniqueSums
is preserved under additive equivalences.
Alias of TwoUniqueProds.of_injective_mulHom
.
Alias of TwoUniqueSums.of_injective_addHom
.
Alias of MulEquiv.twoUniqueProds_iff
.
TwoUniqueProd
is preserved under multiplicative equivalences.
Alias of AddEquiv.twoUniqueSums_iff
.
TwoUniqueSums
is preserved under additive equivalences.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Any FreeMonoid
has the TwoUniqueProds
property.
Equations
- ⋯ = ⋯
Any FreeAddMonoid
has the TwoUniqueSums
property.
Equations
- ⋯ = ⋯