comapMonoidHom — Mathlib

English

For a continuous map f: X → Y, comap f induces a MonoidHom from LocallyConstant Y Z to LocallyConstant X Z by precomposition: (comap f)(g) = g ∘ f.

Русский

Для непрерывного отображения f: X → Y отображение comap f задаёт моноид-гомоморфизм LocallyConstant(Y,Z) → LocallyConstant(X,Z) по композиции слева: (comap f)(g) = g ∘ f.

LaTeX

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

Lean4

/-- `LocallyConstant.comap` as a `MonoidHom`. -/
@[to_additive (attr := simps) /-- `LocallyConstant.comap` as an `AddMonoidHom`. -/
    ]
def comapMonoidHom [MulOneClass Z] (f : C(X, Y)) : LocallyConstant Y Z →* LocallyConstant X Z
    where
  toFun := comap f
  map_one' := rfl
  map_mul' _ _ := rfl

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