Commit 2021-04-21 19:58 721e0b9e
View on Github →feat(order/complete_lattice): independence of an indexed family (#7199)
This PR reclaims the concept of independent
for elements of a complete lattice.
Right now it's defined on subsets -- a subset of a complete lattice L is independent if every
element of it is disjoint from (i.e. bot is the meet of it with) the Sup of all the other elements.
The problem with this is that if you have an indexed family f:I->L of elements of L then
duplications get lost if you ask for the image of f to be independent (rather like the issue
with a basis of a vector space being a subset rather than an indexed family). This is
an issue when defining gradings on rings, for example: if M is a monoid and R is
a ring, then I don't want the map which sends every m to (top : subgroup R) to
be independent.
I have renamed the set-theoretic version of independent
to set_independent