English
Assume C has binary products, D has pullbacks, binary products, and a terminal object, and F: C ⥤ D is full and preserves binary products. For any X in D, if the canonical map from F(a) to pullback(terminal.from(X), terminal.from(X)) along a chosen map g: F.obj a → pullback(...) is relatively representable with respect to F, then the induced map into that pullback is also representable in this sense.
Русский
Пусть C имеет бинарные произведения, D имеет pullbacks, бинарные произведения и терминальный объект, и F: C ⥤ D полно и сохраняет бинарные произведения. Для любого X в D, если каноническое отображение из F(a) в pullback(terminal.from(X), terminal.from(X)) вдоль выбранного отображения g: F.obj a → pullback(...) относительно E представимо по F, то соответствующее отображение в этот pullback тоже является относительно представленным по F.
LaTeX
$$$\text{Let }F: C\to D\text{ be full and preserve binary products. If }\exists a: C\text{ and }g: F(a)\to \mathrm{pullback}(\mathrm{terminal.from}(X), \mathrm{terminal.from}(X))\text{ with } F\text{ relativelyRepresentable (pullback.lift...)}.$$$
Lean4
/-- Assume that
1. `C` has binary products,
2. `D` has pullbacks, binary products and a terminal object, and
3. `F : C ⥤ D` is full and preserves binary products.
For an object `X` in a category `D`, if the diagonal morphism `X ⟶ X × X` is relatively
representable, then every morphism of the form `F.obj a ⟶ X` is relatively representable with
respect to `F`.
-/
theorem of_diag {X : D} (h : F.relativelyRepresentable (Limits.diag X)) ⦃a : C⦄ (g : F.obj a ⟶ X) :
F.relativelyRepresentable g :=
by
rw [(by cat_disch : Limits.diag X = pullback.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).inv)] at h
intro a' g'
obtain ⟨_, ⟨left⟩⟩ := pullback_map_diagonal_isPullback g g' (terminal.from X)
let prodMap : F.obj (a ⨯ a') ⟶ X ⨯ X :=
(preservesLimitIso _ (pair _ _) ≪≫ HasLimit.isoOfNatIso (pairComp _ _ _)).hom ≫ prod.map g g'
let pbRepr :=
(h prodMap).choose_spec.choose_spec.choose_spec.isLimit'.some.conePointUniqueUpToIso <|
pasteHorizIsPullback rfl
(IsPullback.of_vert_isIso_mono (snd :=
pullback.congrHom (terminal.comp_from g) (terminal.comp_from g') ≪≫
(prodIsoPullback _ _).symm ≪≫
(HasLimit.isoOfNatIso (pairComp _ _ _)).symm ≪≫ (preservesLimitIso _ (pair _ _)).symm |>.hom)
⟨by cat_disch⟩).isLimit'.some
left
exact
⟨_,
⟨_,
⟨_,
IsPullback.of_iso_pullback (fst := pbRepr.hom ≫ pullback.fst g g') (snd :=
F.map (Functor.preimage F (pbRepr.hom ≫ pullback.snd g g'))) ⟨by simp [pullback.condition]⟩ pbRepr
(by cat_disch) (by cat_disch)⟩⟩⟩
