ιFunctorObj_extension — Mathlib

English

There exists a canonical extension ιFunctorObj for the functor index along a morphism between A and B indexed families, yielding a morphism fitting the commutation constraints with projections πFunctorObj.

Русский

Существует каноническое продолжение ιFunctorObj для функторного индекса между семействами A и B, дающее морфизм, удовлетворяющий диагональной совместимости с проекциями πFunctorObj.

LaTeX

$$∃ l: B_i ⟶ functorObj f πX, f i ≫ l = t ≫ ιFunctorObj f πX ∧ l ≫ πFunctorObj f πX = b$$

Lean4

theorem ιFunctorObj_extension {i : I} (t : A i ⟶ X) (b : B i ⟶ S) (sq : CommSq t (f i) πX b) :
    ∃ (l : B i ⟶ functorObj f πX), f i ≫ l = t ≫ ιFunctorObj f πX ∧ l ≫ πFunctorObj f πX = b :=
  ⟨Sigma.ι (functorObjTgtFamily f πX) (FunctorObjIndex.mk i t b sq.w) ≫ ρFunctorObj f πX,
    (FunctorObjIndex.mk i t b _).comm, by simp⟩

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