subobject_like class?

Stream: maths

[Thomas Browning]

I'm wondering if it would make sense to add a subobject_like class extending set_like and providing a complete_lattice instance? (example code at the end of the message)

My motivation is that I want to state a lemma like

lemma : ((⨆ i : ι, f i : subgroup α) : set α) = ⋃ s : finset ι, ((⨆ i ∈ s, f i : subgroup α) : set α) := sorry

that holds for subgroups, subalgebras, intermediate_fields, etc... It seems that the natural way to do this sort of thing would be to:

• Add a typeclass or predicate has_directed_unions saying "you take can directed unions of this sort of subobject"
• Prove has_directed_unions for subgroup, subalgebra, intermediate_field, etc...
• Prove the lemma assuming has_directed_unions
  But I can't even state the lemma unless I know that the subobjects form a complete lattice. And I can't just add a complete_lattice instance as a hypothesis because it won't necessarily be compatible with the partial order from set_like. So would it make sense to add a typeclass extending set_like that bundles up the galois_insertion and gives the complete_lattice instance?

Here's some code:

import data.set.lattice
import data.set_like.basic

variables (α β : Type*)

class subobject_like extends set_like α β :=
(closure : set β → α)
(gi : galois_insertion closure coe)

namespace subobject_like

instance [h : subobject_like α β] : complete_lattice α :=
h.gi.lift_complete_lattice

end subobject_like

[Yaël Dillies]

It makes more sense to me to prove those lemmas using any Galois insertion, rather than restricting to set + set_like on one side.

[Thomas Browning]

Ah, of course. I'll give it a shot.

[Thomas Browning]

Well, actually it's not true for any Galois insertion.

[Thomas Browning]

I also need to know this has_directed_unions property.

[Thomas Browning]

But I suppose I could try to formulate that in terms of the Galois insertion too.

[Yaël Dillies]

Maybe you want a directed complete partial order?

[Thomas Browning]

Well, I want to assume that the subobjects form a complete lattice, but that taking the supr of a directed subset is compatible with the Galois insertion.

[Thomas Browning]

In other words, that the supremum of a directed collection of subobjects equals the union of the directed collection of subobjects

[Andrew Yang]

I would assume the has_directed_unions is something like "preserves filtered colimits", so it should be able to be made into a predicate of an order preserving map?

[Thomas Browning]

I guess you could just add a definition

def preserves_filtered_colimits {α β : Type*} [has_le α] [has_Sup α] [has_Sup β] (f : α → β) :=
∀ ι : set α, directed_on (≤) ι → f (⨆ i ∈ ι, i) = ⨆ i ∈ ι, f i

and prove preserves_filtered_colimits coe for subgroups, subalgebras, intermediate_fields, etc...

[Eric Wieser]

I agree that such a class would be nice; I found myself wanting it for docs#direct_sum.is_internal_submodule_iff_independent_and_supr_eq_top, which I can't currently state in the generality of add_subgroup_class because that doesn't come with a lattice structure.