English
For composable SmallHom morphisms α: X → Y and β: Y → Z, the image under equiv of the composite α ∘ β equals the composition of the images: equiv(α ∘ β) = equiv(α) ∘ equiv(β).
Русский
Для сопоставимых малых локализационных гомоморфизмов α: X → Y и β: Y → Z их образ под отображением эквивалентности сохраняет композицию: equiv(α ∘ β) = equiv(α) ∘ equiv(β).
LaTeX
$$$\forall {X,Y,Z} \ [\text{HasSmallLocalizedHom } W X Y] [\text{HasSmallLocalizedHom } W Y Z] [\text{HasSmallLocalizedHom } W X Z],\ \alpha : \mathrm{SmallHom}\, W X Y,\ \beta : \mathrm{SmallHom}\, W Y Z: \\qquad
\operatorname{equiv}_W L (\alpha \cdot \beta) = \operatorname{equiv}_W L (\alpha) \cdot \operatorname{equiv}_W L (\beta).$$$
Lean4
theorem equiv_comp (L : C ⥤ D) [L.IsLocalization W] {X Y Z : C} [HasSmallLocalizedHom.{w} W X Y]
[HasSmallLocalizedHom.{w} W Y Z] [HasSmallLocalizedHom.{w} W X Z] (α : SmallHom.{w} W X Y)
(β : SmallHom.{w} W Y Z) : equiv W L (α.comp β) = equiv W L α ≫ equiv W L β :=
by
letI := small_of_hasSmallLocalizedHom.{w} W W.Q X Y
letI := small_of_hasSmallLocalizedHom.{w} W W.Q Y Z
obtain ⟨α, rfl⟩ := (equivShrink _).surjective α
obtain ⟨β, rfl⟩ := (equivShrink _).surjective β
dsimp [equiv, comp]
rw [Equiv.symm_apply_apply]
simp only [homEquiv_refl, homEquiv_comp]
