Independent families and compactness

This file records lattice consequences of independence that involve compact elements and compact generation.

Main declarations

• Ado.finite_ne_bot_of_iSupIndep_of_isCompactElement: an independent family whose supremum is a compact element has only finitely many nonzero members. Compactness confines the whole family to a finite subfamily, and independence then forces every index outside it to be ⊥. This is the compactness variant of Mathlib's WellFoundedGT.finite_ne_bot_of_iSupIndep, which instead assumes the ascending chain condition.
• Ado.iSupIndep.iSup₂_inf_iSup_eq_iSup₂: a partial supremum of an independent family meets the total supremum of a pointwise dominated family in its corresponding partial supremum.
• Ado.iSupIndep.iSup₂_inf_iSup₂_eq_iSup₂_and: two partial suprema of an independent family meet in the supremum over the intersection of their index predicates.
• OrderIso.isCompactElement and OrderIso.isCompactElement_iff: an order isomorphism of complete lattices preserves and reflects compactness of elements.

theorem OrderIso.isCompactElement {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) {a : α} (ha : IsCompactElement a) : IsCompactElement (f a)

An order isomorphism of complete lattices sends compact elements to compact elements.

@[simp]

theorem OrderIso.isCompactElement_iff {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) {a : α} : IsCompactElement (f a) ↔ IsCompactElement a

An order isomorphism of complete lattices preserves and reflects compactness of elements.

theorem Ado.finite_ne_bot_of_iSupIndep_of_isCompactElement {α : Type u_1} {ι : Type u_2} [CompleteLattice α] {a : ι → α} (ha : iSupIndep a) (hc : IsCompactElement (⨆ (i : ι), a i)) : {i : ι | a i ≠ ⊥}.Finite

An independent family whose supremum is a compact element has only finitely many nonzero members.

theorem Ado.iSupIndep.iSup₂_inf_iSup_eq_iSup₂ {α : Type u_1} {ι : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] {A B : ι → α} (hA : iSupIndep A) (hB : ∀ (i : ι), B i ≤ A i) (P : ι → Prop) : (⨆ (i : ι), ⨆ (_ : P i), A i) ⊓ ⨆ (i : ι), B i = ⨆ (i : ι), ⨆ (_ : P i), B i

A subfamily of an independent family truncates a dominated supremum. If B i ≤ A i for every i and the A i are independent, then the total supremum of the B meets the partial supremum of the A over the indices satisfying P in exactly the partial supremum of the B over those indices.

theorem Ado.iSupIndep.iSup₂_inf_iSup₂_eq_iSup₂_and {α : Type u_1} {ι : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] {A : ι → α} (hA : iSupIndep A) (P Q : ι → Prop) : (⨆ (i : ι), ⨆ (_ : P i), A i) ⊓ ⨆ (i : ι), ⨆ (_ : Q i), A i = ⨆ (i : ι), ⨆ (_ : P i ∧ Q i), A i

Two partial suprema of an independent family meet in the partial supremum selected by both index predicates.