ι_mapBifunctor₁₂Desc — Mathlib

English

The equality of the inclusion map ι when indices are transported via π and the accompanying inverse π-map demonstrates a natural compatibility with the π-indexing structure.

Русский

Равенство включения ι при переносе индексов через π и сопряжённая обратная π-мапа демонстрируют естественную совместимость с π-структурой индексации.

LaTeX

$$$ι_{F,G}(...,i_1,i_2,i_3, j) = G.map(ι_{K_1,K_2,F}(...)) \\circ ι_{mapBifunctor}(...).$$$

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₄ i₁ i₂ i₃ j h ≫ mapBifunctor₁₂Desc f = f i₁ i₂ i₃ h := by
  apply GradedObject.ι_mapBifunctor₁₂BifunctorDesc

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