instRepresentablyCoflatOppositeOpOfRepresentablyFlat

Mathlib.CategoryTheory.Functor.Flat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instRepresentablyCoflatOppositeOpOfRepresentablyFlat

English

If F is an equivalence, then StrongEpi (F.map f) iff StrongEpi f.

Русский

Если F — эквивалентность, то StrongEpi(F.map f) эквивалентно StrongEpi(f).

LaTeX

$$$$ \\operatorname{StrongEpi}(F.map f) \\iff \\operatorname{StrongEpi}(f). $$$$

Lean4

instance [RepresentablyFlat F] : RepresentablyCoflat F.op :=
  (representablyCoflat_op_iff F).2 inferInstance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru