supr is union of finite supr

Stream: maths

[Thomas Browning]

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]

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

[Eric Rodriguez]

does the second thing hold in complete lattices too?

[Thomas Browning]

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

[Yaël Dillies]

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]

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]

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

[Thomas Browning]

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]

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

[Yaël Dillies]

You can just eliminate the coercions.

[Eric Rodriguez]

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

[Rémy Degenne]

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

[Thomas Browning]

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

[Yaël Dillies]

Yeah okay

[Yaël Dillies]

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

[Thomas Browning]

Right. But maybe with some Galois connection magic?

[Thomas Browning]

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]

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]

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]

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

[Anne Baanen]

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]

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]

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]

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]

@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).