paste_horiz_iff — Mathlib

English

A variant of the top-pushout theorem expresses the bottom square as a pushout when the top is given by a certain composed pushout and a commuting condition holds.

Русский

Вариант теоремы о пушауте сверху: нижний квадрат является пушаутом при выполнении условий сопряжённости верха.

LaTeX

$$$\operatorname{IsPushout}(h_{21}, v_{21}, v_{22}, h_{31})$$$

Lean4

theorem paste_horiz_iff {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂}
    {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃} (s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁)
    (e : h₁₂ ≫ v₁₃ = v₁₂ ≫ h₂₂) : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂) ↔ IsPushout h₁₂ v₁₂ v₁₃ h₂₂ :=
  ⟨fun h => h.of_left e s, s.paste_horiz⟩

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