# 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 : α) : -(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 (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