Zulip Chat Archive

Stream: general

Topic: meet in opens X


view this post on Zulip Johan Commelin (Nov 10 2018 at 18:03):

If I have U V : opens X, then (U ⊓ V).val is not defeq to U.val ∩ V.val. Can this be fixed while still using the galois insertion to define the lattice structure on opens X?

view this post on Zulip Johan Commelin (Nov 12 2018 at 13:16):

A related thing that I'm worried about: the opposite category of the category associated with a preorder is not going to be defeq to the category associated with the dual order.

view this post on Zulip Johannes Hölzl (Nov 12 2018 at 13:36):

(U ⊓ V).val := U.val ∩ V.val should be possible. And I think also that op ∘ order2cat = order2cat ∘ dual could be rfl. On both sides we construct a category using the constructor, which looks at the Hom-set fully expanded (so no funext is needed). So both sides should reduce to something like λα [ord], ⟨α, λa b, a ≥ b, ...⟩ (plus/minus some things).

Be aware that this is different to op (op C) = C where C doesn't reduce further

view this post on Zulip Johan Commelin (Nov 12 2018 at 13:37):

Ok, that's reassuring. Thanks!
So how should we make (U ⊓ V).val := U.val ∩ V.val happen?

view this post on Zulip Johannes Hölzl (Nov 12 2018 at 14:06):

wait, you mean the other way round, right?

lemma test (u v : opens α) : (u  v).val = u.val  v.val := rfl

works

view this post on Zulip Johannes Hölzl (Nov 12 2018 at 14:07):

Ah I see. We need to use complete_lattice.copy

view this post on Zulip Johannes Hölzl (Nov 12 2018 at 14:08):

there we can override the lattice operations with equal ones

view this post on Zulip Johan Commelin (Nov 12 2018 at 14:18):

I have no experience with this...

view this post on Zulip Johan Commelin (Nov 17 2018 at 16:18):

What is going on here? https://github.com/leanprover/mathlib/blob/master/order/filter.lean#L314
Locally there are two instances of complete lattice. Why does that not create trouble?
Also, once the complete lattice structure is copied, how can the Galois connection still work?

view this post on Zulip Reid Barton (Nov 17 2018 at 17:57):

"Locally" here is only up to the end of the section (line 341), and there's nothing else in the section.

view this post on Zulip Reid Barton (Nov 17 2018 at 18:03):

And by definition the new instance agrees with the existing preorder, has_top, has_inf instances

view this post on Zulip Johan Commelin (Dec 04 2018 at 19:27):

@Johannes Hölzl Does this look like what you had in mind?

instance : complete_lattice (opens α) :=
complete_lattice.copy
(@order_dual.lattice.complete_lattice _
  (@galois_insertion.lift_complete_lattice
    (order_dual (set α)) (order_dual (opens α)) _ interior (subtype.val : opens α  set α) _ gi))
/- le  -/ (λ U V, U.1  V.1) rfl
/- top -/ set.univ, _root_.is_open_univ (subtype.ext.mpr interior_univ.symm)
/- bot -/ , is_open_empty rfl
/- sup -/ (λ U V, U.1  V.1, _root_.is_open_union U.2 V.2) rfl
/- inf -/ (λ U V, U.1  V.1, _root_.is_open_inter U.2 V.2)
begin
  funext,
  apply subtype.ext.mpr,
  symmetry,
  apply interior_eq_of_open,
  exact (_root_.is_open_inter U.2 V.2),
end
/- Sup -/ (λ Us, ⋃₀ (subtype.val '' Us), _root_.is_open_sUnion $ λ U hU,
by { rcases hU with ⟨⟨V, hV, h, h', dsimp at h', subst h', exact hV})
begin
  funext,
  apply subtype.ext.mpr,
  simp [Sup_range],
  refl,
end
/- Inf -/ _ rfl

view this post on Zulip Johan Commelin (Dec 04 2018 at 19:34):

I guess this also needs a bunch of simp-lemmas to be useful?
Of the form opens_sup_val : (U \cap V).val = U.val \cap V.val := rfl.

view this post on Zulip Johan Commelin (Dec 04 2018 at 19:37):

The only thing I'm not so sure about is the Sup case of the "copy". It isn't rfl to what comes out of the galois insertion, but it also isn't very far of. Should I just use what comes out of the galois insertion, or is what I provide here the more useful thing. Feedback appreciated.

view this post on Zulip Johannes Hölzl (Dec 04 2018 at 20:49):

Yes, that's what I had in mind. If Sup doesn't make sense, then you don't need to change it. Just _ for Sup and rfl for the equality proof.

view this post on Zulip Johan Commelin (Dec 05 2018 at 04:14):

Sup is meaningful, and it gives you the "correct" answer modulo Sup_range. So now the question becomes whether I should make that simplification step here, or leave it to the user.
The one that is meaningless is Inf: it is the interior of an arbitrary intersection of opens.

view this post on Zulip Johan Commelin (Dec 05 2018 at 05:01):

#511


Last updated: May 14 2021 at 21:11 UTC