weakEquivalence_iff — Mathlib

English

For any two maps f0, f1: X → Y, if there is a right homotopy between them, then f0 is a weak equivalence iff f1 is.

Русский

Если между f0 и f1 существует правая гомотопия, то f0 — слабое эквивалентное отображение тогда и только тогда, когда f1 — слабое эквивалентное.

LaTeX

$$$WeakEquivalence\,f_0 \;\iff\; WeakEquivalence\,f_1$$$

Lean4

theorem weakEquivalence_iff [(weakEquivalences C).HasTwoOutOfThreeProperty] [(weakEquivalences C).ContainsIdentities]
    {f₀ f₁ : X ⟶ Y} (h : P.RightHomotopy f₀ f₁) : WeakEquivalence f₀ ↔ WeakEquivalence f₁ :=
  by
  revert P f₀ f₁
  suffices ∀ (P : PathObject Y) {f₀ f₁ : X ⟶ Y} (h : P.RightHomotopy f₀ f₁), WeakEquivalence f₀ → WeakEquivalence f₁
    from fun _ _ _ h ↦ ⟨this _ h, this _ h.symm⟩
  intro P f₀ f₁ h h₀
  have := weakEquivalence_of_postcomp_of_fac h.h₀
  rw [← h.h₁]
  infer_instance

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