pre_map' — Mathlib

English

For F, and E₁, E₂ : K ⥤ J with α : E₁ ⟶ E₂, we have colimit.pre F E₁ = colim.map (whiskerRight α F) ≫ colimit.pre F E₂.

Русский

Пусть F : J ⥤ C, и E₁, E₂ : K ⥤ J, α : E₁ ⟶ E₂. Тогда colimit.pre F E₁ = colim.map (whiskerRight α F) ≫ colimit.pre F E₂.

LaTeX

$$$ \\operatorname{colimit.pre} F E_1 = \\operatorname{colim.map} (\\mathrm{whiskerRight} \\alpha F) \\; \\circ \\operatorname{colimit.pre} F E_2 $$$

Lean4

theorem pre_map' [HasColimitsOfShape K C] (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
    colimit.pre F E₁ = colim.map (whiskerRight α F) ≫ colimit.pre F E₂ :=
  by
  ext1
  simp

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