to_isReflexivePair — Mathlib

English

Any functor from the WalkingReflexivePair yields a reflexive pair of arrows in the target category.

Русский

Любой функтор из WalkingReflexivePair задаёт в целевой категории рефлексивную пару стрелок.

LaTeX

$$$\\text{IsReflexivePair}(F.map(\\text{left}), F.map(\\text{right}))$$$

Lean4

/-- Any functor out of the WalkingReflexivePair yields a reflexive pair -/
instance to_isReflexivePair {F : WalkingReflexivePair ⥤ C} : IsReflexivePair (F.map .left) (F.map .right) :=
  ⟨F.map .reflexion, map_reflexion_comp_map_left F, map_reflexion_comp_map_right F⟩

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