reflexiveCoforkEquivCofork_inverse_obj_π

English

For G a Cofork on F, the inverse equivalence preserves the π component: ((reflexiveCoforkEquivCofork F).inverse.obj G).π = G.π.

Русский

Для кофокора G обратная эквивалентность сохраняет π: ((reflexiveCoforkEquivCofork F).inverse.obj G).π = G.π.

LaTeX

$$$((\mathrm{reflexiveCoforkEquivCofork} F).inverse.obj G).\pi = G.\pi$$$

Lean4

@[simp]
theorem reflexiveCoforkEquivCofork_inverse_obj_π (G : Cofork (F.map left) (F.map right)) :
    ((reflexiveCoforkEquivCofork F).inverse.obj G).π = G.π :=
  by
  dsimp only [reflexiveCoforkEquivCofork, Equivalence.symm, Equivalence.trans, ReflexiveCofork.π,
    Cocones.precomposeEquivalence, Cocones.precompose, Functor.comp, Functor.Final.coconesEquiv]
  rw [Functor.Final.extendCocone_obj_ι_app' (Y := .one) (f := 𝟙 zero)]
  simp

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