Zulip Chat Archive

Stream: general

Topic: lifting complete lattices

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

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: Dec 20 2023 at 11:08 UTC