initial_snd — Mathlib

English

Let A and B be filtered categories, L: A ⥤ T be initial and R: B ⥤ T. Then the induced functor snd L R: Comma L R ⥤ B is initial.

Русский

Пусть A и B — фильтрованные категории, L: A ⥤ T начальный, R: B ⥤ T. Тогда проекция snd L R: Comma L R → B начальна.

LaTeX

$$$\\\\operatorname{Initial}(\\\\mathrm{snd}(L,R))$$$

Lean4

instance initial_snd [L.Initial] : (snd L R).Initial :=
  by
  have : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Final :=
    final_equivalence_comp (opEquiv L R).functor.leftOp (fst R.op L.op)
  have : (snd L R).op.Final := final_of_natIso (opFunctorCompFst _ _)
  apply initial_of_final_op

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