counitForward_naturality₂ — Mathlib

English

A naturality statement for counitForward with respect to a morphism f: t ⟶ s in the costructured arrow context.

Русский

Натуральность counitForward по отношению к морфизму f: t ⟶ s в контексте CostructuredArrow.

LaTeX

$$$$ counitForward G s.unop (F.map f x) = OverArrows.map₂ (counitForward F t.unop x) f.unop.left (by simp) $$$$

Lean4

@[simp]
theorem counitForward_naturality₂ (s t : (CostructuredArrow yoneda A)ᵒᵖ) (f : t ⟶ s) (x : F.obj t) :
    counitForward F s.unop (F.map f x) = OverArrows.map₂ (counitForward F t.unop x) f.unop.left (by simp) :=
  by
  refine OverArrows.ext <| YonedaCollection.ext (by simp) ?_
  have : (CostructuredArrow.mkPrecomp t.unop.hom f.unop.left).op = f ≫ eqToHom (by simp [← CostructuredArrow.eq_mk]) :=
    by
    apply Quiver.Hom.unop_inj
    simp
  cat_disch

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