initial_fst — Mathlib

English

If A and B are cofiltered and L.Initial, then fst L R is initial.

Русский

Если A и B кофильтрованы и L.Initial, то fst L R начальная.

LaTeX

$$$\\\\operatorname{Initial}(\\\\operatorname{fst}(L,R))$$$

Lean4

/-- Let `A` and `B` be cofiltered categories, `L : A ⥤ T` be initial and `R : B ⥤ T`. Then, the
projection `fst L R : Comma L R ⥤ A` is initial. -/
instance initial_fst [IsCofiltered A] [IsCofiltered B] [L.Initial] : (fst L R).Initial :=
  by
  have : ((opFunctor L R).leftOp ⋙ snd R.op L.op).Final := final_equivalence_comp (opEquiv L R).functor.leftOp _
  have : (fst L R).op.Final := final_of_natIso <| opFunctorCompSnd _ _
  apply initial_of_final_op

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