map_on_summand — Mathlib

English

The functor Γ₀ sends a chain complex K to a simplicial object, by mapping a Δ to the direct sum of summands Σ_k X_k indexed by Splitting.IndexSet Δ, with the structure maps defined via the above summand maps.

Русский

Функтор Γ₀ отправляет комплекс цепей K в симплициальный объект, сопоставляя каждому Δ прямую сумму сумманд Σ_k X_k, индексируемых Splitting.IndexSet Δ, с структурами отображений, заданными через соответствующие отображения сумманд.

LaTeX

$$$Γ₀.obj(K): Δ \mapsto \bigoplus_{A ∈ Splitting.IndexSet Δ} K.X A.1.len$$$

Lean4

@[reassoc]
theorem map_on_summand {Δ Δ' : SimplexCategoryᵒᵖ} (A : Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') {Δ'' : SimplexCategory}
    {e : Δ'.unop ⟶ Δ''} {i : Δ'' ⟶ A.1.unop} [Epi e] [Mono i] (fac : e ≫ i = θ.unop ≫ A.e) :
    ((Γ₀.splitting K).cofan Δ).inj A ≫ (Γ₀.obj K).map θ =
      Γ₀.Obj.Termwise.mapMono K i ≫ ((Γ₀.splitting K).cofan Δ').inj (Splitting.IndexSet.mk e) :=
  by
  dsimp [Splitting.cofan]
  change (_ ≫ (Γ₀.obj K).map A.e.op) ≫ (Γ₀.obj K).map θ = _
  rw [assoc, ← Functor.map_comp]
  dsimp [splitting]
  rw [Γ₀.Obj.map_on_summand₀ K (Splitting.IndexSet.id A.1)
      (show e ≫ i = ((Splitting.IndexSet.e A).op ≫ θ).unop ≫ 𝟙 _ by rw [comp_id, fac]; rfl)]
  dsimp only [Splitting.IndexSet.id_fst, Splitting.IndexSet.mk, op_unop, Splitting.IndexSet.e]
  rw [Γ₀.Obj.map_on_summand₀ K (Splitting.IndexSet.id (op Δ'')) (show e ≫ 𝟙 Δ'' = e.op.unop ≫ 𝟙 _ by simp),
    Termwise.mapMono_id]
  dsimp only [Splitting.IndexSet.id_fst]
  rw [id_comp]
  rfl

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