English
Composition with a fixed map g: β → γ yields a nonunital algebra homomorphism from C_c(γ, δ) to C_c(β, δ): f ↦ f ∘ g, preserving addition, multiplication, and scalar action.
Русский
Композицией с фиксированным отображением g: β → γ образуется неполное алгебраическое однородное отображение из C_c(γ, δ) в C_c(β, δ): f ↦ f ∘ g, сохраняющее сложение, умножение и скалярное действие.
LaTeX
$$$\Phi(f) = f \circ g : C_c(γ, δ) \to C_c(β, δ)$ is a nonunital algebra homomorphism, i.e.\n\n$\Phi(f+f') = \Phi(f) + \Phi(f'),\n\Phi(0)=0,\n\Phi(f f') = \Phi(f) \Phi(f'),$$$
Lean4
/-- Composition as a non-unital algebra homomorphism. -/
def compNonUnitalAlgHom {R : Type*} [Semiring R] [NonUnitalNonAssocSemiring δ] [IsTopologicalSemiring δ] [Module R δ]
[ContinuousConstSMul R δ] (g : β →co γ) : C_c(γ, δ) →ₙₐ[R] C_c(β, δ)
where
toFun f := f.comp g
map_smul' _ _ := rfl
map_zero' := rfl
map_add' _ _ := rfl
map_mul' _ _ := rfl
