Complete lattice homomorphisms between powersets #
Mathlib packages the preimage map of a function f : α → β as a complete lattice homomorphism
CompleteLatticeHom.setPreimage f : CompleteLatticeHom (Set β) (Set α). This file proves that
every complete lattice homomorphism Set β → Set α arises this way from exactly one function.
Such a homomorphism sends each point a : α into the image of exactly one singleton {b}, and
the function is a ↦ b.
Main results #
CompleteLatticeHom.existsUnique_mem_map_singleton: each point lies in the image of exactly one singleton.CompleteLatticeHom.setPreimage_surjective,CompleteLatticeHom.setPreimage_injective: every complete lattice homomorphism between powersets is the preimage map of a unique function.
theorem
CompleteLatticeHom.existsUnique_mem_map_singleton
{α : Type u_1}
{β : Type u_2}
(φ : CompleteLatticeHom (Set β) (Set α))
(a : α)
:
∃! b : β, a ∈ φ {b}
A complete lattice homomorphism φ : Set β → Set α places each point of α in the image of
exactly one singleton.
theorem
CompleteLatticeHom.setPreimage_surjective
{α : Type u_1}
{β : Type u_2}
:
Function.Surjective setPreimage
Every complete lattice homomorphism Set β → Set α is the preimage map of a function.
theorem
CompleteLatticeHom.setPreimage_injective
{α : Type u_1}
{β : Type u_2}
:
Function.Injective setPreimage
Distinct functions have distinct preimage maps.