Complete Sublattice

Stream: Is there code for X?

[Oliver Nash]

We have a definition docs#Sublattice for sublattices but nothing for complete sublattices. We could define these along the following lines:

import Mathlib.Order.Sublattice

open Set

variable (α : Type*) [CompleteLattice α]

structure CompleteSublattice extends Sublattice α where
  sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
  sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier

namespace CompleteSublattice

variable (L : CompleteSublattice α)

instance instSetLike : SetLike (CompleteSublattice α) α where
  coe L := L.carrier
  coe_injective' L M h := by cases L; cases M; congr; exact SetLike.coe_injective' h

instance : Bot L where
  bot := ⟨⊥, by simpa using L.sSupClosed' <| empty_subset _⟩

instance : Top L where
  top := ⟨⊤, by simpa using L.sInfClosed' <| empty_subset _⟩

instance : SupSet L where
  sSup s := ⟨sSup s, L.sSupClosed' image_val_subset⟩

instance : InfSet L where
  sInf s := ⟨sInf s, L.sInfClosed' image_val_subset⟩

instance : CompleteLattice L :=
  Subtype.coe_injective.completeLattice _ (fun x y ↦ rfl) (fun x y ↦ rfl) sorry sorry rfl rfl

end CompleteSublattice

I claim this might save us a bit of boilerplate here and there. Has anyone, e.g., @Yaël Dillies any remarks about the desirability of this definition?

[Yaël Dillies]

There's currently exactly one use of sublattices, namely the four functions theorem (and it's not even crucial, just there to make a WLOG argument a bit easier), so it's hard to tell.

[Oliver Nash]

Thanks, that's roughly what I thought. I'll continue with what I'm doing and consider if it seems worth it.

[Yaël Dillies]

Actually, what use cases do you have in mind? Very often, we care about sublattices which are closed under infimum (eg subgroups) or under supremum (no example in mind but I'm sure they exist), but it's much rarer to have a sublattice which is closed under both.

[Antoine Chambert-Loir]

aren't subgroups and submodules, precisely, instances of such a complete lattices?

[Yaël Dillies]

No because the union of subgroups is not a subgroup. That was precisely the point of my previous message.

[Pedro Sánchez Terraf]

Antoine Chambert-Loir said:

aren't subgroups and submodules, precisely, instances of such a complete lattices?

They are, but the sup operation gives you the subgroup generated by the union. Is this not the way the family of substructures is regarded as a lattice?

[Jireh Loreaux]

What Yaël means is that it is not a sublattice in the sense that the coercion to sets of the sup operation on subgroups is not sup operation on sets of their coercion to sets.

So, it is a (complete) lattice, but only a sub-inf-iInf-semilattice.

[Yury G. Kudryashov]

Yaël Dillies said:

or under supremum (no example in mind ...)

docs#TopologicalSpace.Opens

[Oliver Nash]

Yaël Dillies said:

Actually, what use cases do you have in mind?

I don't think it's so hard to come up with examples.

How about the lattice of submodules of a module as a sublattice of the lattice of additive submonoids? (Related to my abandoned #9695, which I might unabandon if / when I feel I've made enough progress with my primary goal.)

The real example to hand is the collection of invariant submodules of a module wrt some (fixed) linear endomorphism. More generally another example is the lattice of Lie submodules of a Lie module. More generally still, surely any location where we use docs#Function.Injective.completeLattice and more generally still, the image of any docs#CompleteLatticeHom

[Oliver Nash]

(Btw I appreciate term has resumed Yaël so I'm not expecting you to spend further time replying here. I just wanted your quick opinion since you've written so much of this corner of the library; your remarks above have already been useful to me.)

[Yaël Dillies]

Oliver Nash said:

How about the lattice of submodules of a module as a sublattice of the lattice of additive submonoids?

The real example to hand is the collection of invariant submodules of a module wrt some (fixed) linear endomorphism. More generally another example is the lattice of Lie submodules of a Lie module.

Okay I can believe these are actually complete sublattices (sub-complete lattices?).

[Yaël Dillies]

Oliver Nash said:

any location where we use docs#Function.Injective.completeLattice and more generally still, the image of any docs#CompleteLatticeHom

Yeah that was basically my use case for docs#Sublattice. Precisely, the reason was that I needed to construct a sublattice L inside a proof and have Lean derive Lattice L. Without Sublattice, I would have needed to fill in docs#Subtype.lattice by hand, and that was particularly irritating in that instance since L was the sublattice generated by a set, so it was obviously closed under inf and sup and I thought it would be bad design to not interface that through a Sublattice type.

[Oliver Nash]

This similar to my situation (though not quite identical). I'll probably propose this new definition.

[Yaël Dillies]

Okay, great! Note that

• I have more Sublattice material in https://github.com/YaelDillies/LeanCamCombi/blob/master/LeanCamCombi/Mathlib/Order/Sublattice.lean
• @Yury G. Kudryashov is currently refactoring bundled sets, so the boilerplate you need to write might change very soon

[Yury G. Kudryashov]

Note that "submodules as a sublattice of additive submonoids" is not a sublattice (as in {s : AddSubmonoid M // _}) but a special type of homomorphism between complete lattices.

[Oliver Nash]

Yes, Submodule is its own type, not just a mere Subtype etc.

[Oliver Nash]

I persuaded myself this was worth having: #9763