pasteVertIsPullbackEquiv — Mathlib

English

Given that the left square is a pushout, the pasted square is a pushout iff the right square is.

Русский

Если левая клетка является пушпоутом, то вставленная клетка является пушпоутом тогда и только тогда, когда правая клетка является пушпоутом.

LaTeX

$$$\\text{pasteHorizIsPushoutEquiv}(H) : \\IsColimit(t_1) \\to \\IsColimit(t_2) \\text{ is an equivalence}$$$

Lean4

/-- Given that the bottom square is a pullback, the pasted square is a pullback iff the top
square is. -/
def pasteVertIsPullbackEquiv (H : IsLimit t₁) : IsLimit (t₁.pasteVert t₂ hi₂) ≃ IsLimit t₂
    where
  toFun H' := topSquareIsPullback t₂ _ H H'
  invFun H' := pasteVertIsPullback _ H H'
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

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