equiv — Mathlib

English

The equivalence lTensor.equiv is the natural isomorphism between the quotient ((Q ⊗ N) ⧸ range (lTensor Q f)) and (Q ⊗ P) induced by the exactness of f and g and the surjectivity of g, realized as a linear equivalence.

Русский

Естественная линейная эквивалентность между фактор-модулем и левым тензорным произведением.

LaTeX

$$lTensor.equiv : ((Q ⊗ N) ⧸ range (lTensor Q f)) ≃_L (Q ⊗ P)$$

Lean4

/-- For a surjective `f : N →ₗ[R] P`,
  the natural equivalence between `Q ⊗ N ⧸ (image of ker f)` to `Q ⊗ P` -/
noncomputable def equiv : ((Q ⊗[R] N) ⧸ (LinearMap.range (lTensor Q f))) ≃ₗ[R] (Q ⊗[R] P) :=
  lTensor.linearEquiv_of_rightInverse Q hfg (Function.rightInverse_surjInv hg)

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