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

• MulDissociated/AddDissociated: Predicate for a set to be dissociated.
• Finset.mulSpan/Finset.addSpan: Span of a finset.

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

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

• AddDissociated s = Set.InjOn (fun (x : Finset α) => ∑ x ∈ x, x) {t : Finset α | ↑t ⊆ s}

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

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

• MulDissociated s = Set.InjOn (fun (x : Finset α) => ∏ x ∈ x, x) {t : Finset α | ↑t ⊆ s}

theorem addDissociated_iff_sum_eq_subsingleton {α : Type u_1} [AddCommGroup α] {s : Set α} : AddDissociated s ↔ ∀ (a : α), {t : Finset α | ↑t ⊆ s ∧ ∑ x ∈ t, x = a}.Subsingleton

theorem mulDissociated_iff_sum_eq_subsingleton {α : Type u_1} [CommGroup α] {s : Set α} : MulDissociated s ↔ ∀ (a : α), {t : Finset α | ↑t ⊆ s ∧ ∏ x ∈ t, x = a}.Subsingleton

theorem AddDissociated.subset {α : Type u_1} [AddCommGroup α] {s : Set α} {t : Set α} (hst : s ⊆ t) (ht : AddDissociated t) : AddDissociated s

theorem MulDissociated.subset {α : Type u_1} [CommGroup α] {s : Set α} {t : Set α} (hst : s ⊆ t) (ht : MulDissociated t) : MulDissociated s

@[simp]

theorem addDissociated_empty {α : Type u_1} [AddCommGroup α] : AddDissociated ∅

@[simp]

theorem mulDissociated_empty {α : Type u_1} [CommGroup α] : MulDissociated ∅

@[simp]

theorem addDissociated_singleton {α : Type u_1} [AddCommGroup α] {a : α} : AddDissociated {a} ↔ a ≠ 0

@[simp]

theorem mulDissociated_singleton {α : Type u_1} [CommGroup α] {a : α} : MulDissociated {a} ↔ a ≠ 1

@[simp]

theorem not_addDissociated {α : Type u_1} [AddCommGroup α] {s : Set α} : ¬AddDissociated s ↔ ∃ (t : Finset α), ↑t ⊆ s ∧ ∃ (u : Finset α), ↑u ⊆ s ∧ t ≠ u ∧ ∑ x ∈ t, x = ∑ x ∈ u, x

@[simp]

theorem not_mulDissociated {α : Type u_1} [CommGroup α] {s : Set α} : ¬MulDissociated s ↔ ∃ (t : Finset α), ↑t ⊆ s ∧ ∃ (u : Finset α), ↑u ⊆ s ∧ t ≠ u ∧ ∏ x ∈ t, x = ∏ x ∈ u, x

abbrev not_addDissociated_iff_exists_disjoint.match_1 {α : Type u_1} [AddCommGroup α] {s : Set α} (motive : (∃ (t : Finset α) (u : Finset α), ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∑ a ∈ t, a = ∑ a ∈ u, a) → Prop) : ∀ (x : ∃ (t : Finset α) (u : Finset α), ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∑ a ∈ t, a = ∑ a ∈ u, a), (∀ (t u : Finset α) (ht : ↑t ⊆ s) (hu : ↑u ⊆ s) (left : Disjoint t u) (htune : t ≠ u) (htusum : ∑ a ∈ t, a = ∑ a ∈ u, a), motive ⋯) → motive x

Equations

• ⋯ = ⋯

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 ∧ ∑ a ∈ t, a = ∑ a ∈ u, 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 ∧ ∏ a ∈ t, a = ∏ a ∈ u, a

@[simp]

theorem AddEquiv.addDissociated_preimage {α : Type u_1} {β : Type u_2} [AddCommGroup α] [AddCommGroup β] {s : Set α} (e : β ≃+ α) : AddDissociated (⇑e ⁻¹' s) ↔ AddDissociated s

@[simp]

theorem MulEquiv.mulDissociated_preimage {α : Type u_1} {β : Type u_2} [CommGroup α] [CommGroup β] {s : Set α} (e : β ≃* α) : MulDissociated (⇑e ⁻¹' s) ↔ MulDissociated s

@[simp]

theorem addDissociated_neg {α : Type u_1} [AddCommGroup α] {s : Set α} : AddDissociated (-s) ↔ AddDissociated s

@[simp]

theorem mulDissociated_inv {α : Type u_1} [CommGroup α] {s : Set α} : MulDissociated s⁻¹ ↔ MulDissociated s

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

Alias of the forward direction of mulDissociated_inv.

theorem MulDissociated.inv {α : Type u_1} [CommGroup α] {s : Set α} : MulDissociated s → MulDissociated s⁻¹

Alias of the reverse direction of mulDissociated_inv.

theorem AddDissociated.of_neg {α : Type u_1} [AddCommGroup α] {s : Set α} : AddDissociated (-s) → AddDissociated s

theorem AddDissociated.neg {α : Type u_1} [AddCommGroup α] {s : Set α} : AddDissociated s → AddDissociated (-s)

def Finset.addSpan {α : Type u_1} [AddCommGroup α] [DecidableEq α] [Fintype α] (s : Finset α) : 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

• s.addSpan = Finset.image (fun (ε : α → ℤ) => ∑ a ∈ s, ε a • a) (Fintype.piFinset fun (_a : α) => {-1, 0, 1})

def Finset.mulSpan {α : Type u_1} [CommGroup α] [DecidableEq α] [Fintype α] (s : Finset α) : 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

• s.mulSpan = Finset.image (fun (ε : α → ℤ) => ∏ a ∈ s, a ^ ε a) (Fintype.piFinset fun (_a : α) => {-1, 0, 1})

@[simp]

theorem Finset.mem_addSpan {α : Type u_1} [AddCommGroup α] [DecidableEq α] [Fintype α] {s : Finset α} {a : α} : a ∈ s.addSpan ↔ ∃ (ε : α → ℤ), (∀ (a : α), ε a = -1 ∨ ε a = 0 ∨ ε a = 1) ∧ ∑ a ∈ s, ε 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) ∧ ∏ a ∈ s, 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) : ∑ a ∈ t, a - ∑ a ∈ u, 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) : (∏ a ∈ t, a) / ∏ a ∈ u, 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.