Anti-additive and anti-multiplicative maps

This file defines anti-additive maps, which send joins to meets, and anti-multiplicative maps, which send meets to joins. They are the join- and meet-preserving maps into the order dual, so both are antitone. Zwarts grades negative expressions by such properties: no one is anti-additive, and not, which also commutes with complementation, is antimorphic. Over Boolean algebras the antimorphic maps are exactly the maps that are both anti-additive and anti-multiplicative and exchange ⊥ with ⊤.

Main definitions

• IsAntiAdditive: f (p ⊔ q) = f p ⊓ f q.
• IsAntiMultiplicative: f (p ⊓ q) = f p ⊔ f q.

Main statements

• IsAntiAdditive.comp_map_sup, IsAntiAdditive.map_inf_comp, isAntiAdditive_iInf: closure under composition with join- and meet-preserving maps and under pointwise infima.
• isAntiAdditive_compl: complementation in a Heyting algebra is anti-additive.
• IsAntiAdditive.map_compl_iff: an anti-additive map between Boolean algebras commutes with complementation iff it is anti-multiplicative and exchanges ⊥ with ⊤.

Implementation notes

Zwarts and Icard state the definitions for maps between Boolean algebras; only the join and the meet are needed. Anti-multiplicativity and its lemmas are generated from anti-additivity by to_dual.

References

• [Zwa98]
• [Ica12]

def IsAntiAdditive {α : Type u_1} {β : Type u_2} [Max α] [Min β] (f : α → β) : Prop

A map is anti-additive if it sends joins to meets ([Zwa98] (107)).

Equations

• IsAntiAdditive f = ∀ (p q : α), f (p ⊔ q) = f p ⊓ f q

def IsAntiMultiplicative {α : Type u_1} {β : Type u_2} [Min α] [Max β] (f : α → β) : Prop

A map is anti-multiplicative if it sends meets to joins ([Ica12] Definition 1.7).

Equations

• IsAntiMultiplicative f = ∀ (p q : α), f (p ⊓ q) = f p ⊔ f q

theorem IsAntiAdditive.antitone {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeInf β] {f : α → β} (h : IsAntiAdditive f) : Antitone f

theorem IsAntiMultiplicative.antitone {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeSup β] {f : α → β} (h : IsAntiMultiplicative f) : Antitone f

Closure

theorem IsAntiAdditive.comp_map_sup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Max α] [Min β] [Max γ] {f : α → β} {g : γ → α} (hf : IsAntiAdditive f) (hg : ∀ (a b : γ), g (a ⊔ b) = g a ⊔ g b) : IsAntiAdditive (f ∘ g)

theorem IsAntiMultiplicative.comp_map_inf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Min α] [Max β] [Min γ] {f : α → β} {g : γ → α} (hf : IsAntiMultiplicative f) (hg : ∀ (a b : γ), g (a ⊓ b) = g a ⊓ g b) : IsAntiMultiplicative (f ∘ g)

theorem IsAntiAdditive.map_inf_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Max α] [Min β] [Min γ] {f : α → β} {g : β → γ} (hf : IsAntiAdditive f) (hg : ∀ (a b : β), g (a ⊓ b) = g a ⊓ g b) : IsAntiAdditive (g ∘ f)

theorem IsAntiMultiplicative.map_sup_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Min α] [Max β] [Max γ] {f : α → β} {g : β → γ} (hf : IsAntiMultiplicative f) (hg : ∀ (a b : β), g (a ⊔ b) = g a ⊔ g b) : IsAntiMultiplicative (g ∘ f)

theorem isAntiAdditive_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Max α] [CompleteLattice β] {f : ι → α → β} (h : ∀ (i : ι), IsAntiAdditive (f i)) : IsAntiAdditive fun (a : α) => ⨅ (i : ι), f i a

Anti-additive maps are closed under pointwise infima, generalizing the binary case of [Ica12] Lemma 1.12.

theorem isAntiMultiplicative_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Min α] [CompleteLattice β] {f : ι → α → β} (h : ∀ (i : ι), IsAntiMultiplicative (f i)) : IsAntiMultiplicative fun (a : α) => ⨆ (i : ι), f i a

Complementation

theorem isAntiAdditive_compl {α : Type u_1} [HeytingAlgebra α] : IsAntiAdditive compl

theorem isAntiMultiplicative_compl {α : Type u_1} [BooleanAlgebra α] : IsAntiMultiplicative compl

theorem IsAntiAdditive.map_compl_iff {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] {f : α → β} (h : IsAntiAdditive f) : (∀ (x : α), f xᶜ = (f x)ᶜ) ↔ f ⊤ = ⊥ ∧ IsAntiMultiplicative f ∧ f ⊥ = ⊤

[Zwa98]'s antimorphic maps (114) are the anti-additive maps that commute with complementation. Between Boolean algebras they are the anti-additive and anti-multiplicative maps that send ⊤ to ⊥ and ⊥ to ⊤, [Ica12]'s completely anti-additive and completely anti-multiplicative maps (Definition 1.7).

Maps on sets

theorem isAntiAdditive_iff_mem {γ : Type u_3} {δ : Type u_4} {f : Set γ → Set δ} : IsAntiAdditive f ↔ ∀ (p q : Set γ) (x : δ), x ∈ f (p ∪ q) ↔ x ∈ f p ∧ x ∈ f q

theorem isAntiAdditive_forall_mem {γ : Type u_3} {δ : Type u_4} (P : γ → δ → Prop) : IsAntiAdditive fun (X : Set γ) (y : δ) => ∀ x ∈ X, P x y