Zulip Chat Archive

Stream: maths

Topic: supr is union of finite supr


Thomas Browning (Jul 14 2022 at 14:13):

I want to know that a supr of intermediate_fields is the union of finite suprs. But this sort of result holds for other subobjects (e.g., subgroups), so I'm wondering if you order-theory folks know the right way to state/prove this sort of thing?

import field_theory.adjoin

variables {K L ι : Type*} [field K] [field L] [algebra K L] {f : ι  intermediate_field K L}

example : (( i : ι, f i : intermediate_field K L) : set L) =
   s : finset ι, (( i  s, f i : intermediate_field K L) : set L) :=
sorry

example {x : L} (hx : x   i : ι, f i) :  s : set ι, s.finite  x   i  s, f i :=
sorry

Yaël Dillies (Jul 14 2022 at 14:20):

This is a general fact about complete lattices, right? It's very easy to prove by antisymmetry.

Eric Rodriguez (Jul 14 2022 at 14:22):

does the second thing hold in complete lattices too?

Thomas Browning (Jul 14 2022 at 14:24):

But can you talk about unions or membership in complete lattices?

Yaël Dillies (Jul 14 2022 at 14:24):

It doesn't make sense as stated, because of the membership relation, but you can replace x ∈ _ by x ≤ _ for an atom x and then it should hold in complete atomic lattices.

Andrew Yang (Jul 14 2022 at 14:25):

The right hand side is in term of sets, so I would imagine it needs some more galois connection magic between the subobject lattice and the set lattice?

Yaël Dillies (Jul 14 2022 at 14:25):

(x ∈ s ↔ {x} ≤ s and {x} is an atom)

Thomas Browning (Jul 14 2022 at 14:25):

Andrew Yang said:

The right hand side is in term of sets, so I would imagine it needs some more galois connection magic between the subobject lattice and the set lattice?

Exactly

Thomas Browning (Jul 14 2022 at 14:26):

And the whole point is that there is a , which makes sense in sets, but not in arbitrary complete lattices.

Yaël Dillies (Jul 14 2022 at 14:27):

You can just eliminate the coercions.

Eric Rodriguez (Jul 14 2022 at 14:28):

how would you state these two in lattice terms, Yael?

Rémy Degenne (Jul 14 2022 at 14:28):

docs#supr_eq_supr_finset looks close to what is written here, up to that union/supr difference

Thomas Browning (Jul 14 2022 at 14:28):

But there's a , which is not the same as

Yaël Dillies (Jul 14 2022 at 14:28):

Yeah okay

Yaël Dillies (Jul 14 2022 at 14:28):

Then that's surely not a general fact about complete lattices after all.

Thomas Browning (Jul 14 2022 at 14:29):

Right. But maybe with some Galois connection magic?

Thomas Browning (Jul 14 2022 at 14:53):

Here's a potential generalization:

def subobject (α : Type*) : Type* := sorry

namespace subobject

variables {α : Type*}

instance : has_coe (subobject α) (set α) := sorry

lemma coe_injective : function.injective (coe : subobject α  set α) := sorry

def closure : set α  subobject α := sorry

instance : partial_order (subobject α) := partial_order.lift coe coe_injective

def key_fact : galois_insertion (closure : set α  subobject α) (coe : subobject α  set α) :=
sorry

instance : complete_lattice (subobject α) := key_fact.lift_complete_lattice

variables {ι : Type*} {f : ι  subobject α}

example : (( i : ι, f i : subobject α) : set α) =
   s : finset ι, (( i  s, f i : subobject α) : set α) :=
sorry

end subobject

Thomas Browning (Jul 14 2022 at 14:59):

So I guess I'm wondering:

  • Is this last sorry true (perhaps with more assumptions?)
  • Is there a better way to state the last example so that it would automatically apply to subgroups, subalgebras, intermediate_fields, etc...?

Thomas Browning (Jul 14 2022 at 16:15):

It feels like the key property of subgroups, subalgebras, intermediate_fields, etc.. is that a direct limit of subobjects is a subobject (e.g., docs#field.direct_limit.field). But it's not entirely clear how to best phrase this in order-theoretic language.

Anne Baanen (Jul 14 2022 at 17:43):

I think you're looking for something related to docs#lower_adjoint

Anne Baanen (Jul 14 2022 at 17:49):

If I parse everything correctly, docs#lower_adjoint.closure_Union_closure is the first step, but it looks like there is nothing related to finiteness...

Junyan Xu (Jul 16 2022 at 00:46):

Let me observe that filters also satisfies a similar identity:

import order.filter.basic
lemma sets_infi_eq_Union {X ι} {f : ι  filter X} :
  ( i : ι, f i).sets =  s : finset ι, ( i  s, f i).sets :=
begin
  ext, simp_rw [set.mem_Union, filter.mem_sets], rw filter.mem_infi, split,
  { rintro I, hI, hx⟩, use hI.to_finset, letI := hI.fintype,
    rw [ filter.mem_infi_of_fintype, infi_subtype''] at hx,
    simp_rw hI.mem_to_finset, exact hx },
  { rintro I, hx⟩, use [I, I.finite_to_set],
    simp_rw [ filter.mem_infi_of_fintype, infi_subtype'', finset.mem_coe],
    exact hx },
end

is replaced here because filter.sets is antitone/contravariant.

Junyan Xu (Jul 16 2022 at 03:03):

And the filters almost satisfies the preserves_filtered_colimits condition, except it requires an additional condition that ι : set α is nonempty! It's basically stated as docs#filter.infi_sets_eq, and just a little maneuver is required to put it in the form of preserves_filtered_colimits:

import order.filter.basic
lemma filter_sets_preserves_filtered_colimits
  {X} {s : set (filter X)} [nonempty s] (hs : directed_on () s) :
  ( U  s, U).sets =  U  s, filter.sets U :=
begin
  rw [ infi_subtype'',  supr_subtype''],
  apply filter.infi_sets_eq,
  rintro a, ha b, hb⟩,
  obtain c, hc, h := hs a ha b hb,
  exact ⟨⟨c, hc⟩, h⟩,
end

When s is empty, the LHS is (⊤ : filter X).sets, which is the singleton {set.univ} : set (set X), while the RHS is the empty set. Such peculiarity! Incidentally, the filter constructed in the proof of src#filter.infi_sets_eq is very similar to filter_of_directed in my recent code snippet, and requires similar conditions.

Thomas Browning (Jul 16 2022 at 08:41):

Yes, the nonempty hypothesis is needed in basically every situation (an empty union of subobjects is almost never going to be a subobject).

Thomas Browning (Jul 16 2022 at 08:43):

@Sam van G Pointed out that mathlib has docs#is_compactly_generated. This might be the right way to phrase things. You first prove compactly generated instances for everything, and then you write one lemma stating that a supr is a union of finite suprs (assuming a function to sets or perhaps to something more general).


Last updated: Dec 20 2023 at 11:08 UTC