## Stream: maths

### Topic: Constructing a complete lattice

#### Heather Macbeth (Oct 31 2020 at 20:57):

Can someone explain this docstring to me?
https://github.com/leanprover-community/mathlib/blob/be161d119ac3ee06db86b7429201e4ea281e13f2/src/order/complete_lattice.lean#L71

/-- Create a complete_lattice from a partial_order and Inf function
that returns the greatest lower bound of a set. Usually this constructor provides
poor definitional equalities, so it should be used with
.. complete_lattice_of_Inf α _. -/
def complete_lattice_of_Inf (α : Type*) [H1 : partial_order α]
[H2 : has_Inf α] (is_glb_Inf : ∀ s : set α, is_glb s (Inf s)) :
complete_lattice α :=


Context: I want to make a complete lattice. There's already a partial order structure, and I can easily write down what the has_Sup and has_Inf instances are. Will it cause definitional problems if I simply pick one of these, say the has_Inf, and then use complete_lattice_of_Inf to make the complete lattice structure?

#### Mario Carneiro (Oct 31 2020 at 20:58):

It means that the has_Sup instance will not be the one you would otherwise have written down

#### Mario Carneiro (Oct 31 2020 at 20:58):

as well as sup and inf and top and bot

#### Mario Carneiro (Oct 31 2020 at 20:59):

However, there is complete_lattice.copy that you can use to edit these fields after constructing most of the structure using complete_lattice_of_Inf

#### Heather Macbeth (Oct 31 2020 at 21:00):

Is it bad to take (eg) the inf that comes from this definition, which is inf := λ a b, Inf {a, b}? Isn't that the same as what I would write down by hand?

#### Mario Carneiro (Oct 31 2020 at 21:01):

It seems unlikely that this is what you would write down in any concrete instance unless you had nothing other than Inf to work with

#### Mario Carneiro (Oct 31 2020 at 21:01):

for instance the inf for set is \cap which is not the same as \bigcap {x, y}

#### Mario Carneiro (Oct 31 2020 at 21:02):

I mean if you don't have any particular reason to care what the values are it's fine to just let it be

#### Mario Carneiro (Oct 31 2020 at 21:03):

but if you ever unfold it and end up with something weird you might consider changing the definition to something more sensible

OK, thanks!

#### Heather Macbeth (Oct 31 2020 at 21:04):

What does "it should be used with .. complete_lattice_of_Inf α _." mean, in particular? (From the docstring I quoted above.)

#### Mario Carneiro (Oct 31 2020 at 21:06):

It's suggesting that you write

instance : complete_lattice my_T :=
{ inf := better_inf,
sup := better_sup,
-- don't care to fix Sup, bot, top
..complete_lattice_of_Inf my_T _ }


which is equivalent to my suggestion of using complete_lattice.copy better_inf <proof> Sup rfl (complete_lattice_of_Inf my_T _)

#### Mario Carneiro (Oct 31 2020 at 21:08):

to take a random example, src#subfield.complete_lattice

#### Mario Carneiro (Oct 31 2020 at 21:08):

notice that top and inf are overridden but bot and sup are not because there isn't any much better expression for the sup of subfields

#### Mario Carneiro (Oct 31 2020 at 21:09):

but it's definitely nice to have the inf of subfields be defeq to the binary intersection

#### Mario Carneiro (Oct 31 2020 at 21:10):

so that you can use <hK, hL> to construct and destruct proofs of x \in K \inf L

#### Heather Macbeth (Oct 31 2020 at 21:11):

I see! So when you do it this way, it is overwriting selected fields. Does it require some kind of compatibility proof of the old fields with the new fields? Eg, do I need to overwrite le_inf too?

#### Mario Carneiro (Oct 31 2020 at 21:12):

You do if the new expression is not defeq to the old one (which is usually the case because otherwise there isn't much need to override)

#### Mario Carneiro (Oct 31 2020 at 21:13):

complete_lattice.copy requires you prove the new field is equal to the old one, while using {inf := new_inf, ..} requires proving the new inf also satisfies the inf axioms

#### Heather Macbeth (Oct 31 2020 at 21:15):

I see. Thanks. I think for my WIP code I'll do it the lazy way, and change it field by field if I find myself using them. When I PR I'll do it the right way ....

#### Bryan Gin-ge Chen (Oct 31 2020 at 21:53):

I agree that this docstring is obscure. It'd be great if we added some of the info from the conversation above to it.

#4859

#### Aaron Anderson (Nov 01 2020 at 02:41):

(deleted)

Last updated: May 09 2021 at 10:11 UTC