mapCone_raiseCone — Mathlib

English

In the setting of a CostructuredArrow and a connected index J, mapping a cone under raiseCone preserves the cone structure; equivalently, mapping a cone along the raiseCone construction yields the same cone as the original one when interpreted in the new over-category.

Русский

Для CostructuredArrow и связного индекса J отображение конуса через raiseCone сохраняет структуру конуса; эквивалентно отображение конуса по raiseCone даёт тот же конус в новой категорийной структуре.

LaTeX

$$$ (CostructuredArrow.proj K B).mapCone (raiseCone c) = c$$$

Lean4

theorem mapCone_raiseCone [IsConnected J] {B : D} {F : J ⥤ CostructuredArrow K B}
    (c : Cone (F ⋙ CostructuredArrow.proj K B)) : (CostructuredArrow.proj K B).mapCone (raiseCone c) = c := by cat_disch

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