functorEquivInverseCompWhiskeringLeftInlIso

English

The inverse direction of the functor equivalence, whiskered on the left with the left injection, is isomorphic to the product projection.

Русский

Обратное направление эквивалентности функторов, взятое через левый инъектор, изоморфно проекции произведения.

LaTeX

$$((\mathrm{functorEquiv} A A' B).inverse .\circ (\mathrm{whiskeringLeft} A (A \oplus A') B).obj(\mathrm{inl}_{A A'})) \cong \mathrm{Prod.fst}(A \to B)(A' \to B)$$

Lean4

/-- Composing the backward direction of `functorEquiv` with precomposition with `inl_ A A'`.
is naturally isomorphic to the first projection. -/
@[simps!]
def functorEquivInverseCompWhiskeringLeftInlIso :
    (functorEquiv A A' B).inverse ⋙ (whiskeringLeft A (A ⊕ A') B).obj (inl_ A A') ≅ Prod.fst (A ⥤ B) (A' ⥤ B) :=
  NatIso.ofComponents (fun _ ↦ Functor.inlCompSum' _ _)

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