inverse_of_rightInverse_comp_rTensor

English

The inverse of the lTensor equivalence composed with lTensor g equals the mkQ map, i.e., the canonical projection onto the quotient by range(f).

Русский

Обратный к композиции левого тензорного эквивалента совпадает с проекцией на квотируемый модуль по образу f.

LaTeX

$$inverse_comp_lTensor : (lTensor.inverse Q hfg hg).comp (lTensor Q g) = Submodule.mkQ (p := LinearMap.range (lTensor Q f))$$

Lean4

theorem inverse_of_rightInverse_comp_rTensor {h : P → N} (hgh : Function.RightInverse h g) :
    (rTensor.inverse_of_rightInverse Q hfg hgh).comp (rTensor Q g) =
      Submodule.mkQ (p := LinearMap.range (rTensor Q f)) :=
  by
  rw [LinearMap.ext_iff]
  intro y
  simp only [coe_comp, Function.comp_apply, Submodule.mkQ_apply, rTensor.inverse_of_rightInverse_apply]

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