Frames and frame homomorphisms

Stream: maths

[Pieter Cuijpers]

A frame is, usually, defined as an order with finite meets and infinite joins, where finite meets moreover distribute over said infinite joins.

In Mathlib4, however, frames are not defined yet (afaik) but frame homomorphisms are... they are defined over complete lattices though.

Now... it is true that any frame can be considered as a complete lattice (having both infinite meets and infinite joins), because an infinite meet can be defined in terms of the infinite join. So it makes sense to simply consider a frame to be a complete lattice with finite meets distributing over infinite joins.

But... the definition of frame homomorphism only states preservation of finite meet, infinite join, and the top element. It does not guarantee preservation of the distributivity law.

I think therefore that it would be conceptually better at least to introduce frames as well and define frame homomorphisms on those.

Is there a reason why that was not (yet) done?

[Oliver Nash]

Is docs4#Order.Frame not a frame?

[Yaël Dillies]

Yes, Oliver is right. We have the definition of frames in mathlib. I don't see what you mean by "preservation of the distributivity law". The distributivity law is not data, so it cannot be preserved.

[Oliver Nash]

Similar to how a group homomorphism is not required to "preserve associativity".

[Reid Barton]

I think mainly the documentation is suboptimal: rather than
" A frame is a complete lattice such that ..."
it should be more like
"A frame is a poset with arbitrary joins and finite meets such that .... Note that, since it is a theorem that every frame also has arbitrary meets, for technical reasons Frame also extends CompleteLattice."

[Yaël Dillies]

That's not really in the mathlib spirit, but sure.

[Pieter Cuijpers]

Thanks, I must have overlooked that! Sorry.

But still, why define a frame homomorphism between complete lattices, rather than between frames?

The distributivity is perhaps not data, but it is structure - so a structure preserving map should preserve it. (I'm not formally trained as a mathematician though, so I may have misunderstood something.)

[Yaël Dillies]

Can you try stating what preserving distributivity would mean? I think you will see what I was getting at.

[Pieter Cuijpers]

So imo it is not similar to a group homomorphism not preserving associativity. It would be more like defining a group homomorphism on semigroups, simply because a group is a semigroup. That feels wrong.

[Pieter Cuijpers]

Since a complete lattice does not have distributivity, a frame homomorphism doesnt make sense between complete lattices.

[Yaël Dillies]

Well... speaking of that, docs#monoid_hom is the structure representing group homomorphisms, and it's defined on monoids.

[Pieter Cuijpers]

Why?

[Yaël Dillies]

It's not defined on semigroups because we need the existence of 1 to state f 1 = 1.

[Yaël Dillies]

This is because a group homomorphism is just a monoid homomorphism between groups. If it were its own thing, we would have to duplicate many, many definitions and lemmas between monoid_hom and group_hom for no clear benefit.

[Yaël Dillies]

This is also why we have docs#module but not vector_space. Vector spaces, modules and semimodules are all the same thing, the only difference being the background assumption that the scalars form a field, ring, semiring.

[Pieter Cuijpers]

Ah, so it is really about duplication of theorems.

[Pieter Cuijpers]

That does not happen automatically once you've proven that every frame is a complete lattice?

[Pieter Cuijpers]

"automatically" being the difficulty, I suppose

[Pieter Cuijpers]

(newbe in theorem proving)

[Pieter Cuijpers]

Thanks!

[Yaël Dillies]

If you make

def monoid_hom (G H : Type) [monoid G] [monoid H] :=
(to_fun : G → H)
(map_one : to_fun 1 = 1)
(map_mul : ∀ a b, to_fun (a * b) = to_fun a * to_fun b)

def monoid_hom (G H : Type) [group G] [group H] :=
(to_fun : G → H)
(map_one : to_fun 1 = 1)
(map_mul : ∀ a b, to_fun (a * b) = to_fun a * to_fun b)

then monoid_hom G H and group_hom G H are simply not the same type. Lean can't just replace one by the other.

[Yaël Dillies]

You would have to prove by hand that every property you care about transfers across the obvious isomorphism monoid_hom G H ≃ group_hom G H, and then perform that transfer on every single theorem.

[Reid Barton]

The analogy here is somewhat flawed in that "frame homomorphism of complete lattices" is not a concept of the same status as say a homomorphism of monoids.

[Yaël Dillies]

Yeah. I must confess that i don't know of uses of frame homs on non-frame complete lattices, but having the def in the generality of complete lattices doesn't hurt.

[Reid Barton]

Well, it seems to cause some confusion at least...

[Yaël Dillies]

And the confusion was cleared up with Pieter learning one of the fundamental designs of mathlib :smiley:

[Pieter Cuijpers]

True. The confusion is cleared up :smile: thanks a lot! (Even though a twinge of disappointment remains :rolling_eyes:. I guess that's just why research in this field is still usefull. :innocent:)