leftSquareIsPullback — Mathlib

Lean4
/-- Given
```
X₁ - f₁ -> X₂ - f₂ -> X₃
|          |          |
i₁         i₂         i₃
↓          ↓          ↓
Y₁ - g₁ -> Y₂ - g₂ -> Y₃
```
Then the left square is a pullback if the right square and the big square are.
-/
def leftSquareIsPullback (H : IsLimit t₂) (H' : IsLimit (t₂.pasteHoriz t₁ hi₂)) : IsLimit t₁ :=
  by
  apply PullbackCone.isLimitAux'
  intro s
  obtain ⟨l, hl, hl'⟩ :=
    PullbackCone.IsLimit.lift' H' s.fst (s.snd ≫ f₂)
      (by rw [Category.assoc, ← t₂.condition, reassoc_of% s.condition, ← hi₂])
  refine
    ⟨l, hl, ?_, ?_⟩
      -- To check that `l` is compatible with the projections, we use the universal property of `t₂`

  · apply PullbackCone.IsLimit.hom_ext H
    · simp [← s.condition, ← hl, ← t₁.condition, ← hi₂]
    · simpa using hl'
  · intro m hm₁ hm₂
    apply PullbackCone.IsLimit.hom_ext H'
    · simpa [hm₁] using hl.symm
    · simpa [← hm₂] using hl'.symm
Похожие утверждения