vComp'_iff_of_equivalences — Mathlib

English

Similarly, when using equivalences in the refined vertical composition, the Guitart exactness is preserved if and only if the original square is Guitart exact.

Русский

Аналогично при более точной вертикальной композиции с эквивалентностями, точность Guitart сохраняется тогда и только тогда, когда исходный квадрат — Guitart точен.

LaTeX

$$$ (w.vComp' w'.hom eL eR).GuitartExact \\iff w.GuitartExact $$$

Lean4

theorem vComp'_iff_of_equivalences (E : C₂ ≌ C₃) (E' : D₂ ≌ D₃) (w' : H₂ ⋙ E'.functor ≅ E.functor ⋙ H₃) {L₁₂ : C₁ ⥤ C₃}
    {R₁₂ : D₁ ⥤ D₃} (eL : L₁ ⋙ E.functor ≅ L₁₂) (eR : R₁ ⋙ E'.functor ≅ R₁₂) :
    (w.vComp' w'.hom eL eR).GuitartExact ↔ w.GuitartExact := by
  rw [← vComp_iff_of_equivalences w E E' w', TwoSquare.vComp', whiskerVertical_iff]

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