inverse_apply — Mathlib

English

The equivalence lTensor.equiv is a linear equivalence between the quotient ((Q ⊗ N) ⧸ range (lTensor Q f)) and Q ⊗ P, provided f,g Exact and hg surjective. Its inverse is lTensor.inverse_of_rightInverse Q hfg hgh.

Русский

Эквивалентность lTensor обеспечивает линейное взаимно однозначное соответствие между фактор-модулем и левым тензорным произведением.

LaTeX

$$$lTensor.equiv : ((Q\\otimes_R N) / \\mathrm{range}(lTensor\\ Q\\ f)) \\simeq_L (Q\\otimes_R P)$$$

Lean4

theorem inverse_apply (y : Q ⊗[R] N) :
    (lTensor.inverse Q hfg hg) ((lTensor Q g) y) = Submodule.Quotient.mk (p := (LinearMap.range (lTensor Q f))) y := by
  rw [lTensor.inverse, lTensor.inverse_of_rightInverse_apply]

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