inverse_of_rightInverse_apply — Mathlib

English

For h : P → N a right inverse of g, and hfg ensuring Exact f g, the inverse_of_rightInverse applied to the forward image yields the canonical quotient class: (lTensor.inverse_of_rightInverse Q hfg hgh)((lTensor Q g) y) equals the class of y in the quotient by range(lTensor Q f).

Русский

Для h: P → N, являющегося правым обратным к g, и g∣f образуют точную последовательность, обращение_inverse после прямого отображения даёт канонический класс смещения по квоты: (lTensor.inverse_of_rightInverse ...)((lTensor Q g) y) равен классy по отношению к range(lTensor Q f).

LaTeX

$$$\\bigl(lTensor.inverse_of_rightInverse Q hfg hgh\\bigr)\\bigl((lTensor Q g) y\\bigr) = \\mathrm{mk}_Q(y)\\;\\in\\; (Q\\otimes_R N)/\\mathrm{range}(lTensor Q f)$$$

Lean4

theorem inverse_of_rightInverse_apply {h : P → N} (hgh : Function.RightInverse h g) (y : Q ⊗[R] N) :
    (lTensor.inverse_of_rightInverse Q hfg hgh) ((lTensor Q g) y) =
      Submodule.Quotient.mk (p := (LinearMap.range (lTensor Q f))) y :=
  by
  simp only [← LinearMap.comp_apply, ← Submodule.mkQ_apply]
  rw [exact_iff] at hfg
  apply LinearMap.congr_fun
  apply TensorProduct.ext'
  intro n q
  suffices Submodule.Quotient.mk (n ⊗ₜ[R] h (g q)) = Submodule.Quotient.mk (n ⊗ₜ[R] q) by simpa
  rw [Submodule.Quotient.eq, ← TensorProduct.tmul_sub]
  apply le_comap_range_lTensor f n
  rw [← hfg, mem_ker, map_sub, sub_eq_zero, hgh]

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