shrinkHomsEquiv — Mathlib

English

There is a natural equivalence between Arrow(ShrinkHoms C) and Arrow C.

Русский

Существует естественная эквивалентность между Arrow(ShrinkHoms C) и Arrow C.

LaTeX

$$$\\\\operatorname{Arrow}(\\\\operatorname{ShrinkHoms}(C)) \\simeq \\\\operatorname{Arrow}(C)$$$

Lean4

/-- The bijection `Arrow.{w} (ShrinkHoms C) ≃ Arrow C`. -/
noncomputable def shrinkHomsEquiv (C : Type u) [Category.{v} C] [LocallySmall.{w} C] :
    Arrow.{w} (ShrinkHoms C) ≃ Arrow C
    where
  toFun := (ShrinkHoms.equivalence C).inverse.mapArrow.obj
  invFun := (ShrinkHoms.equivalence C).functor.mapArrow.obj
  left_inv _ := by simp
  right_inv _ := by simp

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