unitCompPartialBijective_symm_apply

English

The naturality of the inverse bijection with respect to a morphism h: B ⟶ B' expresses that composing with h commutes with taking the inverse bijection.

Русский

Натуральность обратной биекции по отношению к морфизму h: B ⟶ B' выражается тем, что композиция с h коммутирует с взятием обратной биекции.

LaTeX

$$$(unitCompPartialBijective A hB').symm (f \\circ h) = (unitCompPartialBijective A hB).symm f \\circ h$$$

Lean4

@[simp]
theorem unitCompPartialBijective_symm_apply [Reflective i] (A : C) {B : C} (hB : i.essImage B) (f) :
    (unitCompPartialBijective A hB).symm f = (reflectorAdjunction i).unit.app A ≫ f := by
  simp [unitCompPartialBijective, unitCompPartialBijectiveAux_symm_apply]

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