mathlib3 documentation

algebra.group.unique_prods

Unique products and related notions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 unique_prods. Since the condition requires no property of the group operation, we define it for a Type simply satisfying has_mul. We also introduce the analogous "additive" companion, unique_sums and link the two so that to_additive converts unique_prods into unique_sums.

Here you can see several examples of Types that have unique_sums/prods (apply_instance uses covariants.to_unique_prods and covariants.to_unique_sums).

import data.real.basic

example : unique_sums    := by apply_instance
example : unique_sums +  := by apply_instance
example : unique_sums    := by apply_instance
example : unique_sums    := by apply_instance
example : unique_sums    := by apply_instance
example : unique_prods + := by apply_instance
```
def unique_mul {G : Type u_1} [has_mul G] (A B : finset G) (a0 b0 : G) :
Prop

Let G be a Type with multiplication, let A B : finset G be finite subsets and let a0 b0 : G be two elements. unique_mul A B a0 b0 asserts a0 * b0 can be written in at most one way as a product of an element of A and an element of B.

Equations
def unique_add {G : Type u_1} [has_add G] (A B : finset G) (a0 b0 : G) :
Prop

Let G be a Type with addition, let A B : finset G be finite subsets and let a0 b0 : G be two elements. unique_add A B a0 b0 asserts a0 + b0 can be written in at most one way as a sum of an element from A and an element from B.

Equations
theorem unique_mul.mt {G : Type u_1} [has_mul G] {A B : finset G} {a0 b0 : G} (h : unique_mul A B a0 b0) ⦃a b : G⦄ :
a A b B a a0 b b0 a * b a0 * b0
theorem unique_add.subsingleton {G : Type u_1} [has_add G] (A B : finset G) (a0 b0 : G) (h : unique_add A B a0 b0) :
subsingleton {ab // ab.fst A ab.snd B ab.fst + ab.snd = a0 + b0}
theorem unique_mul.subsingleton {G : Type u_1} [has_mul G] (A B : finset G) (a0 b0 : G) (h : unique_mul A B a0 b0) :
subsingleton {ab // ab.fst A ab.snd B ab.fst * ab.snd = a0 * b0}
theorem unique_add.set_subsingleton {G : Type u_1} [has_add G] (A B : finset G) (a0 b0 : G) (h : unique_add A B a0 b0) :
{ab : G × G | ab.fst A ab.snd B ab.fst + ab.snd = a0 + b0}.subsingleton
theorem unique_mul.set_subsingleton {G : Type u_1} [has_mul G] (A B : finset G) (a0 b0 : G) (h : unique_mul A B a0 b0) :
{ab : G × G | ab.fst A ab.snd B ab.fst * ab.snd = a0 * b0}.subsingleton
theorem unique_add.iff_exists_unique {G : Type u_1} [has_add G] {A B : finset G} {a0 b0 : G} (aA : a0 A) (bB : b0 B) :
unique_add A B a0 b0 ∃! (ab : G × G) (H : ab A ×ˢ B), ab.fst + ab.snd = a0 + b0
theorem unique_mul.iff_exists_unique {G : Type u_1} [has_mul G] {A B : finset G} {a0 b0 : G} (aA : a0 A) (bB : b0 B) :
unique_mul A B a0 b0 ∃! (ab : G × G) (H : ab A ×ˢ B), ab.fst * ab.snd = a0 * b0
theorem unique_add.exists_iff_exists_exists_unique {G : Type u_1} [has_add G] {A B : finset G} :
( (a0 b0 : G), a0 A b0 B unique_add A B a0 b0) (g : G), ∃! (ab : G × G) (H : ab A ×ˢ B), ab.fst + ab.snd = g
theorem unique_mul.exists_iff_exists_exists_unique {G : Type u_1} [has_mul G] {A B : finset G} :
( (a0 b0 : G), a0 A b0 B unique_mul A B a0 b0) (g : G), ∃! (ab : G × G) (H : ab A ×ˢ B), ab.fst * ab.snd = g
theorem unique_mul.mul_hom_preimage {G : Type u_1} {H : Type u_2} [has_mul G] [has_mul H] (f : G →ₙ* H) (hf : function.injective f) (a0 b0 : G) {A B : finset H} (u : unique_mul A B (f a0) (f b0)) :
unique_mul (A.preimage f _) (B.preimage f _) a0 b0

unique_mul is preserved by inverse images under injective, multiplicative maps.

theorem unique_add.add_hom_preimage {G : Type u_1} {H : Type u_2} [has_add G] [has_add H] (f : add_hom G H) (hf : function.injective f) (a0 b0 : G) {A B : finset H} (u : unique_add A B (f a0) (f b0)) :
unique_add (A.preimage f _) (B.preimage f _) a0 b0

unique_add is preserved by inverse images under injective, additive maps.

theorem unique_mul.mul_hom_image_iff {G : Type u_1} {H : Type u_2} [has_mul G] [has_mul H] {A B : finset G} {a0 b0 : G} [decidable_eq H] (f : G →ₙ* H) (hf : function.injective f) :
unique_mul (finset.image f A) (finset.image f B) (f a0) (f b0) unique_mul A B a0 b0

unique_mul is preserved under multiplicative maps that are injective.

See unique_mul.mul_hom_map_iff for a version with swapped bundling.

theorem unique_add.add_hom_image_iff {G : Type u_1} {H : Type u_2} [has_add G] [has_add H] {A B : finset G} {a0 b0 : G} [decidable_eq H] (f : add_hom G H) (hf : function.injective f) :
unique_add (finset.image f A) (finset.image f B) (f a0) (f b0) unique_add A B a0 b0

unique_add is preserved under additive maps that are injective.

See unique_add.add_hom_map_iff for a version with swapped bundling.

theorem unique_mul.mul_hom_map_iff {G : Type u_1} {H : Type u_2} [has_mul G] [has_mul H] {A B : finset G} {a0 b0 : G} (f : G H) (mul : (x y : G), f (x * y) = f x * f y) :
unique_mul (finset.map f A) (finset.map f B) (f a0) (f b0) unique_mul A B a0 b0

unique_mul is preserved under embeddings that are multiplicative.

See unique_mul.mul_hom_image_iff for a version with swapped bundling.

theorem unique_add.add_hom_map_iff {G : Type u_1} {H : Type u_2} [has_add G] [has_add H] {A B : finset G} {a0 b0 : G} (f : G H) (mul : (x y : G), f (x + y) = f x + f y) :
unique_add (finset.map f A) (finset.map f B) (f a0) (f b0) unique_add A B a0 b0

unique_add is preserved under embeddings that are additive.

See unique_add.add_hom_image_iff for a version with swapped bundling.

@[class]
structure unique_sums (G : Type u_1) [has_add G] :
Prop

Let G be a Type with addition. unique_sums G asserts that any two non-empty finite subsets of A have the unique_add property, with respect to some element of their sum A + B.

Instances of this typeclass
@[class]
structure unique_prods (G : Type u_1) [has_mul G] :
Prop

Let G be a Type with multiplication. unique_prods G asserts that any two non-empty finite subsets of G have the unique_mul property, with respect to some element of their product A * B.

Instances of this typeclass
@[protected, instance]
@[protected, instance]
theorem eq_and_eq_of_le_of_le_of_mul_le {A : Type u_1} [has_mul A] [linear_order A] [covariant_class A A has_mul.mul has_le.le] [covariant_class A A (function.swap has_mul.mul) has_lt.lt] [contravariant_class A A has_mul.mul has_le.le] {a b a0 b0 : A} (ha : a0 a) (hb : b0 b) (ab : a * b a0 * b0) :
a = a0 b = b0
theorem eq_and_eq_of_le_of_le_of_add_le {A : Type u_1} [has_add A] [linear_order A] [covariant_class A A has_add.add has_le.le] [covariant_class A A (function.swap has_add.add) has_lt.lt] [contravariant_class A A has_add.add has_le.le] {a b a0 b0 : A} (ha : a0 a) (hb : b0 b) (ab : a + b a0 + b0) :
a = a0 b = b0
@[protected, instance]

This instance asserts that if A has a multiplication, a linear order, and multiplication is 'very monotone', then A also has unique_prods.

@[protected, instance]

This instance asserts that if A has an addition, a linear order, and addition is 'very monotone', then A also has unique_sums.