instFaithfulFunctorTensoringRight

English

The functor tensoringRight is faithful: if tensoringRight f equals tensoringRight g, then f = g.

Русский

Функтор tensoringRight верный: если отображения f и g после тензорирования справа совпадают, то f = g.

LaTeX

$$$ (tensoringRight\\, C).Faithful. map\_injective \\{X\\} {Y} f g \\; h \\Rightarrow \\; h$$

Lean4

instance : (tensoringRight C).Faithful where
  map_injective {X} {Y} f g
    h := by
    injections h
    replace h := congr_fun h (𝟙_ C)
    simpa using h

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