Involution lattices and Heyting algebras

Stream: maths

[Yaël Dillies]

@Peter Nelson, I did end up finding lemmas that are true in both involution lattices and Heyting algebras, namely docs#compl_top and docs#compl_bot.

[Yaël Dillies]

Here is what I came up with: branch#involution_lattice

[Peter Nelson]

Nice. Is there a reason to have it as involution-lattice rather than involution-order? I can't think of any examples that separate the two, but nearly none of the material cares about lattices.

My latest commit removes the word 'pseudocomplement' from a docstring; it appears in the literature with another meaning. It is honestly hard to find any '(prefix-)complement words that aren't defined at least once somewhere. The order theory literature is a real labyrinth of definitions...

[Peter Nelson]

By the way, I did think of another weird instance of this - given an i-lattice on α, the operation on lower_set α that exchanges the downsets of antichains s and compl '' s gives an involution on lower_set α.

[Yaël Dillies]

Hmm, interesting.

[Yaël Dillies]

By the way, I don't believe in the example you gave in the module docstring. If a ∈ W ⊓ {a ∈ V | ∀ w ∈ W, wᵀa = 0}, then aᵀa = 0, so a = 0.

[Peter Nelson]

That last conclusion doesn't hold in nonzero characteristic

[Yaël Dillies]

Ah, right.