Lifting order structure

Stream: Is there code for X?

[Yaël Dillies]

Am I right in thinking that we can lift complete_lattice along an injective map provided that the image of the Sup is the Sup of the image?

[Yaël Dillies]

It's like docs#function.injective.lattive but for complete_lattice. And if so, are we missing it?

[Kevin Buzzard]

The inclusion from subgroups of a group to subsets of a group satisfies inf of image equals image of inf but not sups. Now op everything and you get an example where sup isn't preserved. But this isn't exactly your question

[Yaël Dillies]

Ah sorry, I mean that both Sup and Inf are preserved.

[Yaël Dillies]

I'm defining up_set and down_set and there the coercion to set preserves Sup and Inf by definition. So it would be very handy to have such a lifting instance.

[Kevin Buzzard]

If Sup and Inf and le are preserved then I should think all the axioms for a complete lattice follow easily

[Yaël Dillies]

Yeah, but we can also have the general lifting instance to make it easier.