hom_whiskerRight — Mathlib

English

The right whisker of a morphism corresponds to tensoring with identity on the right: (f ▷ N).hom = Algebra.TensorProduct.map f.hom id.

Русский

Правое подгружение морфизма соответствует тензорированию справа тождественным: (f ▷ N).hom = Algebra.TensorProduct.map f.hom (id).

LaTeX

$$$$ (f \triangleright N).\hom = \operatorname{Algebra.TensorProduct.map}(f.\hom, \mathrm{id}_{R}). $$$$

Lean4

theorem hom_whiskerRight {L M : AlgCat.{u} R} (f : L ⟶ M) (N : AlgCat.{u} R) :
    (f ▷ N).hom = Algebra.TensorProduct.map f.hom (.id _ _) :=
  rfl

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