counitForward — Mathlib

English

Repeat of Naturality 2 for the specific instance with restricted Yoneda object η.

Русский

Повтор натуральности 2 для конкретного случая с ограниченным объектом Йонеда η.

LaTeX

$$$$ unitForward_\eta X (YonedaCollection.map_2 (restrictedYonedaObj\eta) f p) = F.map f^{op} (unitForward_\eta Y p) $$$$

Lean4

/-- Forward direction of the counit. -/
def counitForward (F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) (s : CostructuredArrow yoneda A) :
    F.obj (op s) → OverArrows (yonedaCollectionPresheafToA F) s.hom := fun x =>
  ⟨YonedaCollection.mk s.hom x, ⟨by simp [YonedaCollection.yonedaEquivFst_eq]⟩⟩

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