unitCompPartialBijectiveAux — Mathlib

English

(Implementation) An auxiliary definition giving an equivalence between morphisms A ⟶ i.obj B and i.obj((reflector i).obj A) ⟶ i.obj B, built from the unit and isomorphisms witnessing essImage.

Русский

(Реализация) Вспомогательное определение, задающее эквиваленцию между морфизмами A ⟶ i.obj B и i.obj((reflector i).obj A) ⟶ i.obj B, конструируемую из единицы и изоморфизмов, доказывающих принадлежность essImage.

LaTeX

$$$(A \\to i.obj B) \\simeq (i.obj ((reflector i).obj A) \\to i.obj B)$$$

Lean4

/-- (Implementation) Auxiliary definition for `unitCompPartialBijective`. -/
def unitCompPartialBijectiveAux [Reflective i] (A : C) (B : D) :
    (A ⟶ i.obj B) ≃ (i.obj ((reflector i).obj A) ⟶ i.obj B) :=
  ((reflectorAdjunction i).homEquiv _ _).symm.trans (Functor.FullyFaithful.ofFullyFaithful i).homEquiv

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