homEquiv_eq — Mathlib

English

The transitivity of homEquiv states the equality of the composed equivalence with the single equivalence using G, e, and the composed functor.

Русский

Транзитивность homEquiv утверждает равенство составной эквивалентности и одной эквивалентности с использованием G, e и композиции функторов.

LaTeX

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

Lean4

theorem homEquiv_eq (G : D₁ ⥤ D₂) (e : L₁ ⋙ G ≅ L₂) (f : L₁.obj X ⟶ L₁.obj Y) :
    homEquiv W L₁ L₂ f = e.inv.app X ≫ G.map f ≫ e.hom.app Y := by
  rw [homEquiv_apply, LocalizerMorphism.homMap_apply (LocalizerMorphism.id W) L₁ L₂ G e.symm, Iso.symm_hom,
    Iso.symm_inv]

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