cone_π_app_comp_Pi_π_neg — Mathlib

English

Analogous compatibility result on the negative side: for m and n with m ≥ n, the projection through the cone to N_m commutes with the corresponding Pi-map to N_n.

Русский

Аналогично на отрицательной стороне: для m ≥ n проекция через конус к N_m коммутирует с соответствующим Pi-отображением к N_n.

LaTeX

$$$\\forall m\\ge n:\\; (\\mathrm{cone }\\ f)\\pi_{m} \\circ \\mathrm{Pi}.\\pi_n = \\mathrm{Pi}.\\pi_n \\circ (f_n) $$$

Lean4

@[reassoc]
theorem cone_π_app_comp_Pi_π_neg (m n : ℕ) (h : ¬(n < m)) :
    (cone f).π.app ⟨m⟩ ≫ Pi.π _ n = Pi.π _ n ≫ f n ≫ eqToHom (functorObj_eq_neg h).symm :=
  by
  simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, limMap_π,
    Discrete.functor_obj_eq_as, Discrete.natTrans_app]
  rw [dif_neg h]

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