lift_comp_inrHom — Mathlib

English

The toLinearMap part of lift composed with inrHom (restricted scalars) equals g.

Русский

Часть lift как линейное отображение после inrHom (ограничение скаляров) равна g.

LaTeX

$$$ (lift f g hg hfg hgf).toLinearMap.comp (inrHom R M |>.restrictScalars S) = g $$$

Lean4

@[simp]
theorem lift_comp_inrHom (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ x y, g x * g y = 0)
    (hfg : ∀ r x, g (r •> x) = f r * g x) (hgf : ∀ r x, g (x <• r) = g x * f r) :
    (lift f g hg hfg hgf).toLinearMap.comp (inrHom R M |>.restrictScalars S) = g :=
  LinearMap.ext <| lift_apply_inr f g hg hfg hgf

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