equivalenceOfEquiv — Mathlib

English

If J ≃ J' then WidePullbackShape J ≃ WidePullbackShape J'.

Русский

Если J эквивалентно J', то WidePullbackShape J эквивалентен WidePullbackShape J'.

LaTeX

$$$$\\mathrm{WidePullbackShape} \\ J \\simeq \\mathrm{WidePullbackShape} \\ J'\\quad\\text{whenever } J \\simeq J'.$$$$

Lean4

/-- Wide pullback diagrams of equivalent index types are equivalent. -/
def equivalenceOfEquiv (J' : Type w') (h : J ≃ J') : WidePullbackShape J ≌ WidePullbackShape J'
    where
  functor := wideCospan none (fun j => some (h j)) fun j => Hom.term (h j)
  inverse := wideCospan none (fun j => some (h.invFun j)) fun j => Hom.term (h.invFun j)
  unitIso := NatIso.ofComponents (fun j => by cases j <;> exact eqToIso (by simp))
  counitIso := NatIso.ofComponents (fun j => by cases j <;> exact eqToIso (by simp))

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