full_embedding

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.full_embedding

English

If F: D → C^op is full, then the composed embedding with the opposite preserves fullness.

Русский

Если F полно, то композиция вложения с противоположной категорией сохраняет полноту.

LaTeX

$$F.comp(embedding F).Full$$

Lean4

instance full_embedding [Nonempty D] [F.Full] : (F ⋙ embedding F).Full :=
  full_comp_preadditiveCoyonedaObj _ (isSeparator F) (exists_epi F)

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

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

Разделы

Аффилиация

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