Working with order duals

Stream: new members

[Christopher Hoskin]

Sorry, I'm afraid I'm stuck again. I have a class of normed lattices for which I can prove that the inf and sup operations are continuous. As these proofs are long and similar, I want to prove one and then infer the other from the equivalent property for the dual:

import analysis.normed_space.ordered

universe u

class normed_lattice_add_comm_group (α : Type u)
  extends normed_group α, lattice α :=
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
(notation `|`a`|` := a⊔-a) -- temporary notation within this definition
(solid' : ∀ a b : α, |a| ≤ |b| → ∥a∥ ≤ ∥b∥)

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))

-- If α is a normed lattice ordered group, so is order_dual α
instance {α : Type u} : Π [normed_lattice_add_comm_group α], normed_lattice_add_comm_group (order_dual α) := id

-- Proof omitted for brevity
instance normed_lattice_add_comm_group_has_continuous_inf {α : Type u} [normed_lattice_add_comm_group α] :
  has_continuous_inf α := sorry

-- If the inf is continuous in the order dual then the sup is continuous
instance has_continuous_inf_dual_has_continuous_sup
(L : Type*) [topological_space L] [has_sup L] [h: has_continuous_inf (order_dual L)] :
  has_continuous_sup  L :=
{
  continuous_sup :=
    @has_continuous_inf.continuous_inf  (order_dual L) _ _ h
}

-- If the order dual is a normed lattice ordered group, it has continuous inf
lemma dual_normed_lattice_add_comm_group_has_continuous_inf {α : Type u } [h: normed_lattice_add_comm_group (order_dual α)] : has_continuous_inf (order_dual α) :=
begin
  apply normed_lattice_add_comm_group_has_continuous_inf,
end

#check has_continuous_inf_dual_has_continuous_sup

set_option pp.all true
lemma normed_lattice_add_comm_group_dual_has_continuous_inf {α : Type u } [h: normed_lattice_add_comm_group α] : has_continuous_inf (order_dual α) :=
begin
  convert @dual_normed_lattice_add_comm_group_has_continuous_inf α h,
  -- ⊢ order_dual.has_inf α = semilattice_inf.to_has_inf (order_dual α)

  -- ⊢ @eq.{u+1}
  -- (has_inf.{u} (order_dual.{u} α))
  -- (@order_dual.has_inf.{u} α (@semilattice_sup.to_has_sup.{u} α (@lattice.to_semilattice_sup.{u} α (@normed_lattice_add_comm_group.to_lattice.{u} α h))))
  -- (@semilattice_inf.to_has_inf.{u} (order_dual.{u} α) (@lattice.to_semilattice_inf.{u} (order_dual.{u} α) (@normed_lattice_add_comm_group.to_lattice.{u} (order_dual.{u} α) h)))
  sorry
end

I've tried various permutations, but I always end up being asked to prove

order_dual.has_inf α = semilattice_inf.to_has_inf (order_dual α)

and at this point I get stuck.

Thanks,

Christopher

[Eric Wieser]

This looks wrong:

instance {α : Type u} : Π [normed_lattice_add_comm_group α], normed_lattice_add_comm_group (order_dual α) := id

this says order_dual α has the same lattice structure as α, not the dual structure

[Christopher Hoskin]

I adapted that line from this line in Mathlib

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

I think that line says that the dual of a topological space is also a topological space, so I assume my line says that the dual of a normed lattice ordered group is a normed lattice ordered group?

[Eric Wieser]

Yes, but the difference is a topological space has nothing to take the dual of

[Kevin Buzzard]

"Instance" is like "definition", not "theorem". This line in mathlib says "we define the topology on the dual space to be the same as the topology on the original space".

[Eric Wieser]

What you want to do here is copy the topology unmodified, and fill in the remaining fields using the existing instance for lattice (order_dual α)

[Christopher Hoskin]

Thank you. So, something more like:

instance {α : Type u} [h: normed_lattice_add_comm_group α] : normed_lattice_add_comm_group (order_dual α) := {
  add_le_add_left := sorry,
  solid' := sorry,
  ..h,
}

where the sorry remain to be proved?

[Kevin Buzzard]

..h is no good, that will give you the wrong lattice structure.

[Johan Commelin]

I think this also copies the definition of le from h to the order dual

[Johan Commelin]

You want .. order_dual.lattice h, or something like that.

[Christopher Hoskin]

Presumably

instance {α : Type u} : Π [normed_group α], normed_group (order_dual α) := id

is okay, as, like topological_space, the definition of normed_group is independent of order?

[Kevin Buzzard]

Yes, this part looks fine.

[Christopher Hoskin]

Okay, I think I have the proof that the order dual of a normed_lattice_add_comm_group is also a normed_lattice_add_comm_group correct now?

import analysis.normed_space.ordered
import algebra.ordered_group

universe u

class normed_lattice_add_comm_group (α : Type u)
  extends normed_group α, lattice α :=
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
(notation `|`a`|` := a⊔-a) -- temporary notation within this definition
(solid' : ∀ a b : α, |a| ≤ |b| → ∥a∥ ≤ ∥b∥)

-- Every (normed) lattice additive commutative group is also an ordered additive commutative group
-- @[priority 100] -- see Note [lower instance priority]
instance normed_lattice_add_comm_group.to_ordered_add_comm_group (α : Type u)
  [s : normed_lattice_add_comm_group α] : ordered_add_comm_group α :=
{ add := s.add, ..s }

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 {α : Type u} : Π [normed_group α], normed_group (order_dual α) := id

-- Special case of Bourbaki A.VI.9 (2)
-- (Actually this is true for a lattice_add_comm_group, but omit that for simplicity)
lemma neg_join_eq_neg_meet_neg {α : Type u} [normed_lattice_add_comm_group α] (a b : α) : -(a⊔b)=(-a)⊓(-b) :=
begin
  rw le_antisymm_iff,
  split,
  { rw le_inf_iff,
    split,
    { rw neg_le_neg_iff, apply le_sup_left, },
    { rw neg_le_neg_iff, apply le_sup_right, }
  },
  { rw ← neg_le_neg_iff, simp,
    split,
    { rw ← neg_le_neg_iff, simp, },
    { rw ← neg_le_neg_iff, simp, }
  }
end

lemma join_neg_eq_neg_meet {α : Type u} [normed_lattice_add_comm_group α] (a b : α) : -a⊔-b = -(a⊓b) :=
begin
  rw [← neg_neg (-a⊔-b), neg_join_eq_neg_meet_neg (-a) (-b), neg_neg, neg_neg],
end

lemma opsolid {α : Type u} [h: normed_lattice_add_comm_group α] : ∀ a b : α, a⊓-a ≥ b⊓-b → ∥a∥ ≤ ∥b∥ :=
begin
  intros a b h₁,
  apply h.solid',
  nth_rewrite 0 ← neg_neg a,
  rw join_neg_eq_neg_meet,
  nth_rewrite 0 ← neg_neg b,
  rw join_neg_eq_neg_meet,
  finish,
end

-- If α is a normed lattice ordered group, so is order_dual α
instance {α : Type u} [h: normed_lattice_add_comm_group α] : normed_lattice_add_comm_group (order_dual α) := {
  add_le_add_left := begin
    intros a b h₁ c,
    rw ← order_dual.dual_le,
    rw ← order_dual.dual_le at h₁,
    apply h.add_le_add_left,
    exact h₁,
  end,
  solid' := begin
    intros a b h₂,
    apply opsolid,
    rw ← order_dual.dual_le at h₂,
    finish,
  end,
}

However, I still get asked to prove order_dual.has_inf α = semilattice_inf.to_has_inf (order_dual α).

-- Proof omitted for brevity
instance normed_lattice_add_comm_group_has_continuous_inf {α : Type u} [normed_lattice_add_comm_group α] :
  has_continuous_inf α := sorry

-- If the inf is continuous in the order dual then the sup is continuous
instance has_continuous_inf_dual_has_continuous_sup
(L : Type*) [topological_space L] [has_sup L] [h: has_continuous_inf (order_dual L)] :
  has_continuous_sup  L :=
{
  continuous_sup :=
    @has_continuous_inf.continuous_inf  (order_dual L) _ _ h
}

-- If the order dual is a normed lattice ordered group, it has continuous inf
lemma dual_normed_lattice_add_comm_group_has_continuous_inf {α : Type u } [h: normed_lattice_add_comm_group (order_dual α)] : has_continuous_inf (order_dual α) :=
begin
  apply normed_lattice_add_comm_group_has_continuous_inf,
end

lemma normed_lattice_add_comm_group_dual_has_continuous_inf {α : Type u } [h: normed_lattice_add_comm_group α] : has_continuous_inf (order_dual α) :=
begin
  convert @dual_normed_lattice_add_comm_group_has_continuous_inf α h,
  -- ⊢ order_dual.has_inf α = semilattice_inf.to_has_inf (order_dual α)

  sorry
end

Thanks very much for all your help!

[Christopher Hoskin]

Do I need:

set_option old_structure_cmd true

in order to make this work? In Mathlib order/bounded_lattices.lean, bounded_lattice extends lattice and some other classes, and I notice it uses set_option old_structure_cmd true.

[Kevin Buzzard]

That option is for when you extend two typeclasses which have overlapping fields. I suspect normed_group and lattice don't have any overlapping fields so I don't think it will help.

[Kevin Buzzard]

I should add that I'm quite surprised this proof isn't refl (but it isn't)

[Kevin Buzzard]

In fact this goal seems to be false :-(

lemma normed_lattice_add_comm_group_dual_has_continuous_inf {α : Type u } [h: normed_lattice_add_comm_group α] : has_continuous_inf (order_dual α) :=
begin
  convert @dual_normed_lattice_add_comm_group_has_continuous_inf α h,
  -- ⊢ order_dual.has_inf α = semilattice_inf.to_has_inf (order_dual α)
  unfold order_dual.has_inf,
  delta semilattice_inf.to_has_inf,
  congr',
  ext a b,
  have : a ⊔ b = a ⊓ b := sorry, -- cheat by assuming false thing
  rw this,
  refl, -- unfortunately this now works
end

example (α : Type) [lattice α] (a b : α) : (show order_dual α, from a) ⊓ b = (a : α) ⊔ b := rfl -- fails
example (α : Type) [lattice α] (a b : α) : (show order_dual α, from a) ⊔ b = (a : α) ⊔ b := rfl -- works :-(

[Kevin Buzzard]

Actually your proof looks wrong to me, maybe this is expected behaviour. You've proved that NLACGs have a continuous_inf. Your convert line is claiming that what you're trying to prove (dual has continuous inf) follows from dual_normed_lattice_add_comm_group_has_continuous_inf but you're giving it the wrong h, if you give it h then it will identify alpha with its dual and now you're in trouble.

[Kevin Buzzard]

If you put attribute [irreducible] order_dual before normed_lattice_add_comm_group_dual_has_continuous_inf you'll see an error on the convert line, because now Lean cannot unify alpha and order_dual alpha, which is not what you want it to do anyway.

[Kevin Buzzard]

example (α : Type) [lattice α] (a b : α) : (show order_dual α, from a) ⊓ b = ((a ⊔ b : α) : order_dual α) := rfl -- works

OK I see where I was going wrong with my examples. It looks to me like we're back on track.

[Christopher Hoskin]

So, now I have

attribute [irreducible] order_dual

lemma normed_lattice_add_comm_group_dual_has_continuous_inf {α : Type u } [h: normed_lattice_add_comm_group α] : has_continuous_inf (order_dual α) :=
begin
  have h₁ : normed_lattice_add_comm_group (order_dual α) := begin
    exact order_dual.normed_lattice_add_comm_group,
  end,
  convert @dual_normed_lattice_add_comm_group_has_continuous_inf α h₁,
  {
    -- ⊢ order_dual.topological_space = uniform_space.to_topological_space
    sorry,
  },
  {
    -- ⊢ order_dual.has_inf α = semilattice_inf.to_has_inf (order_dual α)
    sorry,
  }
end

?

[Christopher Hoskin]

Better:

lemma normed_lattice_add_comm_group_dual_has_continuous_inf {α : Type u } [h: normed_lattice_add_comm_group α] : has_continuous_inf (order_dual α) :=
begin
  convert @dual_normed_lattice_add_comm_group_has_continuous_inf α order_dual.normed_lattice_add_comm_group,
  -- ⊢ order_dual.topological_space = uniform_space.to_topological_space
  sorry,
end

[Kevin Buzzard]

That goal looks true!

[Kevin Buzzard]

Your convert closes the goal for me. Don't put the irreducibility attribute on order_dual, that was just to show you where your abuse of definitional equality was not what you wanted. Abuse of defeq gives you alpha = order_dual alpha which is bad because then an inf or a sup might slip over that equality and become hard to work with.

[Kevin Buzzard]

The way which I would argue was the "correct" way to do this would be to make order_dual irreducible, define a map to_dual : alpha -> order_dual alpha which was id but defined before order_dual was made irreducible, and then prove a ton of lemmas about to_dual being an order-reversing isomorphism. But the CS people are too lazy to use this principled approach because they are more used to defeq abuse and it makes for shorter code. It's quite a knack to get it right though.

[Kevin Buzzard]

lemma normed_lattice_add_comm_group_dual_has_continuous_inf {α : Type u }
  [h: normed_lattice_add_comm_group α] : has_continuous_inf (order_dual α) :=
infer_instance

It just follows from the two other instances you've made.