inclHomEquiv — Mathlib

English

There is an equivalence between arrows from Incl X to Y and pairs (i, X -> Y_i).

Русский

Существует эквивалентость между стрелами из Incl X в Y и парами (i, X -> Y_i).

LaTeX

$$$((\\mathrm{incl} \\ C).\\mathrm{obj} X \\to Y) \\simeq \\{(i, X \\to Y_i)\\}$$$

Lean4

/-- A map `incl(X) ⟶ Y` is specified by an element of `Y`'s indexing set, and then a morphism
`X ⟶ Y.obj i` in the original category. -/
@[simps!]
def inclHomEquiv (X : C) (Y : FormalCoproduct.{w} C) : ((incl C).obj X ⟶ Y) ≃ (i : Y.I) × (X ⟶ Y.obj i)
    where
  toFun f := f.asSigma
  invFun f := .fromIncl f.1 f.2
  left_inv f := f.fromIncl_asSigma
  right_inv _ := rfl

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