English
Converts given el : α.l ≅ β.l, er : β.r ≅ α.r, and h : conjugateEquiv β.adj α.adj el.hom = er.hom into an isomorphism α ≅ β with hom and inv built from el, er and h.
Русский
Преобразование данных el, er и h в изоморфизм α ≅ β с компонентами, заданными через el, er и h.
LaTeX
$$$$ \exists \theta: \alpha \cong \beta \;\text{ s.t. } \theta.hom.\tau_\ell = el.hom, \; \theta.hom.\tau_r = er.hom, \; \text{conjugateEquiv}_{\tau_\ell}(\theta.hom) = h. $$$$
Lean4
/-- Constructor for isomorphisms between 1-morphisms in the bicategory `Adj B`. -/
@[simps]
def iso₂Mk {α β : a ⟶ b} (el : α.l ≅ β.l) (er : β.r ≅ α.r) (h : conjugateEquiv β.adj α.adj el.hom = er.hom) : α ≅ β
where
hom :=
{ τl := el.hom
τr := er.hom
conjugateEquiv_τl := h }
inv :=
{ τl := el.inv
τr := er.inv
conjugateEquiv_τl := by
rw [← cancel_mono er.hom, Iso.inv_hom_id, ← h, conjugateEquiv_comp, Iso.hom_inv_id, conjugateEquiv_id] }
