English
There exists a natural multiplicative homomorphism from α into the lattice of filters, sending each a ∈ α to the pure (principal) filter at a. This map preserves multiplication: pure(a b) = pure(a) * pure(b).
Русский
Существует естественный мультипликативный гомоморфизм из α в множество фильтров, отправляющий каждый элемент a ∈ α в чистый (принципиальный) фильтр в точке a. Этот отображение сохраняет умножение: pure(a b) = pure(a) * pure(b).
LaTeX
$$$\\text{pureMulHom}: \\alpha \\to \\text{Filter}(\\alpha) \\text{ is a multiplicative homomorphism with } \\text{toFun}(a) = \\text{pure}(a).$$$
Lean4
/-- `pure` operation as a `MulHom`. -/
@[to_additive /-- The singleton operation as an `AddHom`. -/
]
def pureMulHom : α →ₙ* Filter α where toFun := pure; map_mul' _ _ := pure_mul_pure.symm
