mathlib3 documentation

algebra.group.unique_prods

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

unique_mul A B a0 b0 = ∀ ⦃a b : G⦄, a ∈ A → b ∈ B → a * b = a0 * b0 → a = a0 ∧ b = b0

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

unique_add A B a0 b0 = ∀ ⦃a b : G⦄, a ∈ A → b ∈ B → a + b = a0 + b0 → a = a0 ∧ b = b0

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

unique_add_of_nonempty : ∀ {A B : finset G}, A.nonempty → B.nonempty → (∃ (a0 : G) (H : a0 ∈ A) (b0 : G) (H : b0 ∈ B), unique_add A B a0 b0)

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

unique_mul_of_nonempty : ∀ {A B : finset G}, A.nonempty → B.nonempty → (∃ (a0 : G) (H : a0 ∈ A) (b0 : G) (H : b0 ∈ B), unique_mul A B a0 b0)

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]

def multiplicative.unique_prods {M : Type u_1} [has_add M] [unique_sums M] :

unique_prods (multiplicative M)

@[protected, instance]

def additive.unique_sums {M : Type u_1} [has_mul M] [unique_prods M] :

unique_sums (additive M)

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]

def covariants.to_unique_prods {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] :

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]

def covariants.to_unique_sums {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] :

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