Commit 2025-07-19 18:49 40256ad6

View on Github →

feat: decomposition into independent atoms (#21871) Prove that any element in a compactly generated modular atomistic lattice (eg the lattice of submodules of a module) can be written as the supremum of independent atoms. We already knew that ⊤ could be decomposed as such, and all this PR is doing is generalising a few intermediate statements. From PersistentDecomp and Xena

Estimated changes

modified theorem IsAtom.disjoint_of_ne
modified theorem IsAtom.inf_eq_bot_iff
modified theorem IsAtom.inf_eq_bot_of_ne
added theorem IsAtom.ne_bot
added theorem IsAtom.ne_bot_iff_eq
added theorem IsAtom.ne_iff_eq_bot
modified theorem IsCoatom.codisjoint_of_ne
added theorem IsCoatom.ne_iff_eq_top
added theorem IsCoatom.ne_top
added theorem IsCoatom.ne_top_iff_eq
modified theorem IsCoatom.sup_eq_top_iff
modified theorem IsCoatom.sup_eq_top_of_ne
deleted theorem atom_le_iSup
deleted theorem iInf_le_coatom
added theorem Set.insert_diff_subset