English
The functorial right resolution respects the map ι via Φ.functor and i, giving equality of maps on objects.
Русский
右のфункторальная резолюция сохраняет отображение ι через Φ.functor и i, обеспечивая равенство отображений на объектах.
LaTeX
$$$\Phi.functor.map((\mathrm{ι} i)_{\mathrm{app}} X_1) = i_{(\Phi.functor.obj X_1)}$$$
Lean4
theorem isRightDerivabilityStructure_of_functorial_resolutions : Φ.IsRightDerivabilityStructure :=
by
have : W₁.IsMultiplicative := by rw [hW₁]; infer_instance
have := Φ.isLocalizedEquivalence_of_functorial_right_resolutions i hi hW₁
have := Φ.hasRightResolutions_arrow_of_functorial_resolutions i hi
have := Φ.isConnected_rightResolution_of_functorial_resolutions i hi hW₁
apply IsRightDerivabilityStructure.mk'
