instHasTwoOutOfThreePropertyInverseImage

English

If W is a morphism property on C with the two-out-of-three property, then for any functor F: C → D, the inverse image W.inverseImage(F) also has the two-out-of-three property.

Русский

Если W обладает свойством двух из трёх, то для любого функторa F: C → D обратный образ W.inverseImage(F) также имеет свойство двух из трёх.

LaTeX

$$$ (W^{-1} F) \\text{ has two-out-of-three given } W \\text{ has two-out-of-three and } F. $$$

Lean4

instance (F : C ⥤ D) (W : MorphismProperty D) [W.HasTwoOutOfThreeProperty] : (W.inverseImage F).HasTwoOutOfThreeProperty
    where
  of_postcomp f g hg hfg := W.of_postcomp (F.map f) (F.map g) hg (by simpa using hfg)
  of_precomp f g hf hfg := W.of_precomp (F.map f) (F.map g) hf (by simpa using hfg)

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