isoSum_hom_app_inl — Mathlib

English

The left component of isoSum is the identity on the left summand image: (isoSum F).hom.app (inl a) = id_{F(inl a)}.

Русский

Левый компонент изоморфизма суммы равен тождественному отображению на изображении слева: (isoSum F).hom.app (inl a) = id_{F(inl a)}.

LaTeX

$$$ (\\mathrm{isoSum}\\ F).\\mathrm{hom}.\\mathrm{app}(\\mathrm{inl}\\ a) = \\mathrm{Id}_{F(\\mathrm{inl}\\ a)} $$$

Lean4

@[simp]
theorem isoSum_hom_app_inl : (isoSum F).hom.app (inl a) = 𝟙 (F.obj (inl a)) :=
  rfl

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