ι_D₁ — Mathlib

English

There is a canonical isomorphism between mapBifunctor (K1⟦x⟧) K2 F and (mapBifunctor K1 K2 F)⟦x⟧, for integer shift x.

Русский

Существует каноническое изоморфизм между mapBifunctor (K1⟦x⟧) K2 F и (mapBifunctor K1 K2 F)⟦x⟧, для целочисленного сдвига x.

LaTeX

$$$ mapBifunctor (K_1 \llbracket x \rrbracket) K_2 F \cong (mapBifunctor K_1 K_2 F) \llbracket x \rrbracket $$$

Lean4

@[reassoc (attr := simp)]
theorem ι_D₁ [HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] :
    ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' = d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j' := by
  simp [D₁]

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