map_on_summand' — Mathlib

English

The action of Γ₀ on morphisms is defined by composing the direct-sum components after applying f.f to each summand and then reassembling via Γ₀.splitting.

Русский

Действие Γ₀ на морфизмах задаётся через композицию компонентов прямой суммы после применения f.f к каждой суммандной части и повторную сборку через Γ₀.splitting.

LaTeX

$$$Γ₀.map(f): Δ \mapsto Σ (f.f A.1.unop.len) ≫ Γ₀.splitting.K inj A$$$

Lean4

@[reassoc]
theorem map_on_summand' {Δ Δ' : SimplexCategoryᵒᵖ} (A : Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') :
    ((splitting K).cofan Δ).inj A ≫ (obj K).map θ =
      Obj.Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫ ((splitting K).cofan Δ').inj (A.pull θ) :=
  by
  apply Obj.map_on_summand
  apply image.fac

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