English
Let α be a type equipped with a complete Boolean algebra structure and β a complete Boolean algebra. If f: α → β is injective and preserves all Boolean operations, finite joins/meets, arbitrary suprema/infima, the top and bottom elements, and complements, as well as implication and the difference operation, then α inherits a complete Boolean algebra structure via pullback along f.
Русский
Пусть α – тип, на котором задана полная булева алгебра, и β – полная булева алгебра. Если f: α → β инъективно и сохраняет все булевы операции, произведения и т.п., а также произволенные свершения (sSup, sInf, top, bottom, complement, импликацию и разность), то α получает структуру полной булевой алгебры через вытягивание вдоль f.
LaTeX
$$$$ \exists \mathcal{A} = (α, ⊔, ⊓, ⊤, ⊥, ^c, \Rightarrow, \backslash) \; \text{such that } \mathcal{A} \text{ is a } \mathbf{CompleteBooleanAlgebra}$$
$$ \text{and } f: α \to β \text{ is an injection preserving all }\; \lor, \land, \top, \bot, ^c, \Rightarrow, \setminus, \sSup, \sInf.$$$
Lean4
/-- Pullback a `CompleteBooleanAlgebra` along an injection. -/
protected abbrev completeBooleanAlgebra [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α]
[SDiff α] [CompleteBooleanAlgebra β] (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_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a)
(map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ)
(map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : CompleteBooleanAlgebra α
where
__ := hf.completeLattice f map_sup map_inf map_sSup map_sInf map_top map_bot
__ := hf.booleanAlgebra f map_sup map_inf map_top map_bot map_compl map_sdiff map_himp
