extendRestrictScalarsAdj_unit_app_apply

English

The unit of the adjunction is compatible with morphisms through a naturality condition; specifically, the proof exhibits the equalities comparing the unit’s action against how g transforms under restriction and component maps, ensuring naturality in Y and Y'.

Русский

Единица сопряжённости совместима с морфизмами через натуральность: доказательство демонстрирует равенства действий единицы по отношению к тем, как отображение g трансформируется при ограничении и компоновке компонент.

LaTeX

$$$$ η_Y \circ g = (restrictScalars_f).map( (η_{Y'}) ) \circ η_{Y'} \quad\text{(naturality in } Y,Y') $$$$

Lean4

theorem extendRestrictScalarsAdj_unit_app_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S)
    (M : ModuleCat.{max v u₂} R) (m : M) : (extendRestrictScalarsAdj f).unit.app M m = (1 : S) ⊗ₜ[R,f] m :=
  rfl

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