# 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:
• Finset.supIndep_iff_pairwiseDisjoint
• CompleteLattice.setIndependent_iff_pairwiseDisjoint
• CompleteLattice.independent_iff_pairwiseDisjoint
• Otherwise, supremum independence is stronger than pairwise disjointness:
• Finset.SupIndep.pairwiseDisjoint
• CompleteLattice.SetIndependent.pairwiseDisjoint
• CompleteLattice.Independent.pairwiseDisjoint

## 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} [] [] (s : ) (f : ια) :

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

Equations
• s.SupIndep f = ∀ ⦃t : ⦄, t s∀ ⦃i : ι⦄, i sitDisjoint (f i) (t.sup f)
Instances For
instance Finset.instDecidableSupIndepOfDecidableEq {α : Type u_1} {ι : Type u_3} [] [] {s : } {f : ια} [] [] :
Decidable (s.SupIndep f)
Equations
• Finset.instDecidableSupIndepOfDecidableEq = Finset.decidableForallOfDecidableSubsets
theorem Finset.SupIndep.subset {α : Type u_1} {ι : Type u_3} [] [] {s : } {t : } {f : ια} (ht : t.SupIndep f) (h : s t) :
s.SupIndep f
@[simp]
theorem Finset.supIndep_empty {α : Type u_1} {ι : Type u_3} [] [] (f : ια) :
.SupIndep f
theorem Finset.supIndep_singleton {α : Type u_1} {ι : Type u_3} [] [] (i : ι) (f : ια) :
{i}.SupIndep f
theorem Finset.SupIndep.pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [] [] {s : } {f : ια} (hs : s.SupIndep f) :
(s).PairwiseDisjoint f
theorem Finset.SupIndep.le_sup_iff {α : Type u_1} {ι : Type u_3} [] [] {s : } {t : } {f : ια} {i : ι} (hs : s.SupIndep f) (hts : t s) (hi : i s) (hf : ∀ (i : ι), f i ) :
f i t.sup f i t
theorem Finset.supIndep_iff_disjoint_erase {α : Type u_1} {ι : Type u_3} [] [] {s : } {f : ια} [] :
s.SupIndep f is, Disjoint (f i) ((s.erase i).sup f)

The RHS looks like the definition of CompleteLattice.Independent.

theorem Finset.SupIndep.image {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [] [] {f : ια} [] {s : Finset ι'} {g : ι'ι} (hs : s.SupIndep (f g)) :
().SupIndep f
theorem Finset.supIndep_map {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [] [] {f : ια} {s : Finset ι'} {g : ι' ι} :
().SupIndep f s.SupIndep (f g)
@[simp]
theorem Finset.supIndep_pair {α : Type u_1} {ι : Type u_3} [] [] {f : ια} [] {i : ι} {j : ι} (hij : i j) :
{i, j}.SupIndep f Disjoint (f i) (f j)
theorem Finset.supIndep_univ_bool {α : Type u_1} [] [] (f : Boolα) :
Finset.univ.SupIndep f Disjoint () (f true)
@[simp]
theorem Finset.supIndep_univ_fin_two {α : Type u_1} [] [] (f : Fin 2α) :
Finset.univ.SupIndep f Disjoint (f 0) (f 1)
theorem Finset.SupIndep.attach {α : Type u_1} {ι : Type u_3} [] [] {s : } {f : ια} (hs : s.SupIndep f) :
s.attach.SupIndep fun (a : { x : ι // x s }) => f a
@[simp]
theorem Finset.supIndep_attach {α : Type u_1} {ι : Type u_3} [] [] {s : } {f : ια} :
(s.attach.SupIndep fun (a : { x : ι // x s }) => f a) s.SupIndep f
theorem Finset.supIndep_iff_pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [] [] {s : } {f : ια} :
s.SupIndep f (s).PairwiseDisjoint f
theorem Set.PairwiseDisjoint.supIndep {α : Type u_1} {ι : Type u_3} [] [] {s : } {f : ια} :
(s).PairwiseDisjoint fs.SupIndep f

Alias of the reverse direction of Finset.supIndep_iff_pairwiseDisjoint.

theorem Finset.sup_indep.pairwise_disjoint {α : Type u_1} {ι : Type u_3} [] [] {s : } {f : ια} :
s.SupIndep f(s).PairwiseDisjoint f

Alias of the forward direction of Finset.supIndep_iff_pairwiseDisjoint.

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

Bind operation for SupIndep.

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

Bind operation for SupIndep.

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

Bind operation for SupIndep.

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

### On complete lattices via sSup#

def CompleteLattice.SetIndependent {α : Type u_1} [] (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
Instances For
@[simp]
theorem CompleteLattice.SetIndependent.mono {α : Type u_1} [] {s : Set α} (hs : ) {t : Set α} (hst : t s) :
theorem CompleteLattice.SetIndependent.pairwiseDisjoint {α : Type u_1} [] {s : Set α} (hs : ) :
s.PairwiseDisjoint id

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

theorem CompleteLattice.setIndependent_singleton {α : Type u_1} [] (a : α) :
theorem CompleteLattice.setIndependent_pair {α : Type u_1} [] {a : α} {b : α} (hab : a b) :
theorem CompleteLattice.SetIndependent.disjoint_sSup {α : Type u_1} [] {s : Set α} (hs : ) {x : α} {y : Set α} (hx : x s) (hy : y s) (hxy : xy) :

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} [] (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
• = ∀ (i : ι), Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j i), t j)
Instances For
theorem CompleteLattice.setIndependent_iff {α : Type u_5} [] (s : Set α) :
theorem CompleteLattice.independent_def {α : Type u_1} {ι : Type u_3} [] {t : ια} :
∀ (i : ι), Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j i), t j)
theorem CompleteLattice.independent_def' {α : Type u_1} {ι : Type u_3} [] {t : ια} :
∀ (i : ι), Disjoint (t i) (sSup (t '' {j : ι | j i}))
theorem CompleteLattice.independent_def'' {α : Type u_1} {ι : Type u_3} [] {t : ια} :
∀ (i : ι), Disjoint (t i) (sSup {a : α | ∃ (j : ι), j i t j = a})
@[simp]
theorem CompleteLattice.independent_empty {α : Type u_1} [] (t : Emptyα) :
@[simp]
theorem CompleteLattice.independent_pempty {α : Type u_1} [] (t : ) :
theorem CompleteLattice.Independent.pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [] {t : ια} (ht : ) :
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} [] {s : ια} {t : ια} (hs : ) (hst : t s) :
theorem CompleteLattice.Independent.comp {α : Type u_1} [] {ι : Sort u_5} {ι' : Sort u_6} {t : ια} {f : ι'ι} (ht : ) (hf : ) :

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} [] {ι : Sort u_5} {ι' : Sort u_6} {t : ια} {f : ι'ι} (ht : ) (hf : ) :
theorem CompleteLattice.Independent.setIndependent_range {α : Type u_1} {ι : Type u_3} [] {t : ια} (ht : ) :
@[simp]
theorem CompleteLattice.independent_ne_bot_iff_independent {α : Type u_1} {ι : Type u_3} [] {t : ια} :
(CompleteLattice.Independent fun (i : { i : ι // t i }) => t i)
theorem CompleteLattice.Independent.injOn {α : Type u_1} {ι : Type u_3} [] {t : ια} (ht : ) :
Set.InjOn t {i : ι | t i }
theorem CompleteLattice.Independent.injective {α : Type u_1} {ι : Type u_3} [] {t : ια} (ht : ) (h_ne_bot : ∀ (i : ι), t i ) :
theorem CompleteLattice.independent_pair {α : Type u_1} {ι : Type u_3} [] {t : ια} {i : ι} {j : ι} (hij : i j) (huniv : ∀ (k : ι), k = i k = j) :
Disjoint (t i) (t j)
theorem CompleteLattice.Independent.map_orderIso {ι : Sort u_5} {α : Type u_6} {β : Type u_7} [] [] (f : α ≃o β) {a : ια} (ha : ) :

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} [] [] (f : α ≃o β) {a : ια} :
theorem CompleteLattice.Independent.disjoint_biSup {ι : Type u_5} {α : Type u_6} [] {t : ια} (ht : ) {x : ι} {y : Set ι} (hx : xy) :
Disjoint (t x) (iy, 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_of_independent_coe_Iic_comp {α : Type u_1} [] {ι : Sort u_5} {a : α} {t : ι()} (ht : CompleteLattice.Independent (Subtype.val t)) :
theorem CompleteLattice.independent_iff_supIndep {α : Type u_1} {ι : Type u_3} [] {s : } {f : ια} :
CompleteLattice.Independent (f Subtype.val) s.SupIndep f
theorem CompleteLattice.Independent.supIndep {α : Type u_1} {ι : Type u_3} [] {s : } {f : ια} :
CompleteLattice.Independent (f Subtype.val)s.SupIndep f

Alias of the forward direction of CompleteLattice.independent_iff_supIndep.

theorem Finset.SupIndep.independent {α : Type u_1} {ι : Type u_3} [] {s : } {f : ια} :
s.SupIndep fCompleteLattice.Independent (f Subtype.val)

Alias of the reverse direction of CompleteLattice.independent_iff_supIndep.

theorem CompleteLattice.Independent.supIndep' {α : Type u_1} {ι : Type u_3} [] {f : ια} (s : ) (h : ) :
s.SupIndep f
theorem CompleteLattice.independent_iff_supIndep_univ {α : Type u_1} {ι : Type u_3} [] [] {f : ια} :
Finset.univ.SupIndep f

A variant of CompleteLattice.independent_iff_supIndep for Fintypes.

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

Alias of the reverse direction of CompleteLattice.independent_iff_supIndep_univ.

A variant of CompleteLattice.independent_iff_supIndep for Fintypes.

theorem CompleteLattice.Independent.sup_indep_univ {α : Type u_1} {ι : Type u_3} [] [] {f : ια} :
Finset.univ.SupIndep f

Alias of the forward direction of CompleteLattice.independent_iff_supIndep_univ.

A variant of CompleteLattice.independent_iff_supIndep for Fintypes.

theorem CompleteLattice.setIndependent_iff_pairwiseDisjoint {α : Type u_1} [] {s : Set α} :
s.PairwiseDisjoint id
theorem Set.PairwiseDisjoint.setIndependent {α : Type u_1} [] {s : Set α} :
s.PairwiseDisjoint id

Alias of the reverse direction of CompleteLattice.setIndependent_iff_pairwiseDisjoint.

theorem CompleteLattice.independent_iff_pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [] {f : ια} :
Pairwise (Disjoint on f)