factorsThroughLocalization — Mathlib

English

In any category equipped with a class of weak equivalences, any two arrows that are left-homotopic coincide after localization with respect to those weak equivalences.

Русский

В любой категории с слабыми эквивалентностями любые две стрелки, связанные лево-гомотопией, совпадают после локализации по этим слабым эквивалентностям.

LaTeX

$$$ f \sim_L g \Rightarrow L(f) = L(g)$$$

Lean4

theorem factorsThroughLocalization [CategoryWithWeakEquivalences C] :
    LeftHomotopyRel.FactorsThroughLocalization (weakEquivalences C) :=
  by
  rintro X Y f g ⟨P, ⟨h⟩⟩
  let L := (weakEquivalences C).Q
  rw [areEqualizedByLocalization_iff L]
  suffices L.map P.i₀ = L.map P.i₁ by simp only [← h.h₀, ← h.h₁, L.map_comp, this]
  have :=
    Localization.inverts L (weakEquivalences C) P.π
      (by
        rw [← weakEquivalence_iff]
        infer_instance)
  simp [← cancel_mono (L.map P.π), ← L.map_comp, P.i₀_π, P.i₁_π]

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