English
A variant of the top-property criterion: if P on W.Localization is stable under composition, and if every W.map f lies in P and every inverse e from an isomorphism with P-hom lies in P, then P is top.
Русский
Вариант критерия верхнего свойства: если P на W.Localization стабильно по композиции, и если все P(W.map f) и все обратные стороны из изоморфизмов с P-гармонией принадлежат P, то P = top.
LaTeX
$$$P$ is stable under composition and $(\forall f, P(W.map f))$ and $(\forall e, P(e.hom) \Rightarrow P(e.inv)) \Rightarrow P = \top$$$
Lean4
/-- A `MorphismProperty` in `W.Localization` is satisfied by all
morphisms in the localized category if it contains the image of the
morphisms in the original category, if is stable under composition
and if the property is stable by passing to inverses. -/
theorem morphismProperty_is_top' (P : MorphismProperty W.Localization) [P.IsStableUnderComposition]
(hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)) (hP₂ : ∀ ⦃X Y : W.Localization⦄ (e : X ≅ Y) (_ : P e.hom), P e.inv) :
P = ⊤ :=
morphismProperty_is_top P hP₁ (fun _ _ w _ => hP₂ _ (hP₁ w))
