lan_flat_of_flat

Mathlib.CategoryTheory.Functor.Flat

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

English

If F is representably flat, then RepresentablyFlat (F.op.lan).

Русский

Если F представимо плоский, то RepresentablyFlat (F.op.lan).

LaTeX

$$RepresentablyFlat F.op.lan$$

Lean4

instance lan_flat_of_flat (F : C ⥤ D) [RepresentablyFlat F] : RepresentablyFlat (F.op.lan : _ ⥤ Dᵒᵖ ⥤ E) :=
  flat_of_preservesFiniteLimits _

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

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

Разделы

Аффилиация

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