lattices, linear orders and germs

Stream: new members

[Christopher Hoskin]

In order to complete a proof, lean is asking me to show that lattice_of_linear_order = germ.lattice which I think means:

"Given a filter and a linear order β, the linear order induces a lattice structure on β, which induces a lattice structure on the germ. The linear order also induces a linear order on the germ, which in turn induces a lattice structure on the germ. Show that the two lattice structures coincide."

The trouble is, I can't figure out how to formulate this as a lemma, even to be proved with sorry. I'm trying something like:

universe u
lemma test {α : Type u} {β : Type u} [l: filter α] [h: linear_order β] : lattice_of_linear_order linear_order (filter.germ l β) = lattice(filter.germ l β) := sorry

But lattice_of_linear_order seems to be a different sort of beast to lattice and linear_order in that it doesn't map types to types.

Having stared at this for several hours, I'm now hopelessly confused about everything.

Hoping someone can shed some light?

Thanks.

Christopher

[Anne Baanen]

Do I understand correctly that your question is more "how do I phrase the type of test" than "what do I fill in for sorry"?

[Anne Baanen]

First of all, from docs#filter.germ.linear_order it looks like l has to be an ultrafilter.

[Anne Baanen]

This typechecks for me:

import order.filter.germ
import order.lattice
import data.real.hyperreal

universes u v

lemma test {α : Type u} {β : Type v} (l : ultrafilter α) [linear_order β] :
  @lattice_of_linear_order (filter.germ ↑l β) (filter.germ.linear_order) = filter.germ.lattice :=
sorry

[Anne Baanen]

Here's my thought process. We want to state that the two different constructions give rise to the same structure, so we look up what the constructions are called. The first one "a linear order on the germ, which in turn induces a lattice structure on the germ" is called docs#lattice_of_linear_order, and " a lattice structure on β, which induces a lattice structure on the germ" is called docs#filter.germ.lattice. So let's write that out:

import order.filter.germ
import order.lattice
import data.real.hyperreal

universes u v

lemma test {α : Type u} {β : Type v} (l : ultrafilter α) [linear_order β] :
  lattice_of_linear_order = filter.germ.lattice := sorry
-- Error: don't know how to synthesize placeholder ⊢ Type ?

The error means we need to give hints to the elaborator, in order to figure out what type we're actually trying to instantiate the lattice structure on.

The first thing I try is to write out the expected type with a type ascription:

import order.filter.germ
import order.lattice
import data.real.hyperreal

universes u v

lemma test {α : Type u} {β : Type v} (l : ultrafilter α) [linear_order β] :
  (lattice_of_linear_order : lattice (filter.germ ↑l β)) = filter.germ.lattice := sorry
-- Error: don't know how to synthesize placeholder ⊢ Type ?

Seems like this isn't enough, probably because Lean doesn't quite know how to get back the β from filter.germ l β.

Instead of a type ascription, turning the implicit parameters explicit with @ and supplying the correct arguments works, as shown in the above code.

[Eric Wieser]

I think docs#lattice_of_linear_order is dangerous as it constructs new data that forms nondefeq typeclass diamonds

[Eric Wieser]

This same instance just came up in @Yakov Pechersky's thread elsewhere

[Anne Baanen]

Now for filling the sorry: I know that lattices on a type α are uniquely defined by their order, so this should be either available via tactic#ext, or at least available as a theorem named something like docs#lattice.ext. Turns out the former doesn't work, but the latter does, so we need to show ∀ (x y : filter.germ ↑l β), x ≤ y ↔ x ≤ y. (Where the ≤ on the left comes from lattice_of_linear_order and the ≤ on the right comes from filter.germ.lattice.) Checking the sources, both src#filter.germ.linear_order and src#filter.germ.lattice have the same definition of ≤ coming from docs#filter.germ.partial_order, so the two orders are the same by definition:

import order.filter.germ
import order.lattice
import data.real.hyperreal

universes u v

lemma test {α : Type u} {β : Type v} (l : ultrafilter α) [linear_order β] :
  (@lattice_of_linear_order (filter.germ ↑l β) filter.germ.linear_order) = filter.germ.lattice :=
lattice.ext (λ x y, iff.rfl)

[Eric Wieser]

lean#609 fixed this diamond, we just need to wait for a lean release.

[Christopher Hoskin]

@Anne Baanen - thank you very much for the quick response and explaining your working. It appears to solve the problem I was having.

@Eric Wieser - thank you for letting me know that a fix to lean is coming.