Documentation

Mathlib.Combinatorics.Additive.Dissociation

Dissociation and span #

This file defines dissociation and span of sets in groups. These are analogs to the usual linear independence and linear span of sets in a vector space but where the scalars are only allowed to be 0 or ±1. In characteristic 2 or 3, the two pairs of concepts are actually equivalent.

Main declarations #

def AddDissociated {α : Type u_1} [AddCommGroup α] (s : Set α) :

A set is dissociated iff all its finite subsets have different sums.

This is an analog of linear independence in a vector space, but with the "scalars" restricted to 0 and ±1.

Equations
def MulDissociated {α : Type u_1} [CommGroup α] (s : Set α) :

A set is dissociated iff all its finite subsets have different products.

This is an analog of linear independence in a vector space, but with the "scalars" restricted to 0 and ±1.

Equations
theorem addDissociated_iff_sum_eq_subsingleton {α : Type u_1} [AddCommGroup α] {s : Set α} :
AddDissociated s ∀ (a : α), {t : Finset α | t s xt, x = a}.Subsingleton
theorem mulDissociated_iff_sum_eq_subsingleton {α : Type u_1} [CommGroup α] {s : Set α} :
MulDissociated s ∀ (a : α), {t : Finset α | t s xt, x = a}.Subsingleton
theorem AddDissociated.subset {α : Type u_1} [AddCommGroup α] {s : Set α} {t : Set α} (hst : s t) (ht : AddDissociated t) :
theorem MulDissociated.subset {α : Type u_1} [CommGroup α] {s : Set α} {t : Set α} (hst : s t) (ht : MulDissociated t) :
@[simp]
theorem addDissociated_singleton {α : Type u_1} [AddCommGroup α] {a : α} :
@[simp]
theorem mulDissociated_singleton {α : Type u_1} [CommGroup α] {a : α} :
@[simp]
theorem not_addDissociated {α : Type u_1} [AddCommGroup α] {s : Set α} :
¬AddDissociated s ∃ (t : Finset α), t s ∃ (u : Finset α), u s t u xt, x = xu, x
@[simp]
theorem not_mulDissociated {α : Type u_1} [CommGroup α] {s : Set α} :
¬MulDissociated s ∃ (t : Finset α), t s ∃ (u : Finset α), u s t u xt, x = xu, x
theorem not_addDissociated_iff_exists_disjoint {α : Type u_1} [AddCommGroup α] {s : Set α} :
¬AddDissociated s ∃ (t : Finset α) (u : Finset α), t s u s Disjoint t u t u at, a = au, a
theorem not_mulDissociated_iff_exists_disjoint {α : Type u_1} [CommGroup α] {s : Set α} :
¬MulDissociated s ∃ (t : Finset α) (u : Finset α), t s u s Disjoint t u t u at, a = au, a
@[simp]
theorem AddEquiv.addDissociated_preimage {α : Type u_1} {β : Type u_2} [AddCommGroup α] [AddCommGroup β] {s : Set α} (e : β ≃+ α) :
@[simp]
theorem MulEquiv.mulDissociated_preimage {α : Type u_1} {β : Type u_2} [CommGroup α] [CommGroup β] {s : Set α} (e : β ≃* α) :
@[simp]
theorem addDissociated_neg {α : Type u_1} [AddCommGroup α] {s : Set α} :
@[simp]
theorem MulDissociated.inv {α : Type u_1} [CommGroup α] {s : Set α} :

Alias of the reverse direction of mulDissociated_inv.

theorem MulDissociated.of_inv {α : Type u_1} [CommGroup α] {s : Set α} :

Alias of the forward direction of mulDissociated_inv.

theorem AddDissociated.neg {α : Type u_1} [AddCommGroup α] {s : Set α} :
def Finset.addSpan {α : Type u_1} [AddCommGroup α] [DecidableEq α] [Fintype α] (s : Finset α) :

The span of a finset s is the finset of elements of the form ∑ a in s, ε a • a where ε ∈ {-1, 0, 1} ^ s.

This is an analog of the linear span in a vector space, but with the "scalars" restricted to 0 and ±1.

Equations
def Finset.mulSpan {α : Type u_1} [CommGroup α] [DecidableEq α] [Fintype α] (s : Finset α) :

The span of a finset s is the finset of elements of the form ∏ a in s, a ^ ε a where ε ∈ {-1, 0, 1} ^ s.

This is an analog of the linear span in a vector space, but with the "scalars" restricted to 0 and ±1.

Equations
@[simp]
theorem Finset.mem_addSpan {α : Type u_1} [AddCommGroup α] [DecidableEq α] [Fintype α] {s : Finset α} {a : α} :
a s.addSpan ∃ (ε : α), (∀ (a : α), ε a = -1 ε a = 0 ε a = 1) as, ε a a = a
@[simp]
theorem Finset.mem_mulSpan {α : Type u_1} [CommGroup α] [DecidableEq α] [Fintype α] {s : Finset α} {a : α} :
a s.mulSpan ∃ (ε : α), (∀ (a : α), ε a = -1 ε a = 0 ε a = 1) as, a ^ ε a = a
@[simp]
theorem Finset.subset_addSpan {α : Type u_1} [AddCommGroup α] [DecidableEq α] [Fintype α] {s : Finset α} :
s s.addSpan
@[simp]
theorem Finset.subset_mulSpan {α : Type u_1} [CommGroup α] [DecidableEq α] [Fintype α] {s : Finset α} :
s s.mulSpan
theorem Finset.sum_sub_sum_mem_addSpan {α : Type u_1} [AddCommGroup α] [DecidableEq α] [Fintype α] {s : Finset α} {t : Finset α} {u : Finset α} (ht : t s) (hu : u s) :
at, a - au, a s.addSpan
theorem Finset.prod_div_prod_mem_mulSpan {α : Type u_1} [CommGroup α] [DecidableEq α] [Fintype α] {s : Finset α} {t : Finset α} {u : Finset α} (ht : t s) (hu : u s) :
(∏ at, a) / au, a s.mulSpan
theorem Finset.exists_subset_addSpan_card_le_of_forall_addDissociated {α : Type u_1} [AddCommGroup α] [DecidableEq α] [Fintype α] {s : Finset α} {d : } (hs : s's, AddDissociated s's'.card d) :
s's, s'.card d s s'.addSpan

If every dissociated subset of s has size at most d, then s is actually generated by a subset of size at most d.

This is a dissociation analog of the fact that a set whose linearly independent subspaces all have size at most d is of dimension at most d itself.

theorem Finset.exists_subset_mulSpan_card_le_of_forall_mulDissociated {α : Type u_1} [CommGroup α] [DecidableEq α] [Fintype α] {s : Finset α} {d : } (hs : s's, MulDissociated s's'.card d) :
s's, s'.card d s s'.mulSpan

If every dissociated subset of s has size at most d, then s is actually generated by a subset of size at most d.

This is a dissociation analog of the fact that a set whose linearly independent subsets all have size at most d is of dimension at most d itself.