instIsReflexivePairMapAppCounitOtherMap

English

If unit at A is an isomorphism, then R.essImage A holds.

Русский

Если единица η_A изоморфизм, то R.essImage A верно.

LaTeX

$$$\forall A:\ C, IsIso(h.unit.app A) \Rightarrow R.essImage A$$$

Lean4

/-- `(F'Uε_X, otherMap X)` is a reflexive pair: in particular if `A` has reflexive coequalizers then
this pair has a coequalizer.
-/
instance (X : B) : IsReflexivePair (F'.map (U.map (adj₁.counit.app X))) (otherMap _ _ adj₁ adj₂ X) :=
  IsReflexivePair.mk' (F'.map (adj₁.unit.app (U.obj X)))
    (by
      rw [← F'.map_comp, adj₁.right_triangle_components]
      apply F'.map_id)
    (by
      dsimp [otherMap]
      rw [← F'.map_comp_assoc, U.map_comp, adj₁.unit_naturality_assoc, adj₁.right_triangle_components, comp_id,
        adj₂.left_triangle_components])

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