liftBaseChange_comp — Mathlib

English

For l: M → N and l': N → P, the composed map l' ∘ l.liftBaseChange equals (l'.restrictScalars).liftBaseChange.

Русский

Для отображений l: M → N и l': N → P, композиция l' ∘ (l.liftBaseChange) равна (l'.restrictScalars).liftBaseChange.

LaTeX

$$$l' \\circ (l.liftBaseChange) = (l'.restrictScalars R \\circ l).liftBaseChange A$$$

Lean4

theorem liftBaseChange_comp {P} [AddCommMonoid P] [Module A P] [Module R P] [IsScalarTower R A P] (l : M →ₗ[R] N)
    (l' : N →ₗ[A] P) : l' ∘ₗ l.liftBaseChange A = (l'.restrictScalars R ∘ₗ l).liftBaseChange A :=
  by
  ext
  simp

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