Same ordering, Different frame Structure

Stream: new members

[Christian Krause]

Hi,
I'm currently trying to define Sublocales in Lean to prove that the sublocales of a locale X are isomorphic to the nuclei on X.
Therefore, I'm currently trying to follow this definition of a sublocale on nlab:

[L is a frame]
Thus, sublocales of L can be defined as subsets S of L such that S is a locale once we equip it with the order induced from L, and the left adjoint to the inclusion S→L exists and preserves finite meets. [...]
(The inclusion S→L need not preserve joins, so in particular, the lattice structure on S may be different from that of L, only the ordering is the same.)

This is what I have so far:

structure Sublocale (X : Type*) [Order.Frame X] where
  carrier : Set X
  frm : Order.Frame carrier
  l : @InfHom  X ↑carrier _ (frm.toMin)
  gc : @GaloisConnection _ _ _ (frm.toPreorder) l Subtype.val

But this definition has one problem. In Mathlib, there is the Instance Subtype.preorder which gives carrier the same ordering as X. But the carrier also has to be a Frame, which could be different from the Frame on X. I used the frm Field to assert that carrier has to be a Frame. But this is almost certainly wrong, because the Ordering of frm is possibly not the same as the Ordering of X which is supplied by the Subtype.preorder instance.
How can I express in lean, that carrier should be a Frame with the same ordering as X?
(MWE)

[Yaël Dillies]

You should instead assume that carrier is closed under frame operations. See how docs#Subgroup is made

[Eric Wieser]

Probably you want to instead express that carrier is closed under the frame operations?

[Eric Wieser]

Extending docs#Sublattice would presumably be a good start

[Christian Krause]

I looked into docs#CompleteSublattice, but I'm not sure if that's what I want, because the definition says:

(The inclusion S→L need not preserve joins, so in particular, the lattice structure on S may be different from that of L, only the ordering is the same

Or am I not understanding this sentence correctly?

[Christian Krause]

I could probably just use this definition:

Equivalently, sublocales of L can also be described (PP12 §2.1) as subsets S of L that are closed under all meets and for any s∈S and x∈L, we have (x→s)∈S.

which could be implemented in a similar way as docs#Sublattice, but I do want to understand how the first definition would work in lean.

[Yaël Dillies]

Christian K said:

I looked into docs#CompleteSublattice, but I'm not sure if that's what I want, because the definition says:

(The inclusion S→L need not preserve joins, so in particular, the lattice structure on S may be different from that of L, only the ordering is the same

Or am I not understanding this sentence correctly?

Where do you see this sentence? It doesn't appear in this file AFAICT

[Christian Krause]

It is from the definition of sublocales in nlab. (I should have phrased this more clearly earlier ...)

[Christian Krause]

As far as I understand, this is the opposite of what docs#Sublattice does.