instLaxMonoidalObjOppositeFunctorTypeCoyonedaOpTensorUnit

English

For a monoidal functor F out of Type, there is a canonical isomorphism F.obj(Fin(n+1) → β) ≅ F.obj β ⊗ F.obj(Fin n → β).

Русский

Для моноидального функторa F из типа существует естественное тождество F(Fin(n+1) → β) ≅ F(β) ⊗ F(Fin n → β).

LaTeX

$$$\\mathrm{mapPi} : F.obj(\\mathrm{Fin}(n+1) \\to \\beta) \\cong F.obj \\beta \\otimes F.obj(\\mathrm{Fin} n \\to \\beta).$$$

Lean4

instance (C : Type u) [Category.{v} C] [MonoidalCategory C] : (coyoneda.obj (op (𝟙_ C))).LaxMonoidal :=
  Functor.LaxMonoidal.ofTensorHom (ε := fun _ => 𝟙 _) (μ := fun X Y p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) (μ_natural := by
    cat_disch) (associativity := fun X Y Z => by
    ext ⟨⟨f, g⟩, h⟩; dsimp at f g h
    dsimp; simp only [Iso.cancel_iso_inv_left, Category.assoc]
    conv_lhs =>
      rw [← Category.id_comp h, ← tensorHom_comp_tensorHom, Category.assoc, associator_naturality, ← Category.assoc,
        unitors_inv_equal, tensorHom_id, triangle_assoc_comp_right_inv]
    conv_rhs => rw [← Category.id_comp f, ← tensorHom_comp_tensorHom]
    simp) (left_unitality := by
    intros
    ext ⟨⟨⟩, f⟩; dsimp at f
    simp) (right_unitality := fun X => by
    ext ⟨f, ⟨⟩⟩; dsimp at f
    simp [unitors_inv_equal])

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