Zulip Chat Archive

Stream: maths

Topic: subobject_like class?


Thomas Browning (Jul 15 2022 at 10:17):

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 (Jul 15 2022 at 10:21):

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 (Jul 15 2022 at 10:22):

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

Thomas Browning (Jul 15 2022 at 10:22):

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

Thomas Browning (Jul 15 2022 at 10:23):

I also need to know this has_directed_unions property.

Thomas Browning (Jul 15 2022 at 10:23):

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

Yaël Dillies (Jul 15 2022 at 10:25):

Maybe you want a directed complete partial order?

Thomas Browning (Jul 15 2022 at 10:26):

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 (Jul 15 2022 at 10:27):

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

Andrew Yang (Jul 15 2022 at 10:30):

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 (Jul 15 2022 at 10:36):

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 (Jul 15 2022 at 11:48):

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.


Last updated: Dec 20 2023 at 11:08 UTC