English
If a1, a2 : A → Y form a kernel pair for g : Y → Z, then after pulling back along f : X → Z, the induced projections A ×_Z X → X form a kernel pair for the map Y ×_Z X → X.
Русский
Если a1, a2 : A → Y образуют пару ядра для g : Y → Z, то после взятия пулбэка вдоль f : X → Z полученные проекции A ×_Z X → X образуют пару ядра для отображения Y ×_Z X → X.
LaTeX
$$$\\forall X,Y,Z,A,g,f\\;\\bigl(\\operatorname{IsKernelPair}(g,a_1,a_2) \\Rightarrow \\operatorname{IsKernelPair}(\\mathrm{pullback.fst}(f,g),\\mathrm{pullback.map}(f,\\_,\\_,\\_,\\mathbf{1}_X,a_1,\\mathbf{1}_Z,\\text{?}) ,\\mathrm{pullback.map}(\\_,\\_,\\_,\\_,\\mathbf{1}_X,a_2,\\mathbf{1}_Z,\\text{?}))\\bigr).$$$
Lean4
/-- If `a₁ a₂ : A ⟶ Y` is a kernel pair for `g : Y ⟶ Z`, then `a₁ ×[Z] X` and `a₂ ×[Z] X`
(`A ×[Z] X ⟶ Y ×[Z] X`) is a kernel pair for `Y ×[Z] X ⟶ X`. -/
protected theorem pullback {X Y Z A : C} {g : Y ⟶ Z} {a₁ a₂ : A ⟶ Y} (h : IsKernelPair g a₁ a₂) (f : X ⟶ Z)
[HasPullback f g] [HasPullback f (a₁ ≫ g)] :
IsKernelPair (pullback.fst f g) (pullback.map f _ f _ (𝟙 X) a₁ (𝟙 Z) (by simp) <| Category.comp_id _)
(pullback.map _ _ _ _ (𝟙 X) a₂ (𝟙 Z) (by simp) <| (Category.comp_id _).trans h.1.1) :=
by
refine
⟨⟨by rw [pullback.lift_fst, pullback.lift_fst]⟩,
⟨PullbackCone.isLimitAux _
(fun s =>
pullback.lift (s.fst ≫ pullback.fst _ _) (h.lift (s.fst ≫ pullback.snd _ _) (s.snd ≫ pullback.snd _ _) ?_)
?_)
(fun s => ?_) (fun s => ?_) (fun s (m : _ ⟶ pullback f (a₁ ≫ g)) hm => ?_)⟩⟩
· simp_rw [Category.assoc, ← pullback.condition, ← Category.assoc, s.condition]
· simp only [assoc, lift_fst_assoc, pullback.condition]
· ext <;> simp
· ext
· simp [s.condition]
· simp
· apply pullback.hom_ext
· simpa using hm WalkingCospan.left =≫ pullback.fst f g
· apply PullbackCone.IsLimit.hom_ext h.isLimit
· simpa using hm WalkingCospan.left =≫ pullback.snd f g
· simpa using hm WalkingCospan.right =≫ pullback.snd f g
