homEquiv_comp — Mathlib

English

For a morphism f: F₁ ⇒ F₂ and index j ∈ J, the image under homEquiv composed with enrichedHomπ at j equals the corresponding enriched version of τ.app j.

Русский

Для морфизма f: F₁ ⇒ F₂ и индекса j ∈ J, образ под homEquiv затем через enrichedHomπ на j равен соответствующей обогащённой версии τ.app j.

LaTeX

$$$\\mathrm{homEquiv}_V(f) \\;\\circ\\; \\mathrm{enrichedHom} \\pi_{F_1,F_2}(j) = eHomEquiv_V(f.app(j))$$$

Lean4

@[reassoc]
theorem homEquiv_comp (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) :
    (homEquiv V) (f ≫ g) = (λ_ (𝟙_ V)).inv ≫ ((homEquiv V) f ⊗ₘ (homEquiv V) g) ≫ enrichedComp V F₁ F₂ F₃ :=
  by
  ext j
  simp only [homEquiv_apply_π, NatTrans.comp_app, eHomEquiv_comp, assoc, enrichedComp_π, Functor.op_obj,
    tensorHom_comp_tensorHom_assoc]

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