English
IsConnected of RightResolution arrows is established by the constructor under the given hypotheses.
Русский
Связность правых резолюций стрел обеспечивается конструктором при заданных гипотезах.
LaTeX
$$$\text{Constructor.isConnected: IsConnected(Φ.RightResolution X_2) for all X_2}$$$
Lean4
theorem isConnected_rightResolution_of_functorial_resolutions (X₂ : C₂) :
letI : W₁.IsMultiplicative := by rw [hW₁]; infer_instance
IsConnected (Φ.RightResolution X₂) :=
by
have : W₁.IsMultiplicative := by rw [hW₁]; infer_instance
have : Nonempty (Φ.RightResolution X₂) := ⟨{ hw := hi X₂, .. }⟩
have : IsPreconnected (Φ.RightResolution X₂) :=
zigzag_isPreconnected
(fun R₀ R₄ ↦
calc
Zigzag R₀ { hw := W₂.comp_mem _ _ R₀.hw (hi _), .. } := Zigzag.of_hom { f := (ι i).app R₀.X₁ }
Zigzag (J := Φ.RightResolution X₂) _ { hw := hi X₂, .. } :=
(Zigzag.of_inv
{ f := ρ.map R₀.w
comm := (i.naturality R₀.w).symm })
Zigzag (J := Φ.RightResolution X₂) _ { hw := W₂.comp_mem _ _ R₄.hw (hi _), .. } :=
(Zigzag.of_hom
{ f := ρ.map R₄.w
comm := (i.naturality R₄.w).symm })
Zigzag _ R₄ := Zigzag.of_inv { f := (ι i).app R₄.X₁ })
constructor
