enrichedHom_condition — Mathlib

English

Naturality condition for enriched hom components: the enriched hom π at i composed with left whisker is equal to the enriched hom π at j composed with right whisker after applying F₁.map f and F₂.map f.

Русский

Натурализаторная условие для компонентов обогащённой гом: секущая гом π при i после левого whisker равна π при j после правого whisker после применения F₁.map f и F₂.map f.

LaTeX

$$$\\text{enrichedHom}_\\pi(V,F_1,F_2,i) \\;\\circ\\; e_{\\text{Left}} = \\text{enrichedHom}_\\pi(V,F_1,F_2,j) \\;\\circ\\; e_{\\text{Right}}$$$

Lean4

@[reassoc]
theorem enrichedHom_condition {i j : J} (f : i ⟶ j) :
    enrichedHomπ V F₁ F₂ i ≫ eHomWhiskerLeft V (F₁.obj i) (F₂.map f) =
      enrichedHomπ V F₁ F₂ j ≫ eHomWhiskerRight V (F₁.map f) (F₂.obj j) :=
  end_.condition (diagram V F₁ F₂) f

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