English
Given a Boolean ring hom f: α →+* β, there is a corresponding bounded lattice hom between AsBoolAlg α and AsBoolAlg β, defined by toFun = toBoolAlg ∘ f ∘ ofBoolAlg, which preserves sup, inf, top, and bottom.
Русский
Пусть f: α →+* β – гомоморфизм кольца Булевых колец. Существует соответствующий гомоморфизм ограниченной решётки между AsBoolAlg α и AsBoolAlg β, задаваемый toBoolAlg ∘ f ∘ ofBoolAlg и сохраняющий верх, низ, сход и пересечение.
LaTeX
$$$\widehat{f} := \operatorname{toBoolAlg} \circ f \circ \operatorname{ofBoolAlg},\quad \widehat{f}(a \vee b) = \widehat{f}(a) \vee \widehat{f}(b),\quad \widehat{f}(0)=0,\ \widehat{f}(1)=1,\ \widehat{f}(a \wedge b)=\widehat{f}(a) \wedge \widehat{f}(b).$$$
Lean4
/-- Turn a ring homomorphism from Boolean rings `α` to `β` into a bounded lattice homomorphism
from `α` to `β` considered as Boolean algebras. -/
@[simps]
protected def asBoolAlg (f : α →+* β) : BoundedLatticeHom (AsBoolAlg α) (AsBoolAlg β)
where
toFun := toBoolAlg ∘ f ∘ ofBoolAlg
map_sup' a
b := by
dsimp
simp_rw [map_add f, map_mul f, toBoolAlg_add_add_mul]
map_inf' := f.map_mul'
map_top' := f.map_one'
map_bot' := f.map_zero'
