# Zulip Chat Archive

## 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

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

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.

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

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

(deleted)

Last updated: May 09 2021 at 10:11 UTC