unit' — Mathlib

English

There is a natural transformation η: Id_{ModuleCat S} ⇒ restrictScalars f ⋙ coextendScalars f, called the unit of the restriction–coextension adjunction. At each object Y, η_Y is the canonical morphism coming from app' f Y, i.e., it embeds Y into the composed functor via the forgetful/extension construction.

Русский

Существует естественное преобразование η: Id_{ModuleCat S} ⇒ ограничение по скалярам f затем расширение скаляров f, называемое единицей сопряжённости ограничения и расширения. На каждом объекте Y компонент η_Y — канонический морфизм, получаемый из app' f Y.

LaTeX

$$$$\text{unit}'_f: \mathrm{Id}_{\mathrm{ModuleCat}(S)} \Rightarrow \mathrm{restrictScalars}_f \circ \mathrm{coextendScalars}_f,\quad \text{с компонентой } Y:\quad η_Y = \text{app}' f Y. $$$$

Lean4

/-- The natural transformation from identity functor to the composition of restriction and coextension
of scalars.
-/
@[simps]
protected noncomputable def unit' : 𝟭 (ModuleCat S) ⟶ restrictScalars f ⋙ coextendScalars f
    where
  app Y := ofHom (app' f Y)
  naturality Y Y'
    g :=
    hom_ext <|
      LinearMap.ext fun y : Y =>
        LinearMap.ext fun s : S => by
          -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): previously simp [CoextendScalars.map_apply]

          simp only [ModuleCat.hom_comp, Functor.id_map, Functor.id_obj, Functor.comp_obj, Functor.comp_map,
            LinearMap.coe_comp, Function.comp, CoextendScalars.map_apply, restrictScalars.map_apply f]
          change s • (g y) = g (s • y)
          rw [map_smul]

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