Documentation

Mathlib.Algebra.Group.UniqueProds

A group G has unique products if for any two non-empty finite subsets A, B ⊂ G⊂ G, there is an element g ∈ A * B∈ 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.

Here you can see several examples of Types that have UniqueSums/Prods (infer_instance uses covariants.to_uniqueProds and covariants.to_uniqueSums).

import Mathlib.Data.Real.Basic
import Mathlib.Data.PNat.Basic
import Mathlib.Algebra.Group.UniqueProds

example : UniqueSums ℕ   := by infer_instance
example : UniqueSums ℕ+  := by infer_instance
example : UniqueSums ℤ   := by infer_instance
example : UniqueSums ℚ   := by infer_instance
example : UniqueSums ℝ   := by infer_instance
example : UniqueProds ℕ+ := by infer_instance

def UniqueAdd {G : Type u_1} [inst : Add G] (A : Finset G) (B : Finset G) (a0 : G) (b0 : G) :

Let G be a Type with addition, let A B : Finset G be finite subsets and let a0 b0 : G be two elements. UniqueAdd 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

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

def UniqueMul {G : Type u_1} [inst : Mul G] (A : Finset G) (B : Finset G) (a0 : G) (b0 : G) :

Let G be a Type with multiplication, let A B : Finset G be finite subsets and let a0 b0 : G be two elements. UniqueMul 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

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

theorem UniqueMul.mt {G : Type u_1} [inst : Mul G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (h : UniqueMul A B a0 b0) ⦃a : G⦄ ⦃b : G⦄ :

a ∈ A → b ∈ B → a ≠ a0 ∨ b ≠ b0 → a * b ≠ a0 * b0

theorem UniqueAdd.subsingleton {G : Type u_1} [inst : Add G] (A : Finset G) (B : Finset G) (a0 : G) (b0 : G) (h : UniqueAdd A B a0 b0) :

Subsingleton { ab // ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst + ab.snd = a0 + b0 }

abbrev UniqueAdd.subsingleton.match_1 {G : Type u_1} [inst : Add G] (A : Finset G) (B : Finset G) (a0 : G) (b0 : G) (motive : { ab // ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst + ab.snd = a0 + b0 } → Prop) :

(x : { ab // ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst + ab.snd = a0 + b0 }) → ((_a' _b' : G) → (ha' : (_a', _b').fst ∈ A) → (hb' : (_a', _b').snd ∈ B) → (ab' : (_a', _b').fst + (_a', _b').snd = a0 + b0) → motive { val := (_a', _b'), property := (_ : (_a', _b').fst ∈ A ∧ (_a', _b').snd ∈ B ∧ (_a', _b').fst + (_a', _b').snd = a0 + b0) }) → motive x

Equations

One or more equations did not get rendered due to their size.

theorem UniqueMul.subsingleton {G : Type u_1} [inst : Mul G] (A : Finset G) (B : Finset G) (a0 : G) (b0 : G) (h : UniqueMul A B a0 b0) :

Subsingleton { ab // ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst * ab.snd = a0 * b0 }

theorem UniqueAdd.set_subsingleton {G : Type u_1} [inst : Add G] (A : Finset G) (B : Finset G) (a0 : G) (b0 : G) (h : UniqueAdd A B a0 b0) :

Set.Subsingleton { ab | ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst + ab.snd = a0 + b0 }

theorem UniqueMul.set_subsingleton {G : Type u_1} [inst : Mul G] (A : Finset G) (B : Finset G) (a0 : G) (b0 : G) (h : UniqueMul A B a0 b0) :

Set.Subsingleton { ab | ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst * ab.snd = a0 * b0 }

theorem UniqueAdd.iff_existsUnique {G : Type u_1} [inst : Add G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (aA : a0 ∈ A) (bB : b0 ∈ B) :

UniqueAdd A B a0 b0 ↔ ∃! ab x, ab.fst + ab.snd = a0 + b0

theorem UniqueMul.iff_existsUnique {G : Type u_1} [inst : Mul G] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (aA : a0 ∈ A) (bB : b0 ∈ B) :

UniqueMul A B a0 b0 ↔ ∃! ab x, ab.fst * ab.snd = a0 * b0

abbrev UniqueAdd.exists_iff_exists_existsUnique.match_1 {G : Type u_1} [inst : Add G] {A : Finset G} {B : Finset G} (motive : (∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueAdd A B a0 b0) → Prop) :

(x : ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueAdd A B a0 b0) → ((a0 b0 : G) → (hA : a0 ∈ A) → (hB : b0 ∈ B) → (h : UniqueAdd A B a0 b0) → motive (_ : ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueAdd A B a0 b0)) → motive x

Equations

One or more equations did not get rendered due to their size.

abbrev UniqueAdd.exists_iff_exists_existsUnique.match_2 {G : Type u_1} [inst : Add G] {A : Finset G} {B : Finset G} (motive : (∃ g, ∃! ab x, ab.fst + ab.snd = g) → Prop) :

(x : ∃ g, ∃! ab x, ab.fst + ab.snd = g) → ((g : G) → (h : ∃! ab x, ab.fst + ab.snd = g) → motive (_ : ∃ g, ∃! ab x, ab.fst + ab.snd = g)) → motive x

Equations

UniqueAdd.exists_iff_exists_existsUnique.match_2 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem UniqueAdd.exists_iff_exists_existsUnique {G : Type u_1} [inst : Add G] {A : Finset G} {B : Finset G} :

(∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueAdd A B a0 b0) ↔ ∃ g, ∃! ab x, ab.fst + ab.snd = g

theorem UniqueMul.exists_iff_exists_existsUnique {G : Type u_1} [inst : Mul G] {A : Finset G} {B : Finset G} :

(∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0) ↔ ∃ g, ∃! ab x, ab.fst * ab.snd = g

theorem UniqueAdd.addHom_preimage {G : Type u_1} {H : Type u_2} [inst : Add G] [inst : Add H] (f : AddHom G H) (hf : Function.Injective ↑f) (a0 : G) (b0 : G) {A : Finset H} {B : Finset H} (u : UniqueAdd A B (↑f a0) (↑f b0)) :

UniqueAdd (Finset.preimage A ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑A))) (Finset.preimage B ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑B))) a0 b0

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

theorem UniqueMul.mulHom_preimage {G : Type u_1} {H : Type u_2} [inst : Mul G] [inst : Mul H] (f : G →ₙ* H) (hf : Function.Injective ↑f) (a0 : G) (b0 : G) {A : Finset H} {B : Finset H} (u : UniqueMul A B (↑f a0) (↑f b0)) :

UniqueMul (Finset.preimage A ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑A))) (Finset.preimage B ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑B))) a0 b0

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

theorem UniqueAdd.addHom_image_iff {G : Type u_2} {H : Type u_1} [inst : Add G] [inst : Add H] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} [inst : DecidableEq H] (f : AddHom G H) (hf : Function.Injective ↑f) :

UniqueAdd (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0) ↔ UniqueAdd A B a0 b0

UniqueAdd is preserved under additive maps that are injective.

See UniqueAdd.addHom_map_iff for a version with swapped bundling.

theorem UniqueMul.mulHom_image_iff {G : Type u_2} {H : Type u_1} [inst : Mul G] [inst : Mul H] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} [inst : DecidableEq H] (f : G →ₙ* H) (hf : Function.Injective ↑f) :

UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0) ↔ UniqueMul A B a0 b0

Unique_Mul is preserved under multiplicative maps that are injective.

See UniqueMul.mulHom_map_iff for a version with swapped bundling.

theorem UniqueAdd.addHom_map_iff {G : Type u_1} {H : Type u_2} [inst : Add G] [inst : Add H] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (f : G ↪ H) (mul : ∀ (x y : G), ↑f (x + y) = ↑f x + ↑f y) :

UniqueAdd (Finset.map f A) (Finset.map f B) (↑f a0) (↑f b0) ↔ UniqueAdd A B a0 b0

UniqueAdd is preserved under embeddings that are additive.

See UniqueAdd.addHom_image_iff for a version with swapped bundling.

theorem UniqueMul.mulHom_map_iff {G : Type u_1} {H : Type u_2} [inst : Mul G] [inst : Mul H] {A : Finset G} {B : Finset G} {a0 : G} {b0 : G} (f : G ↪ H) (mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y) :

UniqueMul (Finset.map f A) (Finset.map f B) (↑f a0) (↑f b0) ↔ UniqueMul A B a0 b0

UniqueMul is preserved under embeddings that are multiplicative.

See UniqueMul.mulHom_image_iff for a version with swapped bundling.

class UniqueSums (G : Type u_1) [inst : Add G] :

For A B two nonempty finite sets, there always exist a0 ∈ A, b0 ∈ B∈ A, b0 ∈ B∈ B such that UniqueAdd A B a0 b0
uniqueAdd_of_nonempty : ∀ {A B : Finset G}, Finset.Nonempty A → Finset.Nonempty B → ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueAdd A B a0 b0

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

Instances

class UniqueProds (G : Type u_1) [inst : Mul G] :

For A B two nonempty finite sets, there always exist a0 ∈ A, b0 ∈ B∈ A, b0 ∈ B∈ B such that UniqueMul A B a0 b0
uniqueMul_of_nonempty : ∀ {A B : Finset G}, Finset.Nonempty A → Finset.Nonempty B → ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueMul 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.

Instances

instance Multiplicative.instUniqueProdsMultiplicativeMul {M : Type u_1} [inst : Add M] [inst : UniqueSums M] :

UniqueProds (Multiplicative M)

Equations

@Multiplicative.instUniqueProdsMultiplicativeMul = @Multiplicative.instUniqueProdsMultiplicativeMul.proof_1

instance Additive.instUniqueSumsAdditiveAdd {M : Type u_1} [inst : Mul M] [inst : UniqueProds M] :

UniqueSums (Additive M)

Equations

@Additive.instUniqueSumsAdditiveAdd = @Additive.instUniqueSumsAdditiveAdd.proof_1

theorem eq_and_eq_of_le_of_le_of_add_le {A : Type u_1} [inst : Add A] [inst : LinearOrder A] [inst : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : A} {b : A} {a0 : A} {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_mul_le {A : Type u_1} [inst : Mul A] [inst : LinearOrder A] [inst : CovariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ContravariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : A} {b : A} {a0 : A} {b0 : A} (ha : a0 ≤ a) (hb : b0 ≤ b) (ab : a * b ≤ a0 * b0) :

a = a0 ∧ b = b0

instance Covariants.to_uniqueSums {A : Type u_1} [inst : Add A] [inst : LinearOrder A] [inst : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

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

Equations

@Covariants.to_uniqueSums = @Covariants.to_uniqueSums.proof_1

def Covariants.to_uniqueSums.proof_1 {A : Type u_1} [inst : Add A] [inst : LinearOrder A] [inst : CovariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass A A (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

Equations

(_ : UniqueSums A) = (_ : UniqueSums A)

instance Covariants.to_uniqueProds {A : Type u_1} [inst : Mul A] [inst : LinearOrder A] [inst : CovariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ContravariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] :

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

Equations

@Covariants.to_uniqueProds = @Covariants.to_uniqueProds.proof_1