functorEquivFunctorCompSndIso — Mathlib

English

There is an isomorphism relating the forward part of the sum functor with the second projection, via a natural identification.

Русский

Существует изоморфизм, связывающий переднюю часть суммы функторов со второй проекцией через естественное соответствие.

LaTeX

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

Lean4

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

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