rightUnitorCorepresentingIso — Mathlib

English

There exists a canonical isomorphism between corepresentable functors giving the right unitor for the Day convolution.

Русский

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

LaTeX

$$$ (\text{RightUnitorCorepresentingIso}) :\; (\text{whiskeringLeft} \; (\text{tensor} C)) \;\cong\; \text{Coyoneda}.(\op F) $$$

Lean4

/-- The isomorphism of corepresentable functors that defines the right unitor for
Day convolution. -/
@[simps!]
def rightUnitorCorepresentingIso :
    (whiskeringLeft _ _ _).obj (tensor C) ⋙
        (whiskeringLeft _ _ _).obj ((𝟭 C).prod (Functor.fromPUnit.{0} (𝟙_ C))) ⋙
          coyoneda.obj (.op <| F ⊠ Functor.fromPUnit.{0} (𝟙_ V)) ≅
      coyoneda.obj (.op <| F) :=
  by
  calc
    _ ≅
        (whiskeringLeft _ _ _).obj (tensor C) ⋙
          (whiskeringLeft _ _ _).obj ((𝟭 C).prod (Functor.fromPUnit.{0} (𝟙_ C))) ⋙
            (whiskeringLeft _ _ _).obj (prod.rightUnitorEquivalence C).inverse ⋙
              coyoneda.obj (.op <| (prod.rightUnitorEquivalence C).inverse ⋙ F ⊠ Functor.fromPUnit.{0} (𝟙_ V)) :=
      isoWhiskerLeft _
        (isoWhiskerLeft _
          (NatIso.ofComponents fun _ ↦
            Equiv.toIso <| (prod.rightUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv))
    _ ≅
        (whiskeringLeft _ _ _).obj
            ((prod.rightUnitorEquivalence C).inverse ⋙ ((𝟭 C).prod (Functor.fromPUnit.{0} (𝟙_ C))) ⋙ tensor C) ⋙
          coyoneda.obj (.op <| (prod.rightUnitorEquivalence C).inverse ⋙ F ⊠ Functor.fromPUnit.{0} (𝟙_ V)) :=
      (.refl _)
    _ ≅
        (whiskeringLeft _ _ _).obj (𝟭 _) ⋙
          coyoneda.obj (.op <| (prod.rightUnitorEquivalence C).inverse ⋙ F ⊠ Functor.fromPUnit.{0} (𝟙_ V)) :=
      (isoWhiskerRight ((whiskeringLeft _ _ _).mapIso <| NatIso.ofComponents fun _ ↦ ρ_ _) _)
    _ ≅ _ := coyoneda.mapIso <| Iso.op <| NatIso.ofComponents fun _ ↦ (ρ_ _).symm

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