Documentation

Mathlib.Order.SupIndep

Supremum independence #

In this file, we define supremum independence of indexed sets. An indexed family f : ι → α is sup-independent if, for all a, f a and the supremum of the rest are disjoint.

Main definitions #

Finset.SupIndep s f: a family of elements f are supremum independent on the finite set s.
CompleteLattice.SetIndependent s: a set of elements are supremum independent.
CompleteLattice.Independent f: a family of elements are supremum independent.

Main statements #

In a distributive lattice, supremum independence is equivalent to pairwise disjointness:
Otherwise, supremum independence is stronger than pairwise disjointness:

Implementation notes #

For the finite version, we avoid the "obvious" definition ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f) because erase would require decidable equality on ι.

On lattices with a bottom element, via `Finset.sup` #

def Finset.SupIndep {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] (s : Finset ι) (f : ι → α) :

Supremum independence of finite sets. We avoid the "obvious" definition using s.erase i because erase would require decidable equality on ι.

Equations

Finset.SupIndep s f = ∀ ⦃t : Finset ι⦄, t ⊆ s → ∀ ⦃i : ι⦄, i ∈ s → ¬i ∈ t → Disjoint (f i) (Finset.sup t f)

Instances For

instance Finset.instDecidableSupIndep {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ι → α} [DecidableEq ι] [DecidableEq α] :

Decidable (Finset.SupIndep s f)

Equations

Finset.instDecidableSupIndep = Finset.decidableForallOfDecidableSubsets

theorem Finset.SupIndep.subset {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {t : Finset ι} {f : ι → α} (ht : Finset.SupIndep t f) (h : s ⊆ t) :

Finset.SupIndep s f

theorem Finset.supIndep_empty {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] (f : ι → α) :

Finset.SupIndep ∅ f

theorem Finset.supIndep_singleton {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] (i : ι) (f : ι → α) :

Finset.SupIndep {i} f

theorem Finset.SupIndep.pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ι → α} (hs : Finset.SupIndep s f) :

Set.PairwiseDisjoint (↑s) f

theorem Finset.SupIndep.le_sup_iff {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {t : Finset ι} {f : ι → α} {i : ι} (hs : Finset.SupIndep s f) (hts : t ⊆ s) (hi : i ∈ s) (hf : ∀ (i : ι), f i ≠ ⊥) :

f i ≤ Finset.sup t f ↔ i ∈ t

theorem Finset.supIndep_iff_disjoint_erase {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ι → α} [DecidableEq ι] :

Finset.SupIndep s f ↔ ∀ (i : ι), i ∈ s → Disjoint (f i) (Finset.sup (Finset.erase s i) f)

The RHS looks like the definition of CompleteLattice.Independent.

theorem Finset.SupIndep.image {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [OrderBot α] {f : ι → α} [DecidableEq ι] {s : Finset ι'} {g : ι' → ι} (hs : Finset.SupIndep s (f ∘ g)) :

Finset.SupIndep (Finset.image g s) f

theorem Finset.supIndep_map {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [OrderBot α] {f : ι → α} {s : Finset ι'} {g : ι' ↪ ι} :

Finset.SupIndep (Finset.map g s) f ↔ Finset.SupIndep s (f ∘ ↑g)

@[simp]

theorem Finset.supIndep_pair {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {f : ι → α} [DecidableEq ι] {i : ι} {j : ι} (hij : i ≠ j) :

Finset.SupIndep {i, j} f ↔ Disjoint (f i) (f j)

theorem Finset.supIndep_univ_bool {α : Type u_1} [Lattice α] [OrderBot α] (f : Bool → α) :

Finset.SupIndep Finset.univ f ↔ Disjoint (f false) (f true)

@[simp]

theorem Finset.supIndep_univ_fin_two {α : Type u_1} [Lattice α] [OrderBot α] (f : Fin 2 → α) :

Finset.SupIndep Finset.univ f ↔ Disjoint (f 0) (f 1)

theorem Finset.SupIndep.attach {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ι → α} (hs : Finset.SupIndep s f) :

Finset.SupIndep (Finset.attach s) fun a => f ↑a

@[simp]

theorem Finset.supIndep_attach {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ι → α} :

(Finset.SupIndep (Finset.attach s) fun a => f ↑a) ↔ Finset.SupIndep s f

theorem Finset.supIndep_iff_pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ι → α} :

Finset.SupIndep s f ↔ Set.PairwiseDisjoint (↑s) f

theorem Finset.sup_indep.pairwise_disjoint {α : Type u_1} {ι : Type u_3} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ι → α} :

Finset.SupIndep s f → Set.PairwiseDisjoint (↑s) f

Alias of the forward direction of Finset.supIndep_iff_pairwiseDisjoint.

theorem Set.PairwiseDisjoint.supIndep {α : Type u_1} {ι : Type u_3} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ι → α} :

Set.PairwiseDisjoint (↑s) f → Finset.SupIndep s f

Alias of the reverse direction of Finset.supIndep_iff_pairwiseDisjoint.

theorem Finset.SupIndep.sup {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [DistribLattice α] [OrderBot α] [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α} (hs : Finset.SupIndep s fun i => Finset.sup (g i) f) (hg : ∀ (i' : ι'), i' ∈ s → Finset.SupIndep (g i') f) :

Finset.SupIndep (Finset.sup s g) f

Bind operation for SupIndep.

theorem Finset.SupIndep.biUnion {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [DistribLattice α] [OrderBot α] [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α} (hs : Finset.SupIndep s fun i => Finset.sup (g i) f) (hg : ∀ (i' : ι'), i' ∈ s → Finset.SupIndep (g i') f) :

Finset.SupIndep (Finset.biUnion s g) f

Bind operation for SupIndep.

theorem Finset.SupIndep.sigma {α : Type u_1} {ι : Type u_3} [DistribLattice α] [OrderBot α] {β : ι → Type u_5} {s : Finset ι} {g : (i : ι) → Finset (β i)} {f : Sigma β → α} (hs : Finset.SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }) (hg : ∀ (i : ι), i ∈ s → Finset.SupIndep (g i) fun b => f { fst := i, snd := b }) :

Finset.SupIndep (Finset.sigma s g) f

Bind operation for SupIndep.

theorem Finset.SupIndep.product {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [DistribLattice α] [OrderBot α] {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α} (hs : Finset.SupIndep s fun i => Finset.sup t fun i' => f (i, i')) (ht : Finset.SupIndep t fun i' => Finset.sup s fun i => f (i, i')) :

Finset.SupIndep (s ×ˢ t) f

theorem Finset.supIndep_product_iff {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [DistribLattice α] [OrderBot α] {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α} :

Finset.SupIndep (Finset.product s t) f ↔ (Finset.SupIndep s fun i => Finset.sup t fun i' => f (i, i')) ∧ Finset.SupIndep t fun i' => Finset.sup s fun i => f (i, i')

On complete lattices via `sSup` #

def CompleteLattice.SetIndependent {α : Type u_1} [CompleteLattice α] (s : Set α) :

An independent set of elements in a complete lattice is one in which every element is disjoint from the Sup of the rest.

Equations

CompleteLattice.SetIndependent s = ∀ ⦃a : α⦄, a ∈ s → Disjoint a (sSup (s \ {a}))

Instances For

@[simp]

theorem CompleteLattice.setIndependent_empty {α : Type u_1} [CompleteLattice α] :

CompleteLattice.SetIndependent ∅

theorem CompleteLattice.SetIndependent.mono {α : Type u_1} [CompleteLattice α] {s : Set α} (hs : CompleteLattice.SetIndependent s) {t : Set α} (hst : t ⊆ s) :

CompleteLattice.SetIndependent t

theorem CompleteLattice.SetIndependent.pairwiseDisjoint {α : Type u_1} [CompleteLattice α] {s : Set α} (hs : CompleteLattice.SetIndependent s) :

Set.PairwiseDisjoint s id

If the elements of a set are independent, then any pair within that set is disjoint.

theorem CompleteLattice.setIndependent_pair {α : Type u_1} [CompleteLattice α] {a : α} {b : α} (hab : a ≠ b) :

CompleteLattice.SetIndependent {a, b} ↔ Disjoint a b

theorem CompleteLattice.SetIndependent.disjoint_sSup {α : Type u_1} [CompleteLattice α] {s : Set α} (hs : CompleteLattice.SetIndependent s) {x : α} {y : Set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : ¬x ∈ y) :

Disjoint x (sSup y)

If the elements of a set are independent, then any element is disjoint from the sSup of some subset of the rest.

def CompleteLattice.Independent {ι : Sort u_5} {α : Type u_6} [CompleteLattice α] (t : ι → α) :

An independent indexed family of elements in a complete lattice is one in which every element is disjoint from the iSup of the rest.

Example: an indexed family of non-zero elements in a vector space is linearly independent iff the indexed family of subspaces they generate is independent in this sense.

Example: an indexed family of submodules of a module is independent in this sense if and only the natural map from the direct sum of the submodules to the module is injective.

Equations

CompleteLattice.Independent t = ∀ (i : ι), Disjoint (t i) (⨆ (j : ι) (_ : j ≠ i), t j)

Instances For

theorem CompleteLattice.setIndependent_iff {α : Type u_5} [CompleteLattice α] (s : Set α) :

CompleteLattice.SetIndependent s ↔ CompleteLattice.Independent Subtype.val

theorem CompleteLattice.independent_def {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} :

CompleteLattice.Independent t ↔ ∀ (i : ι), Disjoint (t i) (⨆ (j : ι) (_ : j ≠ i), t j)

theorem CompleteLattice.independent_def' {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} :

CompleteLattice.Independent t ↔ ∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))

theorem CompleteLattice.independent_def'' {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} :

CompleteLattice.Independent t ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j x, t j = a})

@[simp]

theorem CompleteLattice.independent_empty {α : Type u_1} [CompleteLattice α] (t : Empty → α) :

CompleteLattice.Independent t

@[simp]

theorem CompleteLattice.independent_pempty {α : Type u_1} [CompleteLattice α] (t : PEmpty.{u_5} → α) :

CompleteLattice.Independent t

theorem CompleteLattice.Independent.pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} (ht : CompleteLattice.Independent t) :

Pairwise (Disjoint on t)

If the elements of a set are independent, then any pair within that set is disjoint.

theorem CompleteLattice.Independent.mono {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {s : ι → α} {t : ι → α} (hs : CompleteLattice.Independent s) (hst : t ≤ s) :

CompleteLattice.Independent t

theorem CompleteLattice.Independent.comp {α : Type u_1} [CompleteLattice α] {ι : Sort u_5} {ι' : Sort u_6} {t : ι → α} {f : ι' → ι} (ht : CompleteLattice.Independent t) (hf : Function.Injective f) :

CompleteLattice.Independent (t ∘ f)

Composing an independent indexed family with an injective function on the index results in another indepedendent indexed family.

theorem CompleteLattice.Independent.comp' {α : Type u_1} [CompleteLattice α] {ι : Sort u_5} {ι' : Sort u_6} {t : ι → α} {f : ι' → ι} (ht : CompleteLattice.Independent (t ∘ f)) (hf : Function.Surjective f) :

CompleteLattice.Independent t

theorem CompleteLattice.Independent.setIndependent_range {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} (ht : CompleteLattice.Independent t) :

CompleteLattice.SetIndependent (Set.range t)

theorem CompleteLattice.Independent.injective {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} (ht : CompleteLattice.Independent t) (h_ne_bot : ∀ (i : ι), t i ≠ ⊥) :

Function.Injective t

theorem CompleteLattice.independent_pair {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} {i : ι} {j : ι} (hij : i ≠ j) (huniv : ∀ (k : ι), k = i ∨ k = j) :

CompleteLattice.Independent t ↔ Disjoint (t i) (t j)

theorem CompleteLattice.Independent.map_orderIso {ι : Sort u_5} {α : Type u_6} {β : Type u_7} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) {a : ι → α} (ha : CompleteLattice.Independent a) :

CompleteLattice.Independent (↑f ∘ a)

Composing an independent indexed family with an order isomorphism on the elements results in another independent indexed family.

@[simp]

theorem CompleteLattice.independent_map_orderIso_iff {ι : Sort u_5} {α : Type u_6} {β : Type u_7} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) {a : ι → α} :

CompleteLattice.Independent (↑f ∘ a) ↔ CompleteLattice.Independent a

theorem CompleteLattice.Independent.disjoint_biSup {ι : Type u_5} {α : Type u_6} [CompleteLattice α] {t : ι → α} (ht : CompleteLattice.Independent t) {x : ι} {y : Set ι} (hx : ¬x ∈ y) :

Disjoint (t x) (⨆ (i : ι) (_ : i ∈ y), t i)

If the elements of a set are independent, then any element is disjoint from the iSup of some subset of the rest.

theorem CompleteLattice.independent_iff_supIndep {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {s : Finset ι} {f : ι → α} :

CompleteLattice.Independent (f ∘ Subtype.val) ↔ Finset.SupIndep s f

theorem CompleteLattice.Independent.supIndep {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {s : Finset ι} {f : ι → α} :

CompleteLattice.Independent (f ∘ Subtype.val) → Finset.SupIndep s f

Alias of the forward direction of CompleteLattice.independent_iff_supIndep.

theorem Finset.SupIndep.independent {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {s : Finset ι} {f : ι → α} :

Finset.SupIndep s f → CompleteLattice.Independent (f ∘ Subtype.val)

Alias of the reverse direction of CompleteLattice.independent_iff_supIndep.

theorem CompleteLattice.independent_iff_supIndep_univ {α : Type u_1} {ι : Type u_3} [CompleteLattice α] [Fintype ι] {f : ι → α} :

CompleteLattice.Independent f ↔ Finset.SupIndep Finset.univ f

A variant of CompleteLattice.independent_iff_supIndep for Fintypes.

theorem CompleteLattice.Independent.sup_indep_univ {α : Type u_1} {ι : Type u_3} [CompleteLattice α] [Fintype ι] {f : ι → α} :

CompleteLattice.Independent f → Finset.SupIndep Finset.univ f

Alias of the forward direction of CompleteLattice.independent_iff_supIndep_univ.

A variant of CompleteLattice.independent_iff_supIndep for Fintypes.

theorem Finset.SupIndep.independent_of_univ {α : Type u_1} {ι : Type u_3} [CompleteLattice α] [Fintype ι] {f : ι → α} :

Finset.SupIndep Finset.univ f → CompleteLattice.Independent f

Alias of the reverse direction of CompleteLattice.independent_iff_supIndep_univ.

A variant of CompleteLattice.independent_iff_supIndep for Fintypes.

theorem CompleteLattice.setIndependent_iff_pairwiseDisjoint {α : Type u_1} [Order.Frame α] {s : Set α} :

CompleteLattice.SetIndependent s ↔ Set.PairwiseDisjoint s id

theorem Set.PairwiseDisjoint.setIndependent {α : Type u_1} [Order.Frame α] {s : Set α} :

Set.PairwiseDisjoint s id → CompleteLattice.SetIndependent s

Alias of the reverse direction of CompleteLattice.setIndependent_iff_pairwiseDisjoint.

theorem CompleteLattice.independent_iff_pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [Order.Frame α] {f : ι → α} :

CompleteLattice.Independent f ↔ Pairwise (Disjoint on f)