mkOfHomEquiv_homEquiv — Mathlib

English

The hom-equivalence produced by mkOfHomEquiv coincides with the given adjunction homEquiv.

Русский

Гом-эквивалентность, получаемая mkOfHomEquiv, совпадает с заданной adj.homEquiv.

LaTeX

$$$ (mkOfHomEquiv adj).homEquiv = adj.homEquiv $$$

Lean4

@[simp]
theorem mkOfHomEquiv_homEquiv (adj : CoreHomEquiv F G) : (mkOfHomEquiv adj).homEquiv = adj.homEquiv :=
  by
  ext X Y g
  simp [mkOfHomEquiv, ← adj.homEquiv_naturality_right (𝟙 _) g]

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