[Merged by Bors] - feat(order/complete_lattice): independence of an indexed family

[kbuzzard]

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

---

A previously suggested name was sindependent (cf Union and sUnion) but am certainly open to other ideas!

[eric-wieser]

Looks good to me now, although I'll let someone else confirm the names are sufficiently bike-shedded.

I managed to prove the following, with the goal of trying to match the API that's there for set_independent, but the proof is ugly and I'm not convinced its useful anyway:

/-- If the elements of a set are independent, then any element is disjoint from the `supr` of some
subset of the rest. -/
lemma independent.disjoint_supr {ι : Type*} {α : Type*} [complete_lattice α]
  {s : ι → α} (hs : independent s) {x : ι} {y : set ι} (hx : x ∉ y) :
  disjoint (s x) (⨆ i ∈ y, s i) :=
begin
  classical,
  have ite_i : independent (λ i, if i ∈ y ∨ i = x then s i else ⊥) := (hs.mono _),
  convert ite_i x using 1,
  { simp, },
  { congr' 1,
    ext i,
    by_cases hiy : i ∈ y,
    { have : i ≠ x := ne_of_mem_of_not_mem hiy hx,
      simp [hiy, this], },
    by_cases hix : i = x,
    { simp [hix, hx], },
    simp [hix, hiy], },
  { intro i,
    dsimp only,
    split_ifs,
    refl,
    simp, }
end

[eric-wieser]

Although this lemma is probably useful:

/-- Composing an indepedent indexed family with an injective function on the index results in
another indepedendent indexed family. -/
lemma independent.comp {ι ι' : Sort*} {α : Type*} [complete_lattice α]
  {s : ι → α} (hs : independent s) (f : ι' → ι) (hf : function.injective f) :
  independent (s ∘ f) :=
λ i, (hs (f i)).mono_right begin
  refine (supr_le_supr $ λ i, _).trans (supr_comp_le _ f),
  exact supr_le_supr_const hf.ne,
end

[kbuzzard]

OK I managed to tame independent.disjoint_supr. I also remaned it -- apparently bsupr is a thing?

[robertylewis]

Looks good to me!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests