reflexiveCoforkEquivCofork_functor_obj_π

English

For any F and reflexive cofork G, the π component of the corresponding functor on G agrees with G.π.

Русский

Для любого F и рефлексивного кофокора G компоненту π соответствующего объекта-функторона на G совпадает с G.π.

LaTeX

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

Lean4

@[simp]
theorem reflexiveCoforkEquivCofork_functor_obj_π (G : ReflexiveCofork F) :
    ((reflexiveCoforkEquivCofork F).functor.obj G).π = G.π :=
  by
  dsimp [reflexiveCoforkEquivCofork]
  rw [ReflexiveCofork.π, Cofork.π]
  simp

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