comp_homEquiv — Mathlib

English

The hom-equivalence of the composite adjunction equals the composition of the hom-equivalences: (adj1.comp adj2).homEquiv(x, y) = adj2.homEquiv(F.obj x, y) ∘ adj1.homEquiv(x, I.obj y).

Русский

Гом-эквивалентность композиции адъюнкций равна композиции их гом-эквивалентностей: (adj1.comp adj2).homEquiv = adj2.homEquiv ∘ adj1.homEquiv.

LaTeX

$$$ (adj_1.comp adj_2).homEquiv = (\lambda x, x_1. (adj_2.homEquiv (F.obj x) x_1) \circ (adj_1.homEquiv x (I.obj x_1))) $$$

Lean4

theorem comp_homEquiv : (adj₁.comp adj₂).homEquiv = fun _ _ ↦ Equiv.trans (adj₂.homEquiv _ _) (adj₁.homEquiv _ _) :=
  mk'_homEquiv _

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