widePushoutShapeOpMap — Mathlib

English

The functorial action on morphisms for the obvious functor from WidePushoutShape to WidePullbackShape is defined by id and init cases similarly to the dual construction.

Русский

Действие на морфизмы у соответствующего функтору от WidePushoutShape к WidePullbackShape задаётся как в двойственной конструкции.

LaTeX

$$$\\text{widePushoutShapeOpMap} : X \\to Y \\mapsto ...$ (формулировка в духе двойственной композиции)$$

Lean4

/-- The action on morphisms of the obvious functor
`widePushoutShapeOp : WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ` -/
def widePushoutShapeOpMap :
    ∀ X Y : WidePushoutShape J, (X ⟶ Y) → ((op X : (WidePullbackShape J)ᵒᵖ) ⟶ (op Y : (WidePullbackShape J)ᵒᵖ))
  | _, _, WidePushoutShape.Hom.id X => Quiver.Hom.op (WidePullbackShape.Hom.id _)
  | _, _, WidePushoutShape.Hom.init _ => Quiver.Hom.op (WidePullbackShape.Hom.term _)

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