instFibrationCompOfIsStableUnderCompositionFibrations

English

Let X → Y be a cofibration and a weak equivalence, and Z any fibrant object. Then the map g ↦ g.postcomp f induces a bijection on RightHomotopyClass(Y,Z) → RightHomotopyClass(X,Z).

Русский

Пусть f: X→Y — кофибрация и слабая эквивалентность, Z — фибривант. Тогда отображение g ↦ g ∘ f порождает биекцию RightHomotopyClass(Y,Z) → RightHomotopyClass(X,Z).

LaTeX

$$$\operatorname{Bij}\Big( \lambda g\in \operatorname{RightHo}(Y,Z),\; g\circ f\Big)$$$

Lean4

instance [CategoryWithFibrations C] [(fibrations C).IsStableUnderComposition] [hf : Fibration f] [hg : Fibration g] :
    Fibration (f ≫ g) :=
  (fibration_iff _).2 ((fibrations C).comp_mem _ _ hf.mem hg.mem)

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