English
There is a natural transformation ε: coextendScalars f ⋙ restrictScalars f ⇒ Id_{ModuleCat R}, called the counit of the restriction–coextension adjunction. For each X, the component ε_X maps a morphism g to g(1_S) and respects addition and scalar multiplication by S via the structure maps defined in Coextend/Restrict construction.
Русский
Существует естественное преобразование ε: coextendScalars_f ∘ restrictScalars_f ⇒ Id_{ModuleCat R}, называемое кофунктором сопряжённости ограничения и расширения. Для каждого X компонент ε_X отправляет отображение g в g(1_S) и сохраняет сложение и умножение на скаляры через заданные структуры Coextend/Restrict.
LaTeX
$$$$\varepsilon_f: \mathrm{coextendScalars}_f \circ \mathrm{restrictScalars}_f \Rightarrow \mathrm{Id}_{\mathrm{ModuleCat}(R)},\quad ε_X(g) = g(1_S). $$$$
Lean4
/-- The natural transformation from the composition of coextension and restriction of scalars to
identity functor.
-/
@[simps]
protected def counit' : coextendScalars f ⋙ restrictScalars f ⟶ 𝟭 (ModuleCat R) where
-- TODO: after https://github.com/leanprover-community/mathlib4/pull/19511 we need to hint `(X := ...)`.
-- This suggests `restrictScalars` needs to be redesigned.
app
X :=
ofHom (X := (restrictScalars f).obj ((coextendScalars f).obj X))
{ toFun := fun g => g.toFun (1 : S)
map_add' := fun x1 x2 => by
dsimp
rw [LinearMap.add_apply]
map_smul' := fun r (g : (restrictScalars f).obj ((coextendScalars f).obj X)) =>
by
dsimp
rw [CoextendScalars.smul_apply, one_mul, ← LinearMap.map_smul]
congr
change f r = f r • (1 : S)
rw [smul_eq_mul (f r) 1, mul_one] }
