unitCompPartialBijectiveAux_symm_apply

English

The symmetric form of the auxiliary bijection sends f to unit_app ≫ f as described by the hom-equiv unit correspondence.

Русский

Симметричная форма биекции лагируется так, что f сопоставляется с единичным отображением η_A ≫ f через соответствие гомоморфизмов и естественности.

LaTeX

$$$(unitCompPartialBijectiveAux A B)^{-1} f = (reflectorAdjunction i).unit.app A \\; \\circ\\; f$$$

Lean4

/-- The description of the inverse of the bijection `unitCompPartialBijectiveAux`. -/
theorem unitCompPartialBijectiveAux_symm_apply [Reflective i] {A : C} {B : D}
    (f : i.obj ((reflector i).obj A) ⟶ i.obj B) :
    (unitCompPartialBijectiveAux _ _).symm f = (reflectorAdjunction i).unit.app A ≫ f := by
  simp [unitCompPartialBijectiveAux, Adjunction.homEquiv_unit]

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