inverse_of_rightInverse_comp_lTensor

English

The composition of the inverse map with the left-tensor map equals the canonical quotient projection: (lTensor.inverse_of_rightInverse Q hfg hgh) ∘ (lTensor Q g) = mkQ(p := range(lTensor Q f)).

Русский

Состав обратной карты и левой тензорной карты равен каноническому проекционному отображению на фактор-пространство.

LaTeX

$$$(lTensor.inverse_of_rightInverse Q hfg hgh) \\circ (lTensor Q g) = \\mathrm{mkQ}_{p := \\mathrm{range}(lTensor Q f)}$$$

Lean4

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

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