order_dual and continuity

Stream: new members

[Christopher Hoskin]

I'm trying to show that if the meet operation is continuous then the join operation is continuous. By analogy with this lemma from order/ord_continuous.lean :

protected lemma order_dual (hf : left_ord_continuous f) :
  @right_ord_continuous (order_dual α) (order_dual β) _ _ f := hf

I was hoping that something like this would work:

import topology.basic
import topology.constructions

class has_continuous_inf (L : Type*) [topological_space L] [has_inf L] : Prop :=
(continuous_inf : continuous (λ p : L × L, p.1 ⊓ p.2))

class has_continuous_sup (L : Type*) [topological_space L] [has_sup L] : Prop :=
(continuous_sup : continuous (λ p : L × L, p.1 ⊔ p.2))


instance (L : Type*) [h: topological_space L] : topological_space (order_dual L) :=
{
  ..h
}

instance has_continuous_inf_dual_has_continuous_sup
(L : Type*) [topological_space L] [has_inf L] [h: has_continuous_inf L] :
  has_continuous_sup (order_dual L) :=
{
  continuous_sup :=
    @has_continuous_inf.continuous_inf  L _ _ h
}

But the proof of continuous_sup fails with:

type mismatch at field 'continuous_sup'
  has_continuous_inf.continuous_inf
has type
  continuous (λ (p : L × L), p.fst ⊓ p.snd)
but is expected to have type
  continuous (λ (p : order_dual L × order_dual L), p.fst ⊔ p.snd)

Perhaps I need to show that a⊓b = a⊔ b where the right hand side is taken in the order dual, but after staring at this for a couple of evenings, I can't see how to formulate this statement in Lean, let alone prove it.

Please can someone give me a hint as where to go with this?

Thanks,

Christopher

[Kevin Buzzard]

The fix is

instance (L : Type*) [h: topological_space L] : topological_space (order_dual L) := h

instead of { ..h}.

Is this the same thing which @Sebastien Gouezel was talking about earlier?

[Kevin Buzzard]

NB the way I debugged this was

  continuous_sup := begin
    convert @has_continuous_inf.continuous_inf  L _ _ h,
    /-
    _inst_1: topological_space L
    ⊢ order_dual.topological_space L = _inst_1
    -/
    -- so the problem is that the top space instances are not *definitionally* equal
    -- let's check they're the same anyway
    tactic.unfreeze_local_instances,
    cases _inst_1,
    refl,
  end

[Kevin Buzzard]

def foo (L : Type*) [h: topological_space L] : topological_space (order_dual L) := { ..h}
def bar (L : Type*) [h: topological_space L] : topological_space (order_dual L) := h

example : @foo = @bar := rfl -- fails

example : @foo = @bar :=
begin
  ext,
  refl,
end

[Christopher Hoskin]

@Kevin Buzzard Thanks very much for the help and explaining how you solved it. Seems I was nearly there.

In fact I subsequently discovered that Mathlib already has an order_dual.topological_space object - if I import topology.algebra.ordered then that includes:

instance : Π [topological_space α], topological_space (order_dual α) := id

which also seems to work.

Christopher