English
Precomposition by a continuous map f: C(α,β) yields an algebra homomorphism C(β,A) →ₐ[R] C(α,A) given by g ↦ g ∘ f.
Русский
Предкомпозиция по непростой карте f: C(α,β) задаёт алгебромоморфизм C(β,A) →ₐ[R] C(α,A), отправляющий g в g ∘ f.
LaTeX
$$$\\mathrm{compRightAlgHom}(f): C(β,A) \\to_{R} C(α,A), \\quad g \\mapsto g \\circ f.$$$
Lean4
/-- Precomposition of functions into a topological semiring by a continuous map is an algebra
homomorphism. -/
@[simps]
def compRightAlgHom {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) : C(β, A) →ₐ[R] C(α, A)
where
toFun g := g.comp f
map_zero' := ext fun _ ↦ rfl
map_add' _ _ := ext fun _ ↦ rfl
map_one' := ext fun _ ↦ rfl
map_mul' _ _ := ext fun _ ↦ rfl
commutes' _ := ext fun _ ↦ rfl
