English
Let f: α → β be an injective map into a Boolean algebra β, and suppose f preserves the Boolean operations: join, meet, top, bottom, complement, set difference, and implication. Then α can be equipped with a Boolean algebra structure transported along f, and f becomes a Boolean algebra embedding.
Русский
Пусть f: α → β — инъекция в булеву алгебру β, и пусть она сохраняет булевы операции: объединение, пересечение, верхний элемент, нижний элемент, комплемент, разность и импликацию. Тогда α наделяется структурой булевой алгебры, перенесённой через f, и f становится вложением булевых алгебр.
LaTeX
$$$\exists \mathcal{A} \text{ on } \alpha\,\Big(\text{BooleanAlgebra}(\alpha, \mathcal{A}) \wedge \forall a,b\in\alpha:\ f(a\lor_{\mathcal{A}} b)=f(a)\lor_{\beta} f(b) \wedge f(a\land_{\mathcal{A}} b)=f(a)\land_{\beta} f(b) \wedge f(\top_{\mathcal{A}})=\top_{\beta} \wedge f(\bot_{\mathcal{A}})=\bot_{\beta} \wedge \forall a:\ f(a^{c_{\mathcal{A}}})=(f(a))^{c_{\beta}} \wedge \forall a,b:\ f(a\setminus_{\mathcal{A}} b)=f(a)\setminus_{\beta} f(b) \wedge \forall a,b:\ f(a\Rightarrow_{\mathcal{A}} b)=f(a)\Rightarrow_{\beta} f(b) \Big).$$$
Lean4
/-- Pullback a `BooleanAlgebra` along an injection. -/
protected abbrev booleanAlgebra [Max α] [Min α] [Top α] [Bot α] [HasCompl α] [SDiff α] [HImp α] [BooleanAlgebra β]
(f : α → β) (hf : Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
(map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b)
(map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) : BooleanAlgebra α
where
__ := hf.generalizedBooleanAlgebra f map_sup map_inf map_bot map_sdiff
compl := compl
himp := himp
top := ⊤
le_top _ := (@le_top β _ _ _).trans map_top.ge
bot_le _ := map_bot.le.trans bot_le
inf_compl_le_bot a := ((map_inf _ _).trans <| by rw [map_compl, inf_compl_eq_bot, map_bot]).le
top_le_sup_compl a := ((map_sup _ _).trans <| by rw [map_compl, sup_compl_eq_top, map_top]).ge
sdiff_eq a b := hf <| (map_sdiff _ _).trans <| sdiff_eq.trans <| by rw [map_inf, map_compl]
himp_eq a b := hf <| (map_himp _ _).trans <| himp_eq.trans <| by rw [map_sup, map_compl]
