Finite atom decompositions in a complemented modular lattice

In a bounded modular lattice that is complemented and satisfies the descending chain condition, every element is the supremum of a finite independent family of atoms: split off an atom a of the element x, meet a complement of a with x, which the modular law makes a complement of a inside x, and recurse on that strictly smaller element.

Mathlib proves the corresponding statement for a complete lattice, where complementedness gives atomisticity and the decomposition is an arbitrary supremum (exists_sSupIndep_of_sSup_atoms, made finite by WellFoundedGT.finite_of_sSupIndep). The descending chain condition makes the family finite from the start, which is what lattices without arbitrary suprema — lattices of subobjects closed under finite meets and joins only — need.

Main declarations

• TauCeti.exists_finset_isAtom_sup_eq: in a complemented modular lattice satisfying the descending chain condition, every element is the supremum of a finite independent family of atoms.
• TauCeti.exists_isCompl_finset_sup_of_isAtom: if a finite family of atoms has supremum ⊤, every element has a complement that is the supremum of a subfamily.

theorem TauCeti.exists_finset_isAtom_sup_eq {L : Type u_1} [Lattice L] [BoundedOrder L] [IsModularLattice L] [ComplementedLattice L] [WellFoundedLT L] (x : L) : ∃ (s : Finset L), (∀ a ∈ s, IsAtom a) ∧ s.SupIndep id ∧ s.sup id = x

Finite atom decomposition. In a bounded modular lattice which is complemented and satisfies the descending chain condition, every element is the supremum of a finite independent family of atoms. This is semisimplicity for a lattice of subobjects: x is the direct sum of finitely many simple subobjects.

theorem TauCeti.exists_isCompl_finset_sup_of_isAtom {α : Type u_2} [Lattice α] [BoundedOrder α] [IsModularLattice α] {ι : Type u_3} [Fintype ι] {N : ι → α} (hN : ∀ (i : ι), IsAtom (N i)) (htop : Finset.univ.sup N = ⊤) (x : α) : ∃ (s : Finset ι), IsCompl x (s.sup N)

Complements from a generating family of atoms. In a bounded modular lattice, if a finite family of atoms has supremum ⊤, then every element has a complement that is the supremum of a subfamily: a subfamily maximal among those whose supremum is disjoint from the element.