enrichedOrdinaryCategorySelf_eHomWhiskerLeft

English

In a Monoidal Closed setting, the left whiskering of eHom by X on g equals the map (ihom X).map g.

Русский

В обстановке моноидально-замкнутой категории левое уславливание eHom по X к г равно отображению (ihom X).map g.

LaTeX

$$$ eHomWhiskerLeft\; C\; X\; g = (ihom\; X).map\; g $$$

Lean4

theorem enrichedOrdinaryCategorySelf_eHomWhiskerLeft (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :
    eHomWhiskerLeft C X g = (ihom X).map g :=
  by
  change (ρ_ _).inv ≫ _ ◁ curry' g ≫ comp X Y₁ Y₂ = _
  rw [whiskerLeft_curry'_comp, Iso.inv_hom_id_assoc]

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