homEquiv_trans — Mathlib

English

HomEquiv respects composition of morphisms across three localizations: composing f then g corresponds to composing their images under homEquiv.

Русский

HomEquiv сохраняет композицию морфизмов через три локализации: композиция f и g равна композиции их образов через HomEquiv.

LaTeX

$$$ homEquiv W L_2 L_3 (homo(f \\circ g)) = homEquiv W L_2 L_3 (f) \\circ homEquiv W L_2 L_3 (g) $$$

Lean4

theorem homEquiv_trans (f : L₁.obj X ⟶ L₁.obj Y) : homEquiv W L₂ L₃ (homEquiv W L₁ L₂ f) = homEquiv W L₁ L₃ f :=
  by
  dsimp only [homEquiv_apply]
  apply LocalizerMorphism.homMap_homMap

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