fromRestriction_hom_apply_apply — Mathlib

English

For any g: (restrictScalars f).obj Y ⟶ X and y ∈ Y, s ∈ S, the hom component of the restriction adjunction is given by (HomEquiv.fromRestriction f g).hom y s = g (s • y).

Русский

Для любого g: (restrictScalars f).obj Y ⟶ X и элементов y ∈ Y, s ∈ S, компоненты гомоморфизма вида HomEquiv.fromRestriction дают: (HomEquiv.fromRestriction f g).hom y s = g (s · y).

LaTeX

$$$(HomEquiv.fromRestriction\ f\ g).hom\ y\ s = g\ (s \cdot y)$$$

Lean4

/-- This should be autogenerated by `@[simps]` but we need to give `s` the correct type here. -/
@[simp]
theorem fromRestriction_hom_apply_apply {X : ModuleCat R} {Y : ModuleCat S} (g : (restrictScalars f).obj Y ⟶ X) (y)
    (s : S) : (HomEquiv.fromRestriction f g).hom y s = g (s • y) :=
  rfl

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