equivalence — Mathlib

English

For any X, Y in a model category with IsCofibrant X, LeftHomotopyRel defines an equivalence relation on all arrows X → Y.

Русский

Для любых X, Y в моделевой категории с условием IsCofibrant X отношение LeftHomotopyRel образует эквивалентность на стрелках X → Y.

LaTeX

$$$\text{LeftHomotopyRel}$ is an equivalence relation on $\mathrm{Hom}(X,Y)$$$

Lean4

theorem equivalence [ModelCategory C] (X Y : C) [IsCofibrant X] : _root_.Equivalence (LeftHomotopyRel (X := X) (Y := Y))
    where
  refl := .refl
  symm h := h.symm
  trans h h' := h.trans h'

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