English
Another presentation of the compatibility between inclusion ι and the first differential D1 in the three-variable setting.
Русский
Еще одно выражение совместимости между инклюзией ι и первым дифференциалом D1 в трёхпеременной настройке.
LaTeX
$$$\iota F_{1 2} G K_1 K_2 K_3 c_{1 2} c_4 i_1 i_2 i_3 j \;\Rightarrow\; D_1 F G K_1 K_2 K_3 c_{1 2} c_4 j j' = d_1 F G K_1 K_2 K_3 c_{1 2} c_4 i_1 i_2 i_3 j'$$$
Lean4
/-- Auxiliary definition for `mapBifunctorShift₁Iso`. -/
@[simps! hom_f_f inv_f_f]
def mapBifunctorHomologicalComplexShift₁Iso :
((F.mapBifunctorHomologicalComplex _ _).obj (K₁⟦x⟧)).obj K₂ ≅
(HomologicalComplex₂.shiftFunctor₁ D x).obj (((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj K₂) :=
HomologicalComplex.Hom.isoOfComponents (fun _ => Iso.refl _)
(by
intros
ext
dsimp
simp only [Linear.comp_units_smul, id_comp, Functor.map_units_smul, NatTrans.app_units_zsmul, comp_id])
