instHasFunctorialFactorizationFunctorFunctorCategory

English

If HasFunctorialFactorization W₁ W₂ holds, then HasFunctorialFactorization (W₁.functorCategory J) (W₂.functorCategory J) holds for any category J.

Русский

Если существует факторизация для W₁ и W₂, то существует факторизация для соответствующих категорий FunctorCategory.

LaTeX

$$[HasFunctorialFactorization W₁ W₂] ⇒ HasFunctorialFactorization (W₁.functorCategory J) (W₂.functorCategory J)$$

Lean4

instance [HasFunctorialFactorization W₁ W₂] (J : Type*) [Category J] :
    HasFunctorialFactorization (W₁.functorCategory J) (W₂.functorCategory J) :=
  ⟨⟨(functorialFactorizationData W₁ W₂).functorCategory J⟩⟩

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