whiskerVertical_iff — Mathlib

English

If w is GuitartExact and α, β are isomorphisms, then (w.whiskerVertical α β) is GuitartExact.

Русский

Если w имеет точность Гитхарта и α, β — изоморфизмы, то (w.whiskerVertical α β) тоже точен.

LaTeX

$$$[w.GuitartExact] \to \mathrm{GuitartExact}(w.whiskerVertical\, α\, β)$$$

Lean4

/-- A 2-square is Guitart exact iff it is so after replacing the left and right functors by
isomorphic functors. -/
@[simp]
theorem whiskerVertical_iff (α : L ≅ L') (β : R ≅ R') : (w.whiskerVertical α.hom β.inv).GuitartExact ↔ w.GuitartExact :=
  by
  constructor
  · intro h
    have : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom :=
      by
      ext X₁
      simp only [Functor.comp_obj, whiskerVertical_app, assoc, Iso.hom_inv_id_app_assoc, ← B.map_comp,
        Iso.hom_inv_id_app, B.map_id, comp_id]
    rw [this]
    exact whiskerVertical (w.whiskerVertical α.hom β.inv) α.symm β.symm
  · intro h
    exact whiskerVertical w α β

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