coyonedaUnique — Mathlib

English

If n is a singleton, coyoneda.obj (op n) is naturally isomorphic to the identity functor.

Русский

Если n — одиничный, то coyoneda.obj (op n) естественно изоморфна тождественному функтору.

LaTeX

$$$\operatorname{coyoneda}(\operatorname{op} n) \cong 1$ for unique n$$

Lean4

/-- If `n` is a singleton, `Hom(n, -)` is the identity in `CommRingCat`. -/
@[simps!]
def coyonedaUnique {n : Type v} [Unique n] : coyoneda.obj (op n) ≅ 𝟭 CommRingCat.{max u v} :=
  NatIso.ofComponents (fun X ↦ (RingEquiv.piUnique _).toCommRingCatIso) (fun f ↦ by ext; simp)

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