Zulip Chat Archive

Stream: general

Topic: lifting complete lattices


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

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

Johan Commelin (Feb 24 2020 at 16:02):

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

Johan Commelin (Feb 24 2020 at 16:13):

Walking to the train helped.

Johan Commelin (Feb 24 2020 at 16:14):

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

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.

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

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.

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.

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.

Mario Carneiro (Feb 24 2020 at 20:32):

yes

Mario Carneiro (Feb 24 2020 at 20:32):

you have to use lemmas to get the version you want

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

Johan Commelin (Feb 24 2020 at 20:39):

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

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: Aug 03 2023 at 10:10 UTC