English
If a morphism property P on W.Localization is stable under composition and contains all images of original arrows and inverses of W, then P is the top property.
Русский
Если свойство морфизмов P на W.Localization стабильно по композиции и содержит изображения всех стрел оригинала и обращения W, то P равно верхнему свойству.
LaTeX
$$$P$ стабильна по композиции and $(\forall f:\ Y\to Z, P(W.map f))$ and $(\forall w:\ X\to Y, W w \Rightarrow P(w^{-1})) \Rightarrow P = \top$$$
Lean4
/-- Under some conditions on the `MorphismProperty`, functors satisfying the strict
universal property of the localization are stable under composition -/
def comp (h₁ : StrictUniversalPropertyFixedTarget L₁ W₁ E) (h₂ : StrictUniversalPropertyFixedTarget L₂ W₂ E)
(W₃ : MorphismProperty C₁) (hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)) (hW₁₃ : W₁ ≤ W₃) (hW₂₃ : W₂ ≤ W₃.map L₁) :
StrictUniversalPropertyFixedTarget (L₁ ⋙ L₂) W₃ E
where
inverts := hW₃
lift F
hF :=
h₂.lift (h₁.lift F (MorphismProperty.IsInvertedBy.of_le _ _ F hF hW₁₃))
(by
refine MorphismProperty.IsInvertedBy.of_le _ _ _ ?_ hW₂₃
simpa only [MorphismProperty.IsInvertedBy.map_iff, h₁.fac F] using hF)
fac F hF := by rw [Functor.assoc, h₂.fac, h₁.fac]
uniq _ _ h := h₂.uniq _ _ (h₁.uniq _ _ (by simpa only [Functor.assoc] using h))
