unions / sups of lattice ideals

Stream: mathlib4

[Sam van G]

The following came up in @Antoine Chambert-Loir's review of my PR #12705 and I wonder what other more experienced Mathlib users think. Currently, the operation sSup on the type Ideal P, where P is a sup-semilattice with bottom, is defined via the CompleteLattice instance, inferred from the fact that any intersection of ideals is an ideal. However, in practice (e.g. around here), one often wants to know that the sSup of a set of ideals is actually equal to a union. The mathematical reason for this is that the union of a directed set of ideals is again an ideal (in Mathlib here).
Is the correct solution to this to add a (simp?) rewrite lemma somewhere that lets one rewrite sSup into sUnion, provided that the collection of ideals is directed?

[Ruben Van de Velde]

Yeah, I guess it makes sense to add the lemma. Not sure about simp

[Yaël Dillies]

Agreed, shouldn't be simp

[Eric Wieser]

I think docs#Submodule.coe_iSup_of_directed is the lemma?

[Yaël Dillies]

It is simp :fear:

[Antoine Chambert-Loir]

In fact, that's for ideals of rings, while Sam wants the analogous result for ideals of lattices. The proof is essentially the same, though, relying on the fact that being an ideal is a property of finite character. It would be the same if one had a refined coercion class. (By the way, couldn't the coercion class provide automatic lemmas of the form IsIdeal, etc.?)

[Sam van G]

Thanks. I'll have a look if I can reproduce docs#Submodule.coe_iSup_of_directed in the lattice context.

[Eric Wieser]

Oh, you mean docs#Order.Ideal not docs#Ideal !

[Sam van G]

Yes, sorry, it's in the topic title but not explicit in the text