compLeft — Mathlib

English

compLeft defines a functorial operation: given f: ContinuousMonoidHom A B, it sends any g: ContinuousMonoidHom B E to g ∘ f.

Русский

compLeft задаёт функторную операцию: для данного f: ContinuousMonoidHom A B функция g ↦ g ∘ f.

LaTeX

$$$\mathrm{compLeft} (f): \mathrm{ContinuousMonoidHom} B E \to \mathrm{ContinuousMonoidHom} A E \quad (g \mapsto g \circ f).$$$

Lean4

/-- `ContinuousMonoidHom _ f` is a functor. -/
@[to_additive /-- `ContinuousAddMonoidHom _ f` is a functor. -/
    ]
def compLeft (f : ContinuousMonoidHom A B) : ContinuousMonoidHom (ContinuousMonoidHom B E) (ContinuousMonoidHom A E)
    where
  toFun g := g.comp f
  map_one' := rfl
  map_mul' _g _h := rfl
  continuous_toFun := f.continuous_comp_left

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