toPullbackTerminal — Mathlib

English

If every morphism F.obj a → X is relatively representable (with respect to F), then the diagonal morphism diag X: X → X × X is relatively representable with respect to F (under appropriate limit-preserving hypotheses).

Русский

Если каждый мороморфизм F.obj a → X относительно представим по F, то диагональный морфизм diag X: X → X × X также относительно представим по F (при выполнении соответствующих условий сохранения пределов).

LaTeX

$$$\Big(\forall a:\, C\,\forall g:\, F.obj(a)\to X,\ F\relativelyRepresentable(g)\Big) \Rightarrow F\relativelyRepresentable(\mathrm{diag}(X))$$$

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 a morphism `g : F.obj a ⟶ pullback (terminal.from X) (terminal.from X)`,
the canonical morphism from `F.obj a` to
`pullback ((g ≫ pullback.fst _ _) ≫ terminal.from X) ((g ≫ pullback.snd _ _) ≫ terminal.from X)`
is relatively representable with respect to `F`.
-/
theorem toPullbackTerminal {X : D} {a : C} [HasPullbacks C] [PreservesLimitsOfShape WalkingCospan F]
    (g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)) :
    F.relativelyRepresentable
      (pullback.lift (f := (g ≫ pullback.fst _ _) ≫ terminal.from X) (g := (g ≫ pullback.snd _ _) ≫ terminal.from X)
        (𝟙 _) (𝟙 _) (by cat_disch)) :=
  by
  let pbIso :=
    pullback.congrHom (terminal.comp_from _ : (g ≫ pullback.fst _ _) ≫ terminal.from X = terminal.from _)
        (terminal.comp_from _ : (g ≫ pullback.snd _ _) ≫ terminal.from X = terminal.from _) ≪≫
      (prodIsoPullback _ _).symm ≪≫
        (HasLimit.isoOfNatIso (pairComp _ _ _)).symm ≪≫ (preservesLimitIso _ (pair _ _)).symm
  rw [← comp_id (pullback.lift _ _), ← pbIso.hom_inv_id, ← Category.assoc]
  apply (respectsIso F).toRespectsRight.postcomp _ (inferInstance : IsIso _) _
  exact map_preimage F (_ ≫ pbIso.hom) ▸ map F (F.preimage _)

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