Zulip Chat Archive

Stream: new members

Topic: Working with order duals


Christopher Hoskin (Jun 21 2021 at 10:32):

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 (Jun 21 2021 at 10:38):

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 (Jun 21 2021 at 12:02):

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 (Jun 21 2021 at 12:03):

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

Kevin Buzzard (Jun 21 2021 at 12:03):

"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 (Jun 21 2021 at 12:04):

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 (Jun 21 2021 at 12:34):

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 (Jun 21 2021 at 12:36):

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

Johan Commelin (Jun 21 2021 at 12:36):

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

Johan Commelin (Jun 21 2021 at 12:37):

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

Christopher Hoskin (Jun 21 2021 at 12:49):

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 (Jun 21 2021 at 12:51):

Yes, this part looks fine.

Christopher Hoskin (Jun 21 2021 at 15:25):

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 : α) : -(ab)=(-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 = -(ab) :=
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 (Jun 22 2021 at 16:09):

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 (Jun 22 2021 at 16:24):

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 (Jun 22 2021 at 16:29):

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

Kevin Buzzard (Jun 22 2021 at 16:33):

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 (Jun 22 2021 at 16:53):

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 (Jun 22 2021 at 16:55):

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 (Jun 22 2021 at 17:08):

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 (Jun 22 2021 at 17:30):

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 (Jun 22 2021 at 17:32):

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 (Jun 22 2021 at 21:36):

That goal looks true!

Kevin Buzzard (Jun 22 2021 at 21:39):

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 (Jun 22 2021 at 21:41):

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 (Jun 22 2021 at 21:42):

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.


Last updated: Dec 20 2023 at 11:08 UTC