Lifting (co)frames along Galois (co)insertions

Stream: general

[Yaël Dillies]

Can anybody do those? They are paper-trivial, but with all my will I can't get Lean to infer the intermediate complete_lattice instance.

import order.complete_boolean_algebra
import order.galois_connection

open order

variables {α β : Type*} {l : α → β} {u : β → α}

/-- Lift all suprema and infima along a Galois insertion. -/
@[reducible] -- See note [reducible non instances]
def lift_coframe [coframe α] [partial_order β] (gi : galois_insertion l u) : coframe β :=
{ infi_sup_le_sup_Inf := λ a s, begin
  change gi.choice _ _ ≤ l (_ ⊔ u (gi.choice _ _)),
  refine gi.u_le_u_iff.1 _,
  -- It *should* be obvious enough for `simp` at this point
  end,
  .. gi.lift_complete_lattice }

/-- Lift all suprema and infima along a Galois coinsertion. -/
@[reducible] -- See note [reducible non instances]
def lift_frame [frame α] [partial_order β] (gi : galois_coinsertion u l) : frame β :=
{ inf_Sup_le_supr_inf := sorry,
  .. gi.lift_complete_lattice }

[Yaël Dillies]

To be precise, for the first case (the second one is the same but with α and β swapped) I can't talk about any inf or sup in β because it's part of the instance I'm creating even though gi.lift_complete_lattice should do the job.

[Yaël Dillies]

And, no, haveI := gi.lift_complete_lattice doesn't do the trick.

[Yaël Dillies]

To show you how trivial this is once we have access to complete_lattice β, here's my solution for a concrete type, namely docs#topological_space.opens:

import topology.opens

open topological_space

instance {α : Type*} [topological_space α] : frame (opens α) :=
{ Sup := Sup,
  inf_Sup_le_supr_inf := λ a s, (opens.ext $ by simp only [opens.coe_inf, set.inf_eq_inter,
    opens.supr_s, opens.coe_Sup, set.inter_Union₂]).le,
  ..opens.complete_lattice }

[Yaël Dillies]

Also, yes, docs#topological_space.opens.gc really should be a galois_coinsertion.

[Yaël Dillies]

Looks like it's a diamond...

[Yaël Dillies]

Oh no it's even dumber. The lifts weren't marked reducible :face_palm: