extendScalars_id_comp — Mathlib

English

The composition extendScalarsId with its inverse yields the identity on all M; i.e., extending by id_R then applying the inverse recovers the original element.

Русский

Составление extendScalarsId с обратным отображением даёт тождество на каждом модуле M; расширение по id_R затем применение обратного отображает исходный элемент.

LaTeX

$$$$ (\mathrm{extendScalarsId} \cdot)_{M} \circ (\mathrm{extendScalarsId})^{-1}_{M} = \mathrm{Id}_{M}. $$$$

Lean4

@[reassoc]
theorem extendScalars_id_comp :
    (extendScalarsComp (RingHom.id R₁) f₁₂).hom ≫
        Functor.whiskerRight (extendScalarsId R₁).hom _ ≫ (Functor.leftUnitor _).hom =
      𝟙 _ :=
  by
  ext M m
  dsimp
  erw [extendScalarsComp_hom_app_one_tmul (RingHom.id R₁) f₁₂ M m]
  rw [ExtendScalars.map_tmul]
  erw [extendScalarsId_hom_app_one_tmul]
  rfl

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