English
The inverse bijection maps f to η_A ≫ f, i.e. the φ-symmetric form of unitCompPartialBijective.
Русский
Обратная биекция переводит f в η_A ≫ f, т.е. симметрическая форма единицы bijection.
LaTeX
$$(EquivLike.toFunLike.coe (unitCompPartialBijective A hB).symm f) = (reflectorAdjunction i).unit.app A ≫ f$$
Lean4
/-- If `i` has a reflector `L`, then the function `(i.obj (L.obj A) ⟶ B) → (A ⟶ B)` given by
precomposing with `η.app A` is a bijection provided `B` is in the essential image of `i`.
That is, the function `fun (f : i.obj (L.obj A) ⟶ B) ↦ η.app A ≫ f` is bijective,
as long as `B` is in the essential image of `i`.
This definition gives an equivalence: the key property that the inverse can be described
nicely is shown in `unitCompPartialBijective_symm_apply`.
This establishes there is a natural bijection `(A ⟶ B) ≃ (i.obj (L.obj A) ⟶ B)`. In other words,
from the point of view of objects in `D`, `A` and `i.obj (L.obj A)` look the same: specifically
that `η.app A` is an isomorphism.
-/
def unitCompPartialBijective [Reflective i] (A : C) {B : C} (hB : i.essImage B) :
(A ⟶ B) ≃ (i.obj ((reflector i).obj A) ⟶ B) :=
calc
(A ⟶ B) ≃ (A ⟶ i.obj (Functor.essImage.witness hB)) := Iso.homCongr (Iso.refl _) hB.getIso.symm
_ ≃ (i.obj _ ⟶ i.obj (Functor.essImage.witness hB)) := (unitCompPartialBijectiveAux _ _)
_ ≃ (i.obj ((reflector i).obj A) ⟶ B) := Iso.homCongr (Iso.refl _) (Functor.essImage.getIso hB)
