map_on_summand₀' — Mathlib

English

Let i: Δ' → Δ be mono and A an index set summand; then the map on summand is given by a canonical factorization through image, i.e., Sigma.ι composed with map is equal to the induced map on the summand via image.ι.

Русский

Пусть i: Δ' → Δ моно и A—индексный суммант; тогда отображение на сумманду задаётся через каноническое разложение через образ: Σι ∘ map = image.ι через соответствующий индуктивный мэп.

LaTeX

$$$\Sigma\!\iota_A \circ map = image.\iota_{(θ.unop \circ A.e)} \circ \Sigma\iota_A$$$

Lean4

@[reassoc]
theorem map_on_summand₀' {Δ Δ' : SimplexCategoryᵒᵖ} (A : Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') :
    Sigma.ι (summand K Δ) A ≫ map K θ =
      Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫ Sigma.ι (summand K _) (A.pull θ) :=
  map_on_summand₀ K A (A.fac_pull θ)

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