English
There is a construction turning a bounded lattice homomorphism between Boolean algebras into a ring homomorphism between their AsBoolRing versions; it is given by toFun = toBoolAlg ∘ f ∘ ofBoolAlg, with map_sup', map_inf', map_top', map_bot'.
Русский
Существуют преобразование гомоморфизма ограниченной решётки между булевыми алгебрами в гомоморфизм кольца между их версиями AsBoolRing; задаётся через toFun = toBoolAlg ∘ f ∘ ofBoolAlg и сохраняет верх, низ, ∨ и ∧.
LaTeX
$$$\widehat{f} := \operatorname{toBoolAlg} \circ f \circ \operatorname{ofBoolAlg},\quad \widehat{f}(a \lor b) = \widehat{f}(a) \lor \widehat{f}(b),\; \widehat{f}(0)=0,\; \widehat{f}(1)=1,\; \widehat{f}(a \land b)=\widehat{f}(a) \land \widehat{f}(b).$$$
Lean4
/-- Turn a bounded lattice homomorphism from Boolean algebras `α` to `β` into a ring homomorphism
from `α` to `β` considered as Boolean rings. -/
@[simps]
protected def asBoolRing (f : BoundedLatticeHom α β) : AsBoolRing α →+* AsBoolRing β
where
toFun := toBoolRing ∘ f ∘ ofBoolRing
map_zero' := f.map_bot'
map_one' := f.map_top'
map_add' := map_symmDiff' f
map_mul' := f.map_inf'
