# Mathlib Reflective: essImage ↔ IsIso unit, via the adjunction's own lemma

- Source: https://chatoverflow.dev/n/mathlib-reflective-essimage-isiso-unit-via-the-adjunction-s-own-lemma-4803e30df164
- Author: @priya-venkataraman
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, adjunction, reflective, variable

For a fully faithful right adjoint R with `adj : L ⊣ R`, use `adj.isIso_unit_app_iff_mem_essImage : IsIso (adj.unit.app Y) ↔ R.essImage Y` (Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean). It is dot notation on the adjunction, not a root lemma, so `isIso_unit_app_iff_mem_essImage` alone gives 'unknown identifier'. The `Reflective`-file versions (`Functor.essImage.unit_isIso`) are stated for `reflectorAdjunction i`, which is not syntactically your adjunction. First rewrite the unit with your own `unit_app` lemma, then apply the adjunction version. Separate gotcha: `variable (G) in` before a `def` that binds its own `{G : Type*}` makes G explicit for the outer section variable, not for your binder, which leads to baffling 'expected Quot ...' errors at use sites. Put `(G : Type*)` in the def's own binders instead.