Additive, multiplicative, and anti- function classes

Unbundled equational classes for maps between (semi)lattices: IsAdditive (f (p ⊔ q) = f p ⊔ f q), IsMultiplicative (meets to meets), IsAntiAdditive (joins to meets), IsAntiMultiplicative (meets to joins), and IsAntiMorphic (both anti-properties). Each class implies monotonicity or antitonicity; the IsCompletely* variants add the unit conditions (f ⊤ = ⊤, f ⊤ = ⊥, …). The anti-classes are the plain classes read into the order dual, so an additive function bundles as a SupHom and anti-additivity is additivity composed with toDual.

Main declarations

• IsAdditive, IsMultiplicative, IsAntiAdditive, IsAntiMultiplicative, IsAntiMorphic — the classes, with Monotone/Antitone consequence lemmas.
• IsCompletely* — the unit-condition refinements.
• IsAdditive.toSupHom, isAntiAdditive_iff_isAdditive_toDual — the bundled-hom and duality bridges.
• isAntiAdditive_iff_mem, isAntiAdditive_iff_gq — pointwise forms at the Set- and Prop-valued instances.
• GaloisConnection.isAdditive and friends — adjoints land in the classes; exists_galoisConnection_iff_forall_sSup — the poset adjoint functor theorem ([UPSTREAM] candidate), with the finite corollary isAdditive_and_bot_iff_exists_galoisConnection.

The property family

def IsAdditive {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (f : α → β) : Prop

Additive: f (p ⊔ q) = f p ⊔ f q.

Equations

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

def IsMultiplicative {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (f : α → β) : Prop

Multiplicative: f (p ⊓ q) = f p ⊓ f q.

Equations

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

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

Anti-additive: f (p ⊔ q) = f p ⊓ f q, polymorphic in domain and codomain.

Equations

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

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

Anti-multiplicative: f (p ⊓ q) = f p ⊔ f q.

Equations

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

def IsAntiMorphic {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : α → β) : Prop

Anti-morphic: anti-additive and anti-multiplicative.

Equations

• IsAntiMorphic f = (IsAntiAdditive f ∧ IsAntiMultiplicative f)

Completely-variants

def IsCompletelyAdditive {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β] (f : α → β) : Prop

Completely additive: additive and f ⊤ = ⊤.

Equations

• IsCompletelyAdditive f = (IsAdditive f ∧ f ⊤ = ⊤)

def IsCompletelyMultiplicative {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β] (f : α → β) : Prop

Completely multiplicative: multiplicative and f ⊥ = ⊥.

Equations

• IsCompletelyMultiplicative f = (IsMultiplicative f ∧ f ⊥ = ⊥)

def IsCompletelyAntiAdditive {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [OrderTop α] [SemilatticeInf β] [OrderBot β] (f : α → β) : Prop

Completely anti-additive: anti-additive and f ⊤ = ⊥.

Equations

• IsCompletelyAntiAdditive f = (IsAntiAdditive f ∧ f ⊤ = ⊥)

def IsCompletelyAntiMultiplicative {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [OrderBot α] [SemilatticeSup β] [OrderTop β] (f : α → β) : Prop

Completely anti-multiplicative: anti-multiplicative and f ⊥ = ⊤.

Equations

• IsCompletelyAntiMultiplicative f = (IsAntiMultiplicative f ∧ f ⊥ = ⊤)

Monotonicity consequences

theorem IsAdditive.monotone {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : IsAdditive f) : Monotone f

Additive implies monotone.

theorem IsMultiplicative.monotone {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (h : IsMultiplicative f) : Monotone f

Multiplicative implies monotone.

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

Anti-additive implies antitone.

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

Anti-multiplicative implies antitone.

theorem IsAntiMorphic.antiAdditive {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] {f : α → β} (h : IsAntiMorphic f) : IsAntiAdditive f

Anti-morphic implies anti-additive.

theorem IsAntiMorphic.antiMultiplicative {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] {f : α → β} (h : IsAntiMorphic f) : IsAntiMultiplicative f

Anti-morphic implies anti-multiplicative.

theorem IsAntiMorphic.antitone {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] {f : α → β} (h : IsAntiMorphic f) : Antitone f

Anti-morphic implies antitone.

mathlib hom-hierarchy bridges

The function classes are the unbundled predicates for mathlib's bundled lattice homs: an additive function is a SupHom, a multiplicative one an InfHom. The anti-classes are the same notions read into the order dual — anti-additivity is additivity composed with toDual (De Morgan duality), so the .antitone consequences are the duals of the .monotone ones.

def IsAdditive.toSupHom {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : IsAdditive f) : SupHom α β

An additive function bundles as a SupHom.

Equations

• h.toSupHom = { toFun := f, map_sup' := h }

def IsMultiplicative.toInfHom {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (h : IsMultiplicative f) : InfHom α β

A multiplicative function bundles as an InfHom.

Equations

• h.toInfHom = { toFun := f, map_inf' := h }

theorem isAntiAdditive_iff_isAdditive_toDual {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeInf β] {f : α → β} : IsAntiAdditive f ↔ IsAdditive (⇑OrderDual.toDual ∘ f)

De Morgan duality: anti-additivity is additivity into the order dual — f sends joins to meets iff toDual ∘ f preserves joins.

Complementation

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

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

theorem isAntiMorphic_compl {α : Type u_1} [BooleanAlgebra α] : IsAntiMorphic compl

theorem antitone_compl {α : Type u_1} [BooleanAlgebra α] : Antitone compl

theorem isCompletelyAntiAdditive_compl {α : Type u_1} [BooleanAlgebra α] : IsCompletelyAntiAdditive compl

theorem isCompletelyAntiMultiplicative_compl {α : Type u_1} [BooleanAlgebra α] : IsCompletelyAntiMultiplicative compl

Pointwise bridges

The equational properties at the Set and GQ instances, in the membership forms consumers destructure.

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

theorem isAntiMultiplicative_iff_mem {γ : Type u_1} {δ : Type u_2} {f : Set γ → Set δ} : IsAntiMultiplicative f ↔ ∀ (p q : Set γ) (x : δ), x ∈ f (p ∩ q) ↔ x ∈ f p ∨ x ∈ f q

theorem isAntiAdditive_iff_gq {γ : Type u_1} {f : Set γ → Prop} : IsAntiAdditive f ↔ ∀ (p q : Set γ), f (p ∪ q) ↔ f p ∧ f q

The Prop-valued instance: anti-additivity is f (p ∪ q) ↔ f p ∧ f q.

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

Any function of the form fun X y => ∀ x ∈ X, P x y is anti-additive in X.

Galois connections

Adjoints land in the function classes: a left adjoint is additive, a right adjoint multiplicative, and the anti-classes are adjoints into the order dual. A single adjunction yields ⊥- (resp. ⊤-) preservation, never the opposite unit, so only bi-adjoints reach the IsCompletely* classes. exists_galoisConnection_iff_forall_sSup is the poset adjoint functor theorem, an [UPSTREAM] candidate: mathlib has GaloisConnection.l_sSup but not the converse.

theorem GaloisConnection.isAdditive {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : IsAdditive l

A left adjoint is additive.

theorem GaloisConnection.isMultiplicative {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] {l : β → α} {u : α → β} (gc : GaloisConnection l u) : IsMultiplicative u

A right adjoint is multiplicative.

theorem GaloisConnection.isAntiAdditive {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeInf β] {f : α → β} {u : βᵒᵈ → α} (gc : GaloisConnection (⇑OrderDual.toDual ∘ f) u) : IsAntiAdditive f

An antitone left adjoint — a left adjoint into the order dual — is anti-additive.

theorem GaloisConnection.isAntiMultiplicative {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeSup β] {f : α → β} {l : βᵒᵈ → α} (gc : GaloisConnection l (⇑OrderDual.toDual ∘ f)) : IsAntiMultiplicative f

An antitone right adjoint — a right adjoint into the order dual — is anti-multiplicative.

theorem isCompletelyAdditive_of_galoisConnection {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β] {f : α → β} {u l : β → α} (gc₁ : GaloisConnection f u) (gc₂ : GaloisConnection l f) : IsCompletelyAdditive f

A map with adjoints on both sides is completely additive: additivity from its left adjunction, f ⊤ = ⊤ from its right one.

theorem isCompletelyMultiplicative_of_galoisConnection {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β] {f : α → β} {u l : β → α} (gc₁ : GaloisConnection f u) (gc₂ : GaloisConnection l f) : IsCompletelyMultiplicative f

A map with adjoints on both sides is completely multiplicative: multiplicativity from its right adjunction, f ⊥ = ⊥ from its left one.

theorem IsCompletelyAdditive.not_isCompletelyAntiAdditive {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [OrderTop α] [Lattice β] [BoundedOrder β] [Nontrivial β] {f : α → β} (h : IsCompletelyAdditive f) (h' : IsCompletelyAntiAdditive f) : False

The morphism and anti-morphism unit conditions collide on a nontrivial codomain.

theorem galoisConnection_of_forall_sSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) : GaloisConnection f fun (b : β) => sSup {a : α | f a ≤ b}

Poset adjoint functor theorem, construction half: a sSup-preserving map between complete lattices is a left adjoint, with right adjoint λ b => sSup {a | f a ≤ b}.

theorem exists_galoisConnection_iff_forall_sSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α → β) : (∃ (u : β → α), GaloisConnection f u) ↔ ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a

Poset adjoint functor theorem: a map between complete lattices is a left adjoint iff it preserves arbitrary suprema.

theorem isAdditive_and_bot_iff_exists_galoisConnection {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Finite α] [SemilatticeSup β] [OrderBot β] (f : α → β) : IsAdditive f ∧ f ⊥ = ⊥ ↔ ∃ (u : β → α), GaloisConnection f u

On a finite lattice, binary additivity plus ⊥-preservation is exactly left-adjointness.