ι_mapBifunctorMap — Mathlib

English

The associativity/compatibility lemma for the mapBifunctorDesc with totalDesc.

Русский

Лемма совместимости для mapBifunctorDesc с totalDesc.

LaTeX

$$ι_mapBifunctorDesc {…} : ∀, ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ mapBifunctorDesc f = f i₁ i₂ h$$

Lean4

@[reassoc (attr := simp)]
theorem ι_mapBifunctorMap (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₁ c₂ c (i₁, i₂) = j) :
    ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ (mapBifunctorMap f₁ f₂ F c).f j =
      (F.map (f₁.f i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ ιMapBifunctor L₁ L₂ F c i₁ i₂ j h :=
  by simp [mapBifunctorMap]

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