English
If i′ and i are mono, then the composition of mapMono in the Γ₀ construction satisfies functorial compatibility: mapMono i ≫ mapMono i′ = mapMono (i′ ≫ i).
Русский
Если i′ и i моно, то композиция mapMono в конструировании Γ₀ удовлетворяет функториальной совместимости: mapMono i ≫ mapMono i′ = mapMono (i′ ≫ i).
LaTeX
$$$mapMono(K,i) \circ mapMono(K,i') = mapMono(K,i'\circ i)$$$
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) :
Sigma.ι (summand K Δ) A ≫ map K θ = Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e) :=
by
simp only [map, colimit.ι_desc, Cofan.mk_ι_app]
have h := SimplexCategory.image_eq fac
subst h
congr
· exact SimplexCategory.image_ι_eq fac
· dsimp only [SimplicialObject.Splitting.IndexSet.pull]
congr
exact SimplexCategory.factorThruImage_eq fac
