homEquiv_comp — Mathlib

English

HomEquiv respects composition in the domain C: composing two morphisms f, g in C corresponds to composing their images under homEquiv.

Русский

HomEquiv сохраняет композицию в области C: композиция двух морфизмов f, g соответствует композиции их изображений через homEquiv.

LaTeX

$$$ homEquiv W L_1 L_2 (f \\circ g) = homEquiv W L_1 L_2 f \\circ homEquiv W L_1 L_2 g $$$

Lean4

theorem homEquiv_comp (f : L₁.obj X ⟶ L₁.obj Y) (g : L₁.obj Y ⟶ L₁.obj Z) :
    homEquiv W L₁ L₂ (f ≫ g) = homEquiv W L₁ L₂ f ≫ homEquiv W L₁ L₂ g := by apply LocalizerMorphism.homMap_comp

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