## 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
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
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
-- ⊢ 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 α) := {
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]

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 α) := {
intros a b h₁ c,
rw ← order_dual.dual_le,
rw ← order_dual.dual_le at h₁,
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
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
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
-- ⊢ 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
-- ⊢ 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
end,
{
-- ⊢ 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
-- ⊢ 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