Involutive complements

This file defines involutive complements. An involutive complement on an ordered type is a complement ᶜ that is involutive, aᶜᶜ = a, and reverses the order. It is Birkhoff's "involution", and a lattice with one is Kalman's "lattice with involution". The De Morgan laws follow from these two properties alone, without any complementation law such as a ⊓ aᶜ = ⊥.

The involution is the common base of two branches between mathlib's lattices and BooleanAlgebra. Adding distributivity gives De Morgan and Kleene algebras (Core/Order/DeMorganAlgebra/); adding non-contradiction gives ortholattices (Core/Order/Ortholattice.lean). A Boolean algebra lies on both.

Main definitions

• InvolutiveCompl: the data class of an involutive, order-reversing complement, extending the notation class Compl and parameterized by the order, as mathlib's InvolutiveNeg extends Neg and OrderTop takes [LE α].
• InvolutiveCompl.complOrderIso: the involution as an order isomorphism α ≃o αᵒᵈ.

Main results

• InvolutiveCompl.compl_sup, InvolutiveCompl.compl_inf: the De Morgan laws.
• InvolutiveCompl.le_compl_comm: a ≤ bᶜ ↔ b ≤ aᶜ.
• BooleanAlgebra.toInvolutiveCompl: a Boolean algebra's complement is involutive.

Implementation notes

The lemmas are protected in the InvolutiveCompl namespace because the root names (compl_compl, compl_sup, ...) belong to mathlib's Boolean and Heyting API. Upstream, the Boolean ones would be generalized to InvolutiveCompl, and complOrderIso would generalize mathlib's OrderIso.compl. There is no OrderDual instance: its complement would have to agree with the one mathlib's OrderDual.instBiheytingAlgebra gives the dual of a Boolean algebra, the one place a genuine Compl diamond can arise.

References

• [Kal58]

class InvolutiveCompl (α : Type u_3) [LE α] extends Compl α : Type u_3

An involutive complement on an ordered type is a complement with aᶜᶜ = a that reverses the order ([Kal58]'s involution, Birkhoff's dual automorphism of period two). Compl is notation, so no complementation law is implied: a ⊓ aᶜ = ⊥ may fail.

• compl : α → α
• compl_compl (a : α) : aᶜᶜ = a

  The complement is involutive, aᶜᶜ = a.

• compl_le_compl {a b : α} : a ≤ b → bᶜ ≤ aᶜ

  The complement reverses the order.

theorem InvolutiveCompl.compl_involutive {α : Type u_1} [LE α] [InvolutiveCompl α] : Function.Involutive compl

theorem InvolutiveCompl.compl_injective {α : Type u_1} [LE α] [InvolutiveCompl α] : Function.Injective compl

theorem InvolutiveCompl.compl_surjective {α : Type u_1} [LE α] [InvolutiveCompl α] : Function.Surjective compl

@[simp]

theorem InvolutiveCompl.compl_inj_iff {α : Type u_1} [LE α] [InvolutiveCompl α] {a b : α} : aᶜ = bᶜ ↔ a = b

theorem InvolutiveCompl.compl_eq_iff_eq_compl {α : Type u_1} [LE α] [InvolutiveCompl α] {a b : α} : aᶜ = b ↔ a = bᶜ

@[simp]

theorem InvolutiveCompl.compl_le_compl_iff_le {α : Type u_1} [LE α] [InvolutiveCompl α] {a b : α} : aᶜ ≤ bᶜ ↔ b ≤ a

theorem InvolutiveCompl.le_compl_comm {α : Type u_1} [LE α] [InvolutiveCompl α] {a b : α} : a ≤ bᶜ ↔ b ≤ aᶜ

Orthogonality is symmetric, a ≤ bᶜ ↔ b ≤ aᶜ.

def InvolutiveCompl.complOrderIso (α : Type u_1) [LE α] [InvolutiveCompl α] : α ≃o αᵒᵈ

The involution bundled as an order isomorphism onto the order dual. Upstream this is mathlib's OrderIso.compl, generalized from BooleanAlgebra to InvolutiveCompl.

Equations

• InvolutiveCompl.complOrderIso α = { toFun := fun (a : α) => OrderDual.toDual aᶜ, invFun := fun (a : αᵒᵈ) => (OrderDual.ofDual a)ᶜ, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem InvolutiveCompl.compl_anti {α : Type u_1} [Preorder α] [InvolutiveCompl α] : Antitone compl

The complement is antitone (bundled form of the compl_le_compl field).

The De Morgan laws and the exchange of the bounds are complOrderIso preserving the lattice operations: they follow from involution and antitonicity alone.

@[simp]

theorem InvolutiveCompl.compl_sup {α : Type u_1} [Lattice α] [InvolutiveCompl α] (a b : α) : (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

@[simp]

theorem InvolutiveCompl.compl_inf {α : Type u_1} [Lattice α] [InvolutiveCompl α] (a b : α) : (a ⊓ b)ᶜ = aᶜ ⊔ bᶜ

@[simp]

theorem InvolutiveCompl.compl_bot {α : Type u_1} [PartialOrder α] [BoundedOrder α] [InvolutiveCompl α] : ⊥ᶜ = ⊤

@[simp]

theorem InvolutiveCompl.compl_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] [InvolutiveCompl α] : ⊤ᶜ = ⊥

@[instance_reducible, instance 100]

instance BooleanAlgebra.toInvolutiveCompl {α : Type u_1} [BooleanAlgebra α] : InvolutiveCompl α

A Boolean algebra's complement is involutive and antitone.

Equations

• BooleanAlgebra.toInvolutiveCompl = { toCompl := inst✝.toCompl, compl_compl := ⋯, compl_le_compl := ⋯ }

Products and functions

@[instance_reducible]

instance instInvolutiveComplProd {α : Type u_1} {β : Type u_2} [LE α] [LE β] [InvolutiveCompl α] [InvolutiveCompl β] : InvolutiveCompl (α × β)

Equations

• instInvolutiveComplProd = { toCompl := Prod.instCompl, compl_compl := ⋯, compl_le_compl := ⋯ }

@[instance_reducible]

instance instInvolutiveComplForall {ι : Type u_3} {π : ι → Type u_4} [(i : ι) → LE (π i)] [(i : ι) → InvolutiveCompl (π i)] : InvolutiveCompl ((i : ι) → π i)

Equations

• instInvolutiveComplForall = { toCompl := Pi.instCompl, compl_compl := ⋯, compl_le_compl := ⋯ }