English
If Φ.IsRightDerivabilityStructure, then TwoSquare.GuitartExact ((Φ.catCommSq L₁ L₂).iso).hom.
Русский
Если Φ обладает правой деривируемостью, то TwoSquare.GuitartExact для соответствующего изоморфизма существует.
LaTeX
$$$[\Phi.IsRightDerivabilityStructure] \Rightarrow TwoSquare.GuitartExact\big((\Phi.catCommSq L_1 L_2).iso\big).hom$$$
Lean4
theorem isConnected :
IsConnected
((TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 _) (Functor.rightUnitor _).inv).CostructuredArrowDownwards y) :=
by
let w := (TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 _) (Functor.rightUnitor _).inv)
have : Nonempty (w.CostructuredArrowDownwards y) := ⟨(fromRightResolution Φ L y).obj (Classical.arbitrary _)⟩
suffices ∀ (X : w.CostructuredArrowDownwards y), ∃ Y, Zigzag X ((fromRightResolution Φ L y).obj Y)
by
refine zigzag_isConnected (fun X X' => ?_)
obtain ⟨Y, hX⟩ := this X
obtain ⟨Y', hX'⟩ := this X'
exact hX.trans ((zigzag_obj_of_zigzag _ (isPreconnected_zigzag Y Y')).trans hX'.symm)
intro X
obtain ⟨c, g, x, fac, rfl⟩ := TwoSquare.CostructuredArrowDownwards.mk_surjective X
dsimp [w] at x fac
rw [id_comp] at fac
let ρ : Φ.arrow.RightResolution (Arrow.mk g) := Classical.arbitrary _
refine ⟨RightResolution.mk ρ.w.left ρ.hw.1, ?_⟩
have :=
zigzag_obj_of_zigzag (fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac)
(isPreconnected_zigzag (RightResolution.mk (𝟙 _) (W₂.id_mem _)) (RightResolution.mk ρ.w.right ρ.hw.2))
refine Zigzag.trans ?_ (Zigzag.trans this ?_)
· exact Zigzag.of_hom (eqToHom (by simp))
· apply Zigzag.of_inv
refine CostructuredArrow.homMk (StructuredArrow.homMk ρ.X₁.hom (by simp)) ?_
ext
dsimp
rw [← cancel_epi (isoOfHom L W₂ ρ.w.left ρ.hw.1).hom, isoOfHom_hom, isoOfHom_hom_inv_id_assoc, ← L.map_comp_assoc,
Arrow.w_mk_right, Arrow.mk_hom, L.map_comp, assoc, isoOfHom_hom_inv_id_assoc, fac]
