functorEquivInverseCompWhiskeringLeftInrIso

English

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

Русский

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

LaTeX

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

Lean4

/-- Composing the backward direction of `functorEquiv` with the second projection is the same as
precomposition with `inr_ A A'`. -/
@[simps!]
def functorEquivInverseCompWhiskeringLeftInrIso :
    (functorEquiv A A' B).inverse ⋙ (whiskeringLeft A' (A ⊕ A') B).obj (inr_ A A') ≅ Prod.snd (A ⥤ B) (A' ⥤ B) :=
  NatIso.ofComponents (fun _ ↦ Functor.inrCompSum' _ _)

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