pi — Mathlib · SciLib

English

If W maps pointwise to each component W_j inverted by F_j, then the pi-construction (product-like) is inverted by the pi-Functor.

Русский

Если каждый компонент W_j разворачивает F_j, то конструкция pi разворачивает соответствующий pi-функтор.

LaTeX

$$$ (\forall j, (W_j).IsInvertedBy(F_j)) \Rightarrow (\mathrm{MorphismProperty.pi}\ W).IsInvertedBy(\mathrm{Functor.pi}\ F) $$$

Lean4

theorem pi {J : Type w} {C : J → Type u} {D : J → Type u'} [∀ j, Category.{v} (C j)] [∀ j, Category.{v'} (D j)]
    (W : ∀ j, MorphismProperty (C j)) (F : ∀ j, C j ⥤ D j) (hF : ∀ j, (W j).IsInvertedBy (F j)) :
    (MorphismProperty.pi W).IsInvertedBy (Functor.pi F) :=
  by
  intro _ _ f hf
  rw [isIso_pi_iff]
  intro j
  exact hF j _ (hf j)

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