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 elementsfare supremum independent on the finite sets.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
@[simp]
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_iff_disjoint_erase
{α : Type u_1}
{ι : Type u_3}
[Lattice α]
[OrderBot α]
{s : Finset ι}
{f : ι → α}
[DecidableEq ι]
:
Finset.SupIndep s f ↔ ∀ 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)
@[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 : { x : ι // x ∈ s }) => 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 : { x : ι // x ∈ s }) => 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' ∈ 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' ∈ 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 : β i) => f { fst := i, snd := b })
(hg : ∀ i ∈ s, Finset.SupIndep (g i) fun (b : β i) => 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 #
An independent set of elements in a complete lattice is one in which every element is disjoint
from the Sup of the rest.
@[simp]
theorem
CompleteLattice.SetIndependent.mono
{α : Type u_1}
[CompleteLattice α]
{s : Set α}
(hs : CompleteLattice.SetIndependent s)
{t : Set α}
(hst : t ⊆ s)
:
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)
:
If the elements of a set are independent, then any element is disjoint from the sSup of some
subset of the rest.
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)
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 : ι → α}
:
theorem
CompleteLattice.independent_def''
{α : Type u_1}
{ι : Type u_3}
[CompleteLattice α]
{t : ι → α}
:
@[simp]
@[simp]
theorem
CompleteLattice.independent_pempty
{α : Type u_1}
[CompleteLattice α]
(t : PEmpty.{u_5} → α)
:
theorem
CompleteLattice.Independent.pairwiseDisjoint
{α : Type u_1}
{ι : Type u_3}
[CompleteLattice α]
{t : ι → α}
(ht : CompleteLattice.Independent 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)
:
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)
:
theorem
CompleteLattice.Independent.setIndependent_range
{α : Type u_1}
{ι : Type u_3}
[CompleteLattice α]
{t : ι → α}
(ht : CompleteLattice.Independent t)
:
@[simp]
theorem
CompleteLattice.independent_ne_bot_iff_independent
{α : Type u_1}
{ι : Type u_3}
[CompleteLattice α]
{t : ι → α}
:
(CompleteLattice.Independent fun (i : { i : ι // t i ≠ ⊥ }) => t ↑i) ↔ CompleteLattice.Independent t
theorem
CompleteLattice.Independent.injOn
{α : Type u_1}
{ι : Type u_3}
[CompleteLattice α]
{t : ι → α}
(ht : CompleteLattice.Independent t)
:
theorem
CompleteLattice.Independent.injective
{α : Type u_1}
{ι : Type u_3}
[CompleteLattice α]
{t : ι → α}
(ht : CompleteLattice.Independent t)
(h_ne_bot : ∀ (i : ι), t i ≠ ⊥)
:
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 : ι → α}
:
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 ∈ 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_of_independent_coe_Iic_comp
{α : Type u_1}
[CompleteLattice α]
{ι : Sort u_5}
{a : α}
{t : ι → ↑(Set.Iic a)}
(ht : CompleteLattice.Independent (Subtype.val ∘ t))
:
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.supIndep'
{α : Type u_1}
{ι : Type u_3}
[CompleteLattice α]
{f : ι → α}
(s : Finset ι)
(h : CompleteLattice.Independent f)
:
Finset.SupIndep s f
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 α}
:
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)