instIsReflexivePairMapAppCounitObj

English

For an adjunction F ⊣ G with counit ε, the pair (F G ε_B, ε_FG B) is reflexive.

Русский

Для сцепления F ⊣ G с контуром ε пара (F G ε_B, ε_{F G B}) образует рефлексивную пару.

LaTeX

$$$\text{For an adjunction } F \dashv G, \; (F\circ G\varepsilon_B, \varepsilon_{F G B}) \text{ is a reflexive pair}$$$

Lean4

/-- For an adjunction `F ⊣ G` with counit `ε`, the pair `(FGε_B, ε_FGB)` is reflexive. -/
instance (B : D) : IsReflexivePair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))) :=
  IsReflexivePair.mk' (F.map (adj.unit.app (G.obj B)))
    (by
      rw [← F.map_comp, adj.right_triangle_components]
      apply F.map_id)
    (adj.left_triangle_components _)

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