of_prod_fst_with_id — Mathlib

English

A canonical pullback for prod.fst and prod.map(f, id_X) is obtained for any product X.

Русский

Канонический пуллбак для prod.fst и prod.map(f, id_X) существует для любого произведения X.

LaTeX

$$$ IsPullback(prod.fst, prod.map f (id_X), f, prod.fst) $$$

Lean4

/-- In a category, given a morphism `f : A ⟶ B` and an object `X`,
this is the obvious pullback diagram:
```
A ⨯ X ⟶ A
  |     |
  v     v
B ⨯ X ⟶ B
```
-/
theorem of_prod_fst_with_id {A B : C} (f : A ⟶ B) (X : C) [HasBinaryProduct A X] [HasBinaryProduct B X] :
    IsPullback prod.fst (prod.map f (𝟙 X)) f prod.fst where
  isLimit' :=
    ⟨PullbackCone.isLimitAux' _
        (fun s ↦ by
          refine ⟨prod.lift s.fst (s.snd ≫ prod.snd), ?_, ?_, ?_⟩
          · simp
          · ext
            · simp [PullbackCone.condition]
            · simp
          · intro m h₁ h₂
            dsimp at m h₁ h₂ ⊢
            ext
            · simpa using h₁
            · simp [← h₂])⟩

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