English
The associativity-compatible hom equivalence for extend/restrict interactions is given by a precise equality between two morphisms, built from the components of extendRestrictScalarsAdj and the corresponding whisks and inverses.
Русский
Единичная эквивалентность гом-отношений для взаимодействий расширения и ограничения выражается точным тождеством между двумя морфизмами, построенными по компонентам extendRestrictScalarsAdj и соответствующим whiskers/обратными отображениями.
LaTeX
$$$$ \text{extendScalars_assoc'}(M) = \text{identity via whiskering/naturality} $$$$
Lean4
/-- The associativity compatibility for the extension of scalars, in the exact form
that is needed in the definition `CommRingCat.moduleCatExtendScalarsPseudofunctor`
in the file `Algebra.Category.ModuleCat.Pseudofunctor` -/
theorem extendScalars_assoc' :
(extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
Functor.whiskerRight (extendScalarsComp f₁₂ f₂₃).hom _ ≫
(Functor.associator _ _ _).hom ≫
Functor.whiskerLeft _ (extendScalarsComp f₂₃ f₃₄).inv ≫ (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).inv =
𝟙 _ :=
by
rw [extendScalars_assoc_assoc]
simp only [Iso.inv_hom_id_assoc, ← Functor.whiskerLeft_comp_assoc, Iso.hom_inv_id, Functor.whiskerLeft_id',
Category.id_comp]
