φ — Mathlib · SciLib

English

For a morphism f: X ⟶ Y, the nth component φ f n is the composite of the nth distinguished summand inclusion with f evaluated in degree n.

Русский

Для морфизма f: X → Y n-й компонент φ f n есть композиция включения из n-й выделенной подсуммы с f в степени n.

LaTeX

$$$\phi(f,n) = s.ι n \;\circ\; f.app(\mathrm{op}(\langle n \rangle))$$$

Lean4

/-- As it is stated in `Splitting.hom_ext`, a morphism `f : X ⟶ Y` from a split
simplicial object to any simplicial object is determined by its restrictions
`s.φ f n : s.N n ⟶ Y _⦋n⦌` to the distinguished summands in each degree `n`. -/
@[simp]
def φ (f : X ⟶ Y) (n : ℕ) : s.N n ⟶ Y _⦋n⦌ :=
  s.ι n ≫ f.app (op ⦋n⦌)

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