homEquiv_refl — Mathlib

English

A second formulation of homEquiv_eq presenting the isomorphism e between L1⋅G and L2, and the map G on f.

Русский

Вторая формулировка homEquiv_eq показывает изоморфизм e между L1⋅G и L2 и отображение G на f.

LaTeX

$$$ homEquiv W L_1 L_2 f = e^{-1} \\circ G.map(f) \\circ e $$$

Lean4

@[simp]
theorem homEquiv_refl (f : L₁.obj X ⟶ L₁.obj Y) : homEquiv W L₁ L₁ f = f := by apply LocalizerMorphism.id_homMap

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