English
Composition on the left by a continuous algebra homomorphism g: A →ₐ[R] A2 induces an AlgHom C(α,A) → C(α,A2) by f ↦ g ∘ f.
Русский
Слева по отношению к непрерывному гомоморфизму алгебр g: A →ₐ[R] A2 индуцируется гомоморфизм AlgHom: C(α,A) → C(α,A2) заданный f ↦ g ∘ f.
LaTeX
$$$\\text{compLeftContinuous}(g,hg):\\ C(α,A) \\to_{R} C(α,A_2), \\quad f \\mapsto g\\circ f.$$$
Lean4
/-- Composition on the left by a (continuous) homomorphism of topological `R`-algebras, as an
`AlgHom`. Similar to `AlgHom.compLeft`. -/
@[simps!]
protected def compLeftContinuous {α : Type*} [TopologicalSpace α] (g : A →ₐ[R] A₂) (hg : Continuous g) :
C(α, A) →ₐ[R] C(α, A₂) :=
{ g.toRingHom.compLeftContinuous α hg with commutes' := fun _ => ContinuousMap.ext fun _ => g.commutes' _ }
