English
Pulling back a complete lattice along an injective map f: α → β, preserving sup and inf, as well as sSup, sInf, top and bottom, yields a complete lattice structure on α. In other words, if β is a complete lattice and f is an injection with the listed preservation properties, then α inherits a complete lattice structure via f.
Русский
Вытягивание полной решетки вдоль инъекции f: α → β, сохраняющей объединение и пересечение, а также верх и низ, даёт на α структуру полной решетки.
LaTeX
$$$ [Top\, α] [Bot\, α] [SupSet\, α] [InfSet\, α] \,(f: α \to β) \text{ инъекция},\ f(a \vee b) = f(a) \vee f(b),\ f(a \wedge b) = f(a) \wedge f(b),\ f(\top)=\top,\ f(\bot)=\bot \Rightarrow \CompleteLattice\, α.$$$
Lean4
/-- Pullback a `CompleteLattice` along an injection. -/
protected abbrev completeLattice [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [CompleteLattice β] (f : α → β)
(hf : Function.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 ⊥ = ⊥) : CompleteLattice α where
-- we cannot use BoundedOrder.lift here as the `LE` instance doesn't exist yet
__ := hf.lattice f map_sup map_inf
le_sSup _ a h := (le_iSup₂ a h).trans (map_sSup _).ge
sSup_le _ _ h := (map_sSup _).trans_le <| iSup₂_le h
sInf_le _ a h := (map_sInf _).trans_le <| iInf₂_le a h
le_sInf _ _ h := (le_iInf₂ h).trans (map_sInf _).ge
top := ⊤
le_top _ := (@le_top β _ _ _).trans map_top.ge
bot := ⊥
bot_le _ := map_bot.le.trans bot_le
