map_restrictFullyFaithful_counit_app

English

If A ∈ D and the counit at A is split epi, then A lies in essImage j.

Русский

Если A ∈ D и counit в A является разложимым эпиморфом, тогда A принадлежит essImage j.

LaTeX

$$j.essImage A$$

Lean4

@[simp, reassoc]
theorem map_restrictFullyFaithful_counit_app (X : D) :
    iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X) =
      comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X) :=
  by
  dsimp [restrictFullyFaithful]
  simp

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