lattice homomorphisms

Stream: general

[Simon Hudon]

Is there such a thing as a lattice homomorphism in mathlib?

[Johannes Hölzl]

there is only one for countable suprema: def ord_continuous (f : α → β) := ∀s : set α, f (Sup s) = (⨆i∈s, f i)

[Mario Carneiro]

I think that's arbitrary suprema

[Mario Carneiro]

I should note that a "complete lattice homomorphism" has to preserve suprema and infima. Despite the fact that you can define suprema from infima and vice versa, there are Sup-lattice homs that are not complete lattice homs (see wiki)

[Mario Carneiro]

@Floris van Doorn By the way, that wiki page also mentions something related to our discussion yesterday, on the presumed existence of "free constructions". Apparently the free complete lattice (in the category of complete lattices and complete lattice homs) does not always exist in ZFC, because you need a proper class collection of conditions

[Floris van Doorn]

On free complete lattices: since the meet and the sup operations can have any cardinal as arity, you don't get a universe closed under the free complete lattice operation (probably that is inconsistent). However, with higher inductive types in HoTT you can construct free algebras for infinitary algebraic theories, which are not constructible in ZFC (without large cardinal assumptions), see https://arxiv.org/abs/1705.07088, section 9.

[Mario Carneiro]

I was aware of this result, but when reading it directly I find it is weaker than expected. The paper constructs a HIT F that implies the existence of an uncountable regular cardinal; but ZFC gives scads of uncountable regular cardinals, like aleph_1. They argue that this gives additional power over ZF (which is true, since you can't prove that aleph_1 is regular without choice) but it's not clear to me how this relates to ZFC.