English
There is a natural operation that precomposes a MorphComponents object with a morphism of simplicial objects. Given f : MorphComponents X n Z and g : X' ⟶ X, one obtains a MorphComponents X' n Z with components a' and b'i defined by a' = g.app(op ⟨n+1⟩) ∘ f.a and b'i = g.app(op ⟨n⟩) ∘ f.b i.
Русский
Существует естественная операция предкомпонования MorphComponents морфизмом между симплициальными объектами. Пусть f : MorphComponents X n Z и g : X' ⟶ X, тогда получается MorphComponents X' n Z с компонентами a' и b'i, заданными как a' = g.app(op ⟨n+1⟩) ∘ f.a и b'i = g.app(op ⟨n⟩) ∘ f.b i.
LaTeX
$$$\\text{preComp}(f,g) : \\text{MorphComponents } X' n Z \\quad\\text{with}\\quad(\\text{preComp}(f,g)).a = g.\\mathrm{app}(\\mathrm{op}(\\langle n+1\\rangle)) \\circ f.a,\quad (\\text{preComp}(f,g)).b_i = g.\\mathrm{app}(\\mathrm{op}(\\langle n\\rangle)) \\circ f.b_i.$$$
Lean4
/-- A `MorphComponents` can be precomposed with a morphism of simplicial objects. -/
@[simps]
def preComp : MorphComponents X' n Z where
a := g.app (op ⦋n + 1⦌) ≫ f.a
b i := g.app (op ⦋n⦌) ≫ f.b i
