ι_mapBifunctor₂₃Desc — Mathlib

English

The map that selects the i₁,i₂,i₃-th component of the descended bifunctor commutes with the correspondingDesc map in the target index j.

Русский

Отображение, выбирающее компоненту i₁,i₂,i₃ нижнего бифункторного распада, коммутирует с соответствующимDesc отображением для индекса j.

LaTeX

$$$\iota\; F\; G_{23}\; K_1\; K_2\; K_3\; c_{12}\; c_{23}\; c_4\; j\; h = f$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_mapBifunctor₂₃Desc (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : ComplexShape.r c₁ c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
    ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h ≫ mapBifunctor₂₃Desc c₁₂ f = f i₁ i₂ i₃ h := by
  apply GradedObject.ι_mapBifunctorBifunctor₂₃Desc

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