Zulip Chat Archive

Stream: general

Topic: lifting complete lattices


view this post on Zulip Johan Commelin (Feb 24 2020 at 16:00):

It seems to me that lifting a complete lattice gives you very very bad definitional equalities for supr and infi. I haven't really built an MWE, and I need to run to my train now. But a quasi-MWE is here: https://leanprover-community.github.io/lean-web-editor/#code=import%20order.galois_connection%20data.set.lattice%0A%0Auniverse%20variables%20u%20u'%0A%0Avariables%20%7BE%20%3A%20Type*%7D%20%7Bs%20%3A%20set%20E%7D%0A%0Aopen%20set%20lattice%0A%0A--%20Move%20this!!%20--%20this%20is%20some%20where%20in%20filter.lean%20but%20should%20be%20in%20a%20more%20general%20file%0Anamespace%20lattice%0Avariables%20%7B%CE%B1%20%3A%20Type%20u%7D%0A%0Adef%20complete_lattice.copy%20%28c%20%3A%20complete_lattice%20%CE%B1%29%0A%20%20%28le%20%3A%20%CE%B1%20%E2%86%92%20%CE%B1%20%E2%86%92%20Prop%29%20%28eq_le%20%3A%20le%20%3D%20%40complete_lattice.le%20%CE%B1%20c%29%0A%20%20%28top%20%3A%20%CE%B1%29%20%28eq_top%20%3A%20top%20%3D%20%40complete_lattice.top%20%CE%B1%20c%29%0A%20%20%28bot%20%3A%20%CE%B1%29%20%28eq_bot%20%3A%20bot%20%3D%20%40complete_lattice.bot%20%CE%B1%20c%29%0A%20%20%28sup%20%3A%20%CE%B1%20%E2%86%92%20%CE%B1%20%E2%86%92%20%CE%B1%29%20%28eq_sup%20%3A%20sup%20%3D%20%40complete_lattice.sup%20%CE%B1%20c%29%0A%20%20%28inf%20%3A%20%CE%B1%20%E2%86%92%20%CE%B1%20%E2%86%92%20%CE%B1%29%20%28eq_inf%20%3A%20inf%20%3D%20%40complete_lattice.inf%20%CE%B1%20c%29%0A%20%20%28Sup%20%3A%20set%20%CE%B1%20%E2%86%92%20%CE%B1%29%20%28eq_Sup%20%3A%20Sup%20%3D%20%40complete_lattice.Sup%20%CE%B1%20c%29%0A%20%20%28Inf%20%3A%20set%20%CE%B1%20%E2%86%92%20%CE%B1%29%20%28eq_Inf%20%3A%20Inf%20%3D%20%40complete_lattice.Inf%20%CE%B1%20c%29%20%3A%0A%20%20complete_lattice%20%CE%B1%20%3A%3D%0Abegin%0A%20%20refine%20%7B%20le%20%3A%3D%20le%2C%20top%20%3A%3D%20top%2C%20bot%20%3A%3D%20bot%2C%20sup%20%3A%3D%20sup%2C%20inf%20%3A%3D%20inf%2C%20Sup%20%3A%3D%20Sup%2C%20Inf%20%3A%3D%20Inf%2C%20..%7D%3B%0A%20%20%20%20subst_vars%2C%0A%20%20exact%20%40complete_lattice.le_refl%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.le_trans%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.le_antisymm%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.le_sup_left%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.le_sup_right%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.sup_le%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.inf_le_left%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.inf_le_right%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.le_inf%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.le_top%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.bot_le%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.le_Sup%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.Sup_le%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.Inf_le%20%CE%B1%20c%2C%0A%20%20exact%20%40complete_lattice.le_Inf%20%CE%B1%20c%0Aend%0A%0Aend%20lattice%0A%0Adef%20tmp%20%28s%20%3A%20set%20E%29%20%3A%20%40galois_insertion%20%28order_dual%20%28set%20E%29%29%20%28order_dual%20%7Bs'%20%2F%2F%20s'%20%E2%8A%86%20s%7D%29%20_%20_%0A%20%20%28%CE%BB%20%28s'%20%3A%20set%20E%29%2C%20%28%E2%9F%A8s%20%E2%88%A9%20s'%2C%20inter_subset_left%20s%20s'%E2%9F%A9%20%3A%20%7Bs'%20%2F%2F%20s'%20%E2%8A%86%20s%7D%29%29%0A%20%20%28%CE%BB%20%28s'%20%3A%20%7Bs'%20%2F%2F%20s'%20%E2%8A%86%20s%7D%29%2C%20%28s'%20%3A%20set%20E%29%29%20%3A%3D%0A%7B%20choice%20%3A%3D%20%CE%BB%20x%20hx%2C%20%E2%9F%A8x%2C%20subset.trans%20hx%20%24%20inter_subset_left%20_%20_%E2%9F%A9%2C%0A%20%20gc%20%3A%3D%20%CE%BB%20%28x%20%3A%20set%20E%29%20%28s'%20%3A%20%7Bs'%20%2F%2F%20s'%20%E2%8A%86%20s%7D%29%2C%20show%20s'%20%E2%89%A4%20%E2%9F%A8s%20%E2%88%A9%20x%2C%20_%E2%9F%A9%20%E2%86%94%20%E2%86%91s'%20%E2%89%A4%20x%2C%0A%20%20%20%20from%20%E2%9F%A8%CE%BB%20h%2C%20le_trans%20h%20%24%20inter_subset_right%20_%20_%2C%20subset_inter%20s'.property%E2%9F%A9%2C%0A%20%20le_l_u%20%3A%3D%20%CE%BB%20s'%2C%20inter_subset_right%20_%20_%2C%0A%20%20choice_eq%20%3A%3D%20%CE%BB%20%28x%20%3A%20set%20E%29%20h%2C%20subtype.ext.2%20%24%20subset.antisymm%20h%20%24%20inter_subset_right%20_%20_%20%7D%0A%0Adef%20tmpi%20%3A%20complete_lattice%20%7Bs'%20%2F%2F%20s'%20%E2%8A%86%20s%7D%20%3A%3D%0A%40order_dual.lattice.complete_lattice%20%28order_dual%20%7Bs'%20%2F%2F%20s'%20%E2%8A%86%20s%7D%29%20%24%0Agalois_insertion.lift_complete_lattice%20%28tmp%20s%29%0A%0Ainstance%20tmpii%20%3A%20complete_lattice%20%7Bs'%20%2F%2F%20s'%20%E2%8A%86%20s%7D%20%3A%3D%20tmpi.copy%0A%2F-%20le%20%20-%2F%20%28%E2%89%A4%29%20rfl%0A%2F-%20top%20-%2F%20%E2%9F%A8s%2C%20subset.refl%20s%E2%9F%A9%20%28subtype.coe_ext.mpr%20%24%20show%20s%20%3D%20s%20%E2%88%A9%20univ%2C%20from%20%28inter_univ%20s%29.symm%29%0A%2F-%20bot%20-%2F%20%E2%9F%A8%E2%88%85%2C%20_%E2%9F%A9%20rfl%0A%2F-%20sup%20-%2F%20%28%CE%BB%20s%E2%82%81%20s%E2%82%82%2C%20%E2%9F%A8s%E2%82%81%20%E2%88%AA%20s%E2%82%82%2C%20_%E2%9F%A9%29%20rfl%0A%2F-%20inf%20-%2F%20%28%CE%BB%20s%E2%82%81%20s%E2%82%82%2C%20%E2%9F%A8s%E2%82%81%20%E2%88%A9%20s%E2%82%82%2C%20subset.trans%20%28inter_subset_left%20_%20_%29%20s%E2%82%81.2%E2%9F%A9%29%0A%28by%20%7B%20ext%20s%E2%82%81%20s%E2%82%82%2C%20rw%20subtype.coe_ext%2C%20show%20%28s%E2%82%81%20%3A%20set%20E%29%20%E2%88%A9%20s%E2%82%82%20%3D%20s%20%E2%88%A9%20%28s%E2%82%81%20%E2%88%A9%20s%E2%82%82%29%2C%0A%20%20refine%20%28inter_eq_self_of_subset_right%20_%29.symm%2C%20exact%20subset.trans%20%28inter_subset_left%20_%20_%29%20s%E2%82%81.2%20%7D%29%0A%2F-%20Sup%20-%2F%20%28%CE%BB%20S%2C%20%E2%9F%A8%28%E2%8B%83%20s%20%E2%88%88%20S%2C%20%28s%20%3A%20set%20E%29%29%2C%20_%E2%9F%A9%29%20rfl%0A%2F-%20Inf%20-%2F%20%28%CE%BB%20S%2C%20%E2%9F%A8s%20%E2%88%A9%20%28%E2%8B%82%20s%20%E2%88%88%20S%2C%20%28s%20%3A%20set%20E%29%29%2C%20inter_subset_left%20_%20_%E2%9F%A9%29%20rfl%0A%0A%2F-%0ATODO%3A%0A--%20Lifting%20a%20complete%20lattice%20along%20a%20galois%20insertion%20gives%20horrible%0A--%20%60supr%60%20and%20%60infi%60%20as%20can%20be%20seen%20in%20the%20example%20below.%0A--%20TODO%3A%20Fix%20this%20in%20general%0A-%2F%0A%0Alemma%20help%20%7B%CE%B9%20%3A%20Sort%20u'%7D%20%28f%20%3A%20%CE%B9%20%E2%86%92%20%7Bs'%20%2F%2F%20s'%20%E2%8A%86%20s%7D%29%20%3A%0A%20%20%28%28%28%E2%A8%85%20i%2C%20f%20i%29%20%3A%20%7Bs'%20%2F%2F%20s'%20%E2%8A%86%20s%7D%29%20%3A%20set%20E%29%20%3D%20s%20%E2%88%A9%20%28%E2%8B%82%20i%2C%20%28f%20i%20%3A%20set%20E%29%29%20%3A%3D%0Abegin%0A%20%20have%20%3A%3D%20%28tmp%20s%29.gc.l_supr%2C%0A%20%20swap%203%2C%20exact%20%CE%BB%20%28i%3A%CE%B9%29%2C%20%28f%20i%20%3A%20set%20E%29%2C%0A%20%20rw%20subtype.coe_ext%20at%20this%2C%0A%20%20dsimp%20at%20this%2C%0A%20%20convert%20this%2C%0A%20%20show%20s%20%E2%88%A9%20_%20%3D%20s%20%E2%88%A9%20_%2C%0A%20%20sorry%0A%20%20--%20apply%20subset.antisymm%2C%0A%20%20--%20%7B%20sorry%20%7D%2C%0A%20%20--%20%7B%20refine%20%28tmp%20s%29.gc.l_supr%2C%20%7D%2C%0Aend

view this post on Zulip Johan Commelin (Feb 24 2020 at 16:01):

Code:

import order.galois_connection data.set.lattice

universe variables u u'

variables {E : Type*} {s : set E}

open set lattice

-- Move this!! -- this is some where in filter.lean but should be in a more general file
namespace lattice
variables {α : Type u}

def complete_lattice.copy (c : complete_lattice α)
  (le : α  α  Prop) (eq_le : le = @complete_lattice.le α c)
  (top : α) (eq_top : top = @complete_lattice.top α c)
  (bot : α) (eq_bot : bot = @complete_lattice.bot α c)
  (sup : α  α  α) (eq_sup : sup = @complete_lattice.sup α c)
  (inf : α  α  α) (eq_inf : inf = @complete_lattice.inf α c)
  (Sup : set α  α) (eq_Sup : Sup = @complete_lattice.Sup α c)
  (Inf : set α  α) (eq_Inf : Inf = @complete_lattice.Inf α c) :
  complete_lattice α :=
begin
  refine { le := le, top := top, bot := bot, sup := sup, inf := inf, Sup := Sup, Inf := Inf, ..};
    subst_vars,
  exact @complete_lattice.le_refl α c,
  exact @complete_lattice.le_trans α c,
  exact @complete_lattice.le_antisymm α c,
  exact @complete_lattice.le_sup_left α c,
  exact @complete_lattice.le_sup_right α c,
  exact @complete_lattice.sup_le α c,
  exact @complete_lattice.inf_le_left α c,
  exact @complete_lattice.inf_le_right α c,
  exact @complete_lattice.le_inf α c,
  exact @complete_lattice.le_top α c,
  exact @complete_lattice.bot_le α c,
  exact @complete_lattice.le_Sup α c,
  exact @complete_lattice.Sup_le α c,
  exact @complete_lattice.Inf_le α c,
  exact @complete_lattice.le_Inf α c
end

end lattice

def tmp (s : set E) : @galois_insertion (order_dual (set E)) (order_dual {s' // s'  s}) _ _
  (λ (s' : set E), (s  s', inter_subset_left s s' : {s' // s'  s}))
  (λ (s' : {s' // s'  s}), (s' : set E)) :=
{ choice := λ x hx, x, subset.trans hx $ inter_subset_left _ _⟩,
  gc := λ (x : set E) (s' : {s' // s'  s}), show s'  s  x, _⟩  s'  x,
    from ⟨λ h, le_trans h $ inter_subset_right _ _, subset_inter s'.property,
  le_l_u := λ s', inter_subset_right _ _,
  choice_eq := λ (x : set E) h, subtype.ext.2 $ subset.antisymm h $ inter_subset_right _ _ }

def tmpi : complete_lattice {s' // s'  s} :=
@order_dual.lattice.complete_lattice (order_dual {s' // s'  s}) $
galois_insertion.lift_complete_lattice (tmp s)

instance tmpii : complete_lattice {s' // s'  s} := tmpi.copy
/- le  -/ () rfl
/- top -/ s, subset.refl s (subtype.coe_ext.mpr $ show s = s  univ, from (inter_univ s).symm)
/- bot -/ , _⟩ rfl
/- sup -/ (λ s₁ s₂, s₁  s₂, _⟩) rfl
/- inf -/ (λ s₁ s₂, s₁  s₂, subset.trans (inter_subset_left _ _) s₁.2)
(by { ext s₁ s₂, rw subtype.coe_ext, show (s₁ : set E)  s₂ = s  (s₁  s₂),
  refine (inter_eq_self_of_subset_right _).symm, exact subset.trans (inter_subset_left _ _) s₁.2 })
/- Sup -/ (λ S, ( s  S, (s : set E)), _⟩) rfl
/- Inf -/ (λ S, s  ( s  S, (s : set E)), inter_subset_left _ _⟩) rfl

/-
TODO:
-- Lifting a complete lattice along a galois insertion gives horrible
-- `supr` and `infi` as can be seen in the example below.
-- TODO: Fix this in general
-/

lemma help {ι : Sort u'} (f : ι  {s' // s'  s}) :
  ((( i, f i) : {s' // s'  s}) : set E) = s  ( i, (f i : set E)) :=
begin
  have := (tmp s).gc.l_supr,
  swap 3, exact λ (i:ι), (f i : set E),
  rw subtype.coe_ext at this,
  dsimp at this,
  convert this,
  show s  _ = s  _,
  sorry
  -- apply subset.antisymm,
  -- { sorry },
  -- { refine (tmp s).gc.l_supr, },
end

view this post on Zulip Johan Commelin (Feb 24 2020 at 16:02):

If I'm doing something stupid, I would love to be enlightened

view this post on Zulip Johan Commelin (Feb 24 2020 at 16:13):

Walking to the train helped.

view this post on Zulip Johan Commelin (Feb 24 2020 at 16:14):

I think this has nothing to do with lifting the lattice structure

view this post on Zulip Johan Commelin (Feb 24 2020 at 16:14):

What is really the problem is that some useful lemmas for how galois_insertion interacts with supr are missing.

view this post on Zulip Mario Carneiro (Feb 24 2020 at 18:59):

The function complete_lattice.copy is there to fix up any bad definitional equalities caused by another definition

view this post on Zulip Johan Commelin (Feb 24 2020 at 19:04):

Yes, but it doesn't help here. Because supr and infi are defined in terms of range.

view this post on Zulip Johan Commelin (Feb 24 2020 at 19:04):

lemma help {ι : Sort u'} (f : ι  {s' // s'  s}) :
  ((( i, f i) : {s' // s'  s}) : set E) = s  ( i, (f i : set E)) :=

looks like it should be a triviality, but it isn't.

view this post on Zulip Johan Commelin (Feb 24 2020 at 19:05):

And I now realised that this has nothing to do with complete_lattice.copy or lift_complete_lattice. It's just an inherent problem with supr and infi.

view this post on Zulip Mario Carneiro (Feb 24 2020 at 20:32):

yes

view this post on Zulip Mario Carneiro (Feb 24 2020 at 20:32):

you have to use lemmas to get the version you want

view this post on Zulip Mario Carneiro (Feb 24 2020 at 20:33):

it's impossible to put supr and infi with the "right" definitional equality in the structure, because that would involve quantifying over all universes

view this post on Zulip Johan Commelin (Feb 24 2020 at 20:39):

I know. But this is still very unfortunate (-;

view this post on Zulip Johan Commelin (Feb 24 2020 at 20:40):

lemma l_supr_u [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
  {ι : Sort x} (f : ι  β) :
  l ( i, u (f i)) =  i, (f i) :=
calc l ( (i : ι), u (f i)) =  (i : ι), l (u (f i)) : gi.gc.l_supr
                        ... =  (i : ι), f i : congr_arg _ $ funext $ λ i, gi.l_u_eq (f i)

lemma l_supr_of_ul [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
  {ι : Sort x} (f : ι  α) (hf :  i, u (l (f i)) = f i) :
  l ( i, (f i)) =  i, l (f i) :=
calc l ( (i : ι), (f i)) = l  (i : ι), (u (l (f i))) : by simp [hf]
                        ... =  (i : ι), l (f i) : gi.l_supr_u _

lemma l_infi_u [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
  {ι : Sort x} (f : ι  β) :
  l ( i, u (f i)) =  i, (f i) :=
calc l ( (i : ι), u (f i)) = l (u ( (i : ι), (f i))) : congr_arg l gi.gc.u_infi.symm
                        ... =  (i : ι), f i : gi.l_u_eq _

lemma l_infi_of_ul [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
  {ι : Sort x} (f : ι  α) (hf :  i, u (l (f i)) = f i) :
  l ( i, (f i)) =  i, l (f i) :=
calc l ( i, (f i)) =  l  (i : ι), (u (l (f i))) : by simp [hf]
                ... =  i, l (f i) : gi.l_infi_u _

@Mario Carneiro We are missing things like :up:


Last updated: May 14 2021 at 13:24 UTC