lightToProfinite_map_proj_eq — Mathlib

English

Equality between the image of a projection under lightToProfinite and the corresponding projection in the limit cone of the diagram.

Русский

Равенство между образом проекции в lightToProfinite и соответствующей проекции в предельном конусе диаграммы.

LaTeX

$$$$ lightToProfinite.map (S.proj n) = (lightToProfinite.obj S).asLimitCone.\\pi.app \\langle n \\rangle $$$$

Lean4

theorem lightToProfinite_map_proj_eq (n : ℕ) :
    lightToProfinite.map (S.proj n) = (lightToProfinite.obj S).asLimitCone.π.app _ :=
  by
  simp only [Functor.comp_obj, toCompHausLike_map]
  let c : Cone (S.diagram ⋙ lightToProfinite) := S.toLightDiagram.cone
  let hc : IsLimit c := S.toLightDiagram.isLimit
  exact liftedLimitMapsToOriginal_inv_map_π hc _

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