homEquiv_id — Mathlib

English

Applying homEquiv to an identity morphism yields the identity morphism in the target localization.

Русский

Применение homEquiv к тождественному морфизму даёт тождественный морфизм в целевой локализации.

LaTeX

$$$ homEquiv W L_1 L_2 (\\mathrm{id}_{L_1 X}) = \\mathrm{id}_{L_2 X} $$$

Lean4

@[simp]
theorem homEquiv_id : homEquiv W L₁ L₂ (𝟙 (L₁.obj X)) = 𝟙 (L₂.obj X) := by simp [homEquiv_apply]

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