vComp — Mathlib

English

If two composable two-square configurations are individually Guitart exact, then their vertical composition is again Guitart exact.

Русский

Если два связанных двумя квадратами наборы отображений обладающих свойством Guitart Exact на каждом элементе, то их вертикальная композиция также имеет свойство Guitart Exact.

LaTeX

$$$ \\text{GuitartExact}(w) \\land \\text{GuitartExact}(w') \\Rightarrow \\text{GuitartExact}(w \\gg_v w') $$$

Lean4

instance vComp [hw : w.GuitartExact] [hw' : w'.GuitartExact] : (w ≫ᵥ w').GuitartExact :=
  by
  simp only [TwoSquare.guitartExact_iff_initial]
  intro Y₁
  rw [← Functor.initial_natIso_iff (structuredArrowDownwardsComp w w' Y₁)]
  infer_instance

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