English
The associativity axiom for extendScalars_assoc' expresses that the composite of three successive extension morphisms equals the identity morphism up to the associator and whiskering adjustments.
Русский
Аксиома ассоциативности для extendScalars_assoc' формулирует, что композиция из трёх последовательных отображений расширения равна тождественному отображению с поправками ассоциатора и обрамления.
LaTeX
$$$$ \text{extendScalars_assoc' }(f_1,f_2,f_3) = 𝟙 \;.$$$$
Lean4
@[reassoc]
theorem extendScalars_assoc :
(extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫ Functor.whiskerRight (extendScalarsComp f₁₂ f₂₃).hom _ =
(extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
Functor.whiskerLeft _ (extendScalarsComp f₂₃ f₃₄).hom ≫ (Functor.associator _ _ _).inv :=
by
ext M m
have h₁ := extendScalarsComp_hom_app_one_tmul (f₂₃.comp f₁₂) f₃₄ M m
have h₂ := extendScalarsComp_hom_app_one_tmul f₁₂ (f₃₄.comp f₂₃) M m
have h₃ := extendScalarsComp_hom_app_one_tmul f₂₃ f₃₄
have h₄ := extendScalarsComp_hom_app_one_tmul f₁₂ f₂₃ M m
dsimp at h₁ h₂ h₃ h₄ ⊢
rw [h₁]
erw [h₂]
rw [h₃, ExtendScalars.map_tmul, h₄]
