mapMono_on_summand_id — Mathlib

English

Compatibility of summand maps with the composition of θ: the map on summand after composing θ with i equals the composition of image.ι with the pullback along θ.

Русский

Совместимость отображений сумманд со сложением θ: отображение на сумманд после компоновки θ с i равно композиции image.ι с вытягиванием через θ.

LaTeX

$$map_on_summand_comp(K, A, θ, i) expresses commutativity of summand maps with map K.map θ.$$

Lean4

@[reassoc]
theorem mapMono_on_summand_id {Δ Δ' : SimplexCategory} (i : Δ' ⟶ Δ) [Mono i] :
    ((splitting K).cofan _).inj (Splitting.IndexSet.id (op Δ)) ≫ (obj K).map i.op =
      Obj.Termwise.mapMono K i ≫ ((splitting K).cofan _).inj (Splitting.IndexSet.id (op Δ')) :=
  Obj.map_on_summand K (Splitting.IndexSet.id (op Δ)) i.op (rfl : 𝟙 _ ≫ i = i ≫ 𝟙 _)

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