English
Special case of map_epi_on_summand_id: for Δ, Δ' equal, the induced map is the identity on summands. This mirrors the identity behavior for simplicial maps on identical objects.
Русский
Особый случай map_epi_on_summand_id: при Δ = Δ′ отображение на сумманду есть тождество. Это соответствует идентичному поведению отображений на суммандах.
LaTeX
$$map_epi_on_summand_id(K,i) = Id$$
Lean4
/-- The functor `Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C`, on objects. -/
@[simps]
def obj (K : ChainComplex C ℕ) : SimplicialObject C
where
obj Δ := Obj.obj₂ K Δ
map θ := Obj.map K θ
map_id
Δ :=
colimit.hom_ext
(fun ⟨A⟩ => by
dsimp
have fac : A.e ≫ 𝟙 A.1.unop = (𝟙 Δ).unop ≫ A.e := by rw [unop_id, comp_id, id_comp]
rw [Obj.map_on_summand₀ K A fac, Obj.Termwise.mapMono_id, id_comp]
dsimp only [Obj.obj₂]
rw [comp_id]
rfl)
map_comp {Δ'' Δ' Δ} θ'
θ :=
colimit.hom_ext
(fun ⟨A⟩ => by
have fac : θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e := by rw [unop_comp, assoc]
rw [← image.fac (θ'.unop ≫ A.e), ← assoc, ← image.fac (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)), assoc] at fac
simp only [Obj.map_on_summand₀'_assoc K A θ', Obj.map_on_summand₀' K _ θ, Obj.Termwise.mapMono_comp_assoc,
Obj.map_on_summand₀ K A fac]
rfl)
