lift_lsmul_mul_eq_lsmul_lift_lsmul

English

The lifting map commutes with left-smul and mul in the precise way: lift (lsmul_R M ∘ₗ mul R R r) = lsmul_R M r ∘ₗ lift (lsmul_R M).

Русский

Лиственный подъем коммутирует с левым умножением на скаляры и умножением в точном виде: lift ∘ (lsmul ∘ mul r) = (lsmul r) ∘ lift ∘ (lsmul).

LaTeX

$$$$ \mathrm{lift} \circ (\mathrm{lsmul}_R M \circ_ℓ \mathrm{mul}_R R r) = (\mathrm{lsmul}_R M r) \circ_ℓ \mathrm{lift}(\mathrm{lsmul}_R M). $$$$

Lean4

theorem lift_lsmul_mul_eq_lsmul_lift_lsmul {r : R} : lift (lsmul R M ∘ₗ mul R R r) = lsmul R M r ∘ₗ lift (lsmul R M) :=
  by
  apply TensorProduct.ext'
  intro x a
  simp [← mul_smul, mul_comm]

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