instHasRightResolutionsIdOfContainsIdentities

English

The identity LocalizerMorphism id W₁ has right resolutions; for each object X₂ there is a right resolution given by the identity on X₂.

Русский

Локализующий морфизм-идентичность id W₁ имеет правые резолюции; для каждого объекта X₂ существует правая резолюция, заданная тождественным отображением на X₂.

LaTeX

$$$\bigl(\mathrm{LocalizerMorphism.id\;W_1}\bigr).HasRightResolutions$$

Lean4

instance [W₁.ContainsIdentities] : (LocalizerMorphism.id W₁).HasRightResolutions := fun X₂ =>
  ⟨RightResolution.mk (𝟙 X₂) (W₁.id_mem X₂)⟩

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