unitCompPartialBijective_symm_natural

English

The unit-composed partial bijection is the composed chain of isomorphisms relating A ⟶ B to i.obj((reflector i).obj A) ⟶ B via essImage witnesses and unit/counit morphisms.

Русский

Единичное отображение, составляющее частичную биекцию, задаётся как композиция изоморфизмов между A ⟶ B и i.obj((reflector i).obj A) ⟶ B через свидетели essImage и единицу/коуницию.

LaTeX

$$unitCompPartialBijective A hB = Iso.homCongr (Iso.refl _) hB.getIso.symm ≫ (unitCompPartialBijectiveAux _ _) ≫ Iso.homCongr (Iso.refl _) (Functor.essImage.getIso hB)$$

Lean4

theorem unitCompPartialBijective_symm_natural [Reflective i] (A : C) {B B' : C} (h : B ⟶ B') (hB : i.essImage B)
    (hB' : i.essImage B') (f : i.obj ((reflector i).obj A) ⟶ B) :
    (unitCompPartialBijective A hB').symm (f ≫ h) = (unitCompPartialBijective A hB).symm f ≫ h := by simp

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