whiskerRightIso_refl — Mathlib

English

Left whiskering by the identity on X yields the identitywise left whisker: whiskerRightIso (Iso.refl X) W = Iso.refl (X ⊗ W).

Русский

Левый whisker по тождественному изоморфизму на X равен тождественному изоморфизму на X ⊗ W.

LaTeX

$$$ \mathrm{whiskerRightIso}(\mathrm{Iso.refl}(X), W) = \mathrm{Iso.refl}(X \otimes W). $$$

Lean4

@[simp]
theorem whiskerRightIso_refl (X W : C) : whiskerRightIso (Iso.refl X) W = Iso.refl (X ⊗ W) :=
  Iso.ext (id_whiskerRight X W)

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