dual — Mathlib

English

There is a natural equivalence between BotHom α β and TopHom αᵒᵈ βᵒᵈ.

Русский

Существует естественное эквивалентное соответствие между BotHom α β и TopHom αᵒᵈ βᵒᵈ.

LaTeX

$$$\mathrm{BotHom}(\alpha,\beta) \simeq \mathrm{TopHom}(\alpha^{\mathrm{op}},\beta^{\mathrm{op}})$$$

Lean4

/-- Reinterpret a bot homomorphism as a top homomorphism between the dual lattices. -/
@[simps]
protected def dual : BotHom α β ≃ TopHom αᵒᵈ βᵒᵈ
    where
  toFun f := ⟨f, f.map_bot'⟩
  invFun f := ⟨f, f.map_top'⟩

Похожие утверждения