shrinkEquiv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The bijection `Arrow (Shrink C) ≃ Arrow C`. -/
noncomputable def shrinkEquiv (C : Type u) [Category.{v} C] [Small.{w} C] : Arrow (Shrink.{w} C) ≃ Arrow C
    where
  toFun := (Shrink.equivalence C).inverse.mapArrow.obj
  invFun := (Shrink.equivalence C).functor.mapArrow.obj
  left_inv _ := Arrow.ext (Equiv.apply_symm_apply _ _) ((Equiv.apply_symm_apply _ _)) (by simp; rfl)
  right_inv _ := Arrow.ext (by simp [Shrink.equivalence]) (by simp [Shrink.equivalence]) (by simp [Shrink.equivalence])

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