comapRingHom — Mathlib

English

For a continuous map f, comapRingHom f is a RingHom from LocallyConstant Y Z to LocallyConstant X Z, obtained by precomposition with f.

Русский

Для непрерывного отображения f, comapRingHom f — это кольцевой гомоморфизм из LocallyConstant(Y,Z) в LocallyConstant(X,Z), получаемый через композицию с f.

LaTeX

$$$\operatorname{comapRingHom}(f): \operatorname{LocallyConstant}(Y,Z) \to^+_* \operatorname{LocallyConstant}(X,Z)$$$

Lean4

/-- `LocallyConstant.comap` as a `RingHom`. -/
@[simps!]
def comapRingHom [Semiring Z] (f : C(X, Y)) : LocallyConstant Y Z →+* LocallyConstant X Z
    where
  toMonoidHom := comapMonoidHom f
  __ := (comapAddMonoidHom f)

Похожие утверждения