tensorObj — Mathlib

Lean4
/-- A tensor product of representable functors is representable. -/
@[simps]
protected def tensorObj {F : Cᵒᵖ ⥤ Type v} {G : Cᵒᵖ ⥤ Type v} {X Y : C} (h₁ : F.RepresentableBy X)
    (h₂ : G.RepresentableBy Y) : (F ⊗ G).RepresentableBy (X ⊗ Y)
    where
  homEquiv {I} := homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)
  homEquiv_comp {I W} f
    g := by
    refine Prod.ext ?_ ?_
    · change h₁.homEquiv ((f ≫ g) ≫ fst X Y) = F.map f.op (h₁.homEquiv (g ≫ fst X Y))
      simp [h₁.homEquiv_comp]
    · change h₂.homEquiv ((f ≫ g) ≫ snd X Y) = G.map f.op (h₂.homEquiv (g ≫ snd X Y))
      simp [h₂.homEquiv_comp]
Похожие утверждения