English
For a continuous map f and a suitable base ring R, comapₐ provides an AlgHom from LocallyConstant Y Z to LocallyConstant X Z, extending comapRingHom compatibly with algebra structures.
Русский
Для непрерывного отображения f и подходящей основы кольца R comapₐ задаёт алгеброгомоморфизм LocallyConstant(Y,Z) → LocallyConstant(X,Z,).
LaTeX
$$$\operatorname{comap}_{A}(f): \operatorname{LocallyConstant}(Y,Z) \to_{\mathrm{Alg}} \operatorname{LocallyConstant}(X,Z)$$$
Lean4
/-- `LocallyConstant.comap` as an `AlgHom` -/
@[simps!]
def comapₐ (R : Type*) [CommSemiring R] [Semiring Z] [Algebra R Z] (f : C(X, Y)) :
LocallyConstant Y Z →ₐ[R] LocallyConstant X Z
where
toRingHom := comapRingHom f
commutes' _ := rfl
