English
The identity LocalizerMorphism id W₁ has left resolutions; for each object X₁ there is a left resolution given by the identity on X₁.
Русский
Локализующий морфизм-идентичность id W₁ имеет левые резолюции; для каждого объекта X₁ существует левая резолюция, заданная тождественным отображением на X₁.
LaTeX
$$$\bigl(\mathrm{LocalizerMorphism.id\;W_1}\bigr).HasLeftResolutions$$
Lean4
instance [W₁.ContainsIdentities] : (LocalizerMorphism.id W₁).IsRightDerivabilityStructure :=
by
rw [(LocalizerMorphism.id W₁).isRightDerivabilityStructure_iff W₁.Q W₁.Q (𝟭 W₁.Localization) (Iso.refl _)]
dsimp
exact TwoSquare.guitartExact_id W₁.Q
