factorsThroughLocalization — Mathlib

English

For any f, RightHomotopyRel f f holds (reflexivity of right homotopy).

Русский

Для любого f выполняется RightHomotopyRel f f (рефлексивность правой гомотопии).

LaTeX

$$RightHomotopyRel f f$$

Lean4

theorem factorsThroughLocalization [CategoryWithWeakEquivalences C] :
    RightHomotopyRel.FactorsThroughLocalization (weakEquivalences C) :=
  by
  rintro X Y f g ⟨P, ⟨h⟩⟩
  let L := (weakEquivalences C).Q
  rw [areEqualizedByLocalization_iff L]
  suffices L.map P.p₀ = L.map P.p₁ 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_epi (L.map P.ι), ← L.map_comp]

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