arrowMap_restrictionLE — Mathlib

English

If F is a functor on Set.Iic j and j′ ≤ j, then restricting F along j′ yields an arrowMap that equals the corresponding arrowMap with the adjusted witness: arrowMap (restrictionLE F hj′) i1 i2 h12 h2 = arrowMap F i1 i2 h12 (h2.trans hj′).

Русский

Если F — функтор на Set.Iic j и j′ ≤ j, то ограничение F по j′ даёт стрелку, равную соответствующей стрелке с учётом нового доказательства: arrowMap (restrictionLE F hj′) i1 i2 h12 h2 = arrowMap F i1 i2 h12 (h2.trans hj′).

LaTeX

$$$ \\operatorname{arrowMap}(\\operatorname{restrictionLE} F hj')\, i_1\, i_2\, h_{12}\, h_2 = \\operatorname{arrowMap} F\, i_1\, i_2\, h_{12}\, (h_2 \\circ hj') $$$

Lean4

theorem arrowMap_restrictionLE {j : J} (F : Set.Iic j ⥤ C) {j' : J} (hj' : j' ≤ j) (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂)
    (h₂ : i₂ ≤ j') : arrowMap (restrictionLE F hj') i₁ i₂ h₁₂ h₂ = arrowMap F i₁ i₂ h₁₂ (h₂.trans hj') :=
  rfl

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