paste_vert_iff — Mathlib

English

Given a pushout s and an equation e, the two-square pasting equivalence holds between the two possible pushouts.

Русский

Дано пушаут s и уравнение e; существует эквивалентность между двумя возможными пушаутами.

LaTeX

$$$\operatorname{IsPushout}(h_{11}, v_{11}\circ v_{21}, v_{12}\circ v_{22}, h_{31}) \iff \operatorname{IsPushout}(h_{21}, v_{21}, v_{22}, h_{31})$$

Lean4

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

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