Zulip Chat Archive

Stream: general

Topic: meet in opens X

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?

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.

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

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?

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


Johannes Hölzl (Nov 12 2018 at 14:07):

Ah I see. We need to use complete_lattice.copy

Johannes Hölzl (Nov 12 2018 at 14:08):

there we can override the lattice operations with equal ones

Johan Commelin (Nov 12 2018 at 14:18):

I have no experience with this...

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?

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.

Reid Barton (Nov 17 2018 at 18:03):

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

Johan Commelin (Dec 04 2018 at 19:27):

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

instance : complete_lattice (opens α) :=
(@order_dual.lattice.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)
  apply subtype.ext.mpr,
  apply interior_eq_of_open,
  exact (_root_.is_open_inter U.2 V.2),
/- 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})
  apply subtype.ext.mpr,
  simp [Sup_range],
/- Inf -/ _ rfl

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.

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.

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.

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.

Johan Commelin (Dec 05 2018 at 05:01):


Last updated: Dec 20 2023 at 11:08 UTC