English
The diagonal diag X is relatively representable with respect to F if and only if every morphism F.obj a → X is relatively representable with respect to F.
Русский
Диагональ диагонал X относительно представима по F тогда и только тогда, когда каждый мороморфизм F.obj a → X относительно представлен по F.
LaTeX
$$$F\relativelyRepresentable(\mathrm{diag}(X)) \iff \forall a:\, C, \forall g:\, F.obj(a)\to X,\ F.relativelyRepresentable(g).$$$
Lean4
/-- Assume that
1. `C` has binary products and pullbacks,
2. `D` has pullbacks, binary products and a terminal object, and
3. `F : C ⥤ D` is full and preserves binary products and pullbacks.
For an object `X` in a category `D`, if every morphism of the form `F.obj a ⟶ X` is relatively
representable with respect to `F`, so is the diagonal morphism `X ⟶ X × X`.
-/
theorem diag_of_map_from_obj [HasPullbacks C] [PreservesLimitsOfShape WalkingCospan F] {X : D}
(h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g) : F.relativelyRepresentable (Limits.diag X) :=
by
rw [(by cat_disch : Limits.diag X = pullback.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).inv)]
suffices F.relativelyRepresentable (pullback.lift (𝟙 _) (𝟙 _)) from
(respectsIso F).toRespectsRight.postcomp _ (inferInstance : IsIso _) _ this
intro a g
obtain ⟨_, ⟨_, ⟨_, pbRepr⟩⟩⟩ := h (g ≫ pullback.fst _ _) (g ≫ pullback.snd _ _)
obtain ⟨_, ⟨bot⟩⟩ :=
IsPullback.of_iso_pullback ⟨by rw [assoc]; simp [pullback.condition]⟩
(pbRepr.isoPullback ≪≫
(pullbackDiagonalMapIdIso (g ≫ pullback.fst _ _) (g ≫ pullback.snd _ _) (terminal.from X)).symm)
rfl rfl
obtain ⟨_, ⟨_, ⟨topMap, top⟩⟩⟩ :=
(toPullbackTerminal g) <|
(pbRepr.isoPullback ≪≫
(pullbackDiagonalMapIdIso (g ≫ pullback.fst _ _) (g ≫ pullback.snd _ _) (terminal.from X)).symm).hom ≫
pullback.snd (pullback.diagonal (terminal.from X))
(pullback.map _ _ _ _ _ _ (𝟙 _) (by cat_disch) (by cat_disch))
have hg :
g =
pullback.lift (𝟙 _) (𝟙 _) (by cat_disch) ≫
pullback.map ((g ≫ pullback.fst _ _) ≫ terminal.from X) ((g ≫ pullback.snd _ _) ≫ terminal.from X) _ _
(g ≫ pullback.fst _ _) (g ≫ pullback.snd _ _) (𝟙 _) (by cat_disch) (by cat_disch) :=
by apply Limits.pullback.hom_ext <;> simp
exact
hg ▸
⟨_,
⟨_, ⟨_, IsPullback.of_isLimit <| pasteVertIsPullback rfl bot (map_preimage F topMap ▸ top).flip.isLimit'.some⟩⟩⟩
