English
Variant of IsPullback.of_right where the left-top arrow is induced from a morphism and the right square has the universal property; the conclusion is a pullback for the left-hand square.
Русский
Вариант IsPullback.of_right, когда левый верхний морфизм индуцирован, и правая склейка обладает универсальным свойством; вывод — левый квадрат является пуллбаком.
LaTeX
$$$ (s : IsPullback h_{13} \; v_{11} \; v_{13} \; h_{23}) \; (t : IsPullback h_{12} \; v_{12} \; v_{13} \; h_{22}) \; \\Rightarrow \\\\ IsPullback(h_{11} \\gg h_{13}, v_{11}, v_{12}, h_{21}) $$$
Lean4
/-- Variant of `IsPullback.of_right` where `h₁₁` is induced from a morphism `h₁₃ : X₁₁ ⟶ X₁₃`, and
the universal property of the right square.
The objects fit in the following diagram:
```
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
```
-/
theorem of_right' {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 : IsPullback h₁₃ v₁₁ v₁₃ (h₂₁ ≫ h₂₂))
(t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂) : IsPullback (t.lift h₁₃ (v₁₁ ≫ h₂₁) (by rw [s.w, Category.assoc])) v₁₁ v₁₂ h₂₁ :=
of_right ((t.lift_fst _ _ _) ▸ s) (t.lift_snd _ _ _) t
