English
Variant of IsPullback.of_bot, where the left-vertical edge is induced from a morphism and the bottom square carries the universal property; yields a pullback for the entire diagram.
Русский
Вариант IsPullback.of_bot, когда левый столбец индуцирован, а нижний квадрат имеет универсальное свойство; получается пуллбак всей диаграммы.
LaTeX
$$$ (s : IsPullback h_{11} \\; v_{3} \\; v_{12} \\; h_{31}) \\; (t : IsPullback h_{21} \\; v_{21} \\; v_{22} \\; h_{31}) \\Rightarrow IsPullback(h_{11}, v_{13} , v_{12}, h_{21}) $$$
Lean4
/-- Variant of `IsPullback.of_bot`, where `v₁₁` is induced from a morphism `v₃₁ : X₁₁ ⟶ X₃₁`, and
the universal property of the bottom square.
The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
```
-/
theorem of_bot' {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 : IsPullback h₁₁ v₃₁ (v₁₂ ≫ v₂₂) h₃₁)
(t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁) : IsPullback h₁₁ (t.lift (h₁₁ ≫ v₁₂) v₃₁ (by rw [Category.assoc, s.w])) v₁₂ h₂₁ :=
of_bot ((t.lift_snd _ _ _) ▸ s) (by simp only [lift_fst]) t
