instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient

Mathlib.Algebra.Homology.HomotopyCategory

URI: https://scilib.ai/kg/mathlib#HomotopyCategory.instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient

English

The left whiskering functor, when passed to the quotient, remains full.

Русский

Левый конический функтор при переходе к квоте сохраняет полноту.

LaTeX

$$$\text{Full}((\text{Functor.whiskeringLeft} \; - \; -).(\mathrm{HomotopyCategory}))$$$

Lean4

instance {D : Type*} [Category D] : ((Functor.whiskeringLeft _ _ D).obj (quotient V c)).Full :=
  Quotient.full_whiskeringLeft_functor _ _

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

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

Разделы

Аффилиация

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