pullbackObjIsDefined_eq_top — Mathlib

English

There is a right adjoint structure to pushforward functor given by a certain equivalence

Русский

Существует структура правого сопряжённого отображения к операции pushforward

LaTeX

$$$\\text{pushforward}(\\varphi) \\dashv ?$$$

Lean4

theorem pullbackObjIsDefined_eq_top : pullbackObjIsDefined.{u} φ = ⊤ :=
  by
  ext M
  simp only [Pi.top_apply, «Prop».top_eq_true, iff_true]
  apply Functor.leftAdjointObjIsDefined_of_isColimit M.isColimitFreeYonedaCoproductsCokernelCofork
  rintro (_ | _)
  all_goals apply Functor.leftAdjointObjIsDefined_colimit _ (fun _ ↦ pullbackObjIsDefined_free_yoneda _ _)

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