homEquiv_naturality_two_symm — Mathlib

English

Let f2: F2 ⟶ F2' and g: F2' ⟶ functorEnrichedHom C F1 F3 be morphisms in the respective functor categories. The inverse of the composite under the homEquiv is given by whiskering on the left by F1 and composing with the inverse image of g.

Русский

Пусть f2: F2 ⟶ F2' и g: F2' ⟶ functorEnrichedHom C F1 F3 являются морфизмами. Обратный образ композиции f2 ≫ g через гом-эквивариантность равен левому усечению по F1 и последующему композиционному применению обратного образа g.

LaTeX

$$$ \\mathrm{homEquiv}^{-1}(f_2 \\;\\circ\\; g) = F_1 \\triangleleft f_2 \\;\\circ\\; \\mathrm{homEquiv}^{-1}(g) $$$

Lean4

theorem homEquiv_naturality_two_symm (f₂ : F₂ ⟶ F₂') (g : F₂' ⟶ functorEnrichedHom C F₁ F₃) :
    homEquiv.symm (f₂ ≫ g) = F₁ ◁ f₂ ≫ homEquiv.symm g :=
  by
  dsimp [homEquiv]
  ext j
  simp [← uncurry_natural_left]

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