quotientTensorEquiv — Mathlib

English

The inverse of quotientTensorQuotientEquiv, applied to Submodule.Quotient.mk (x ⊗ y), returns Submodule.Quotient.mk x ⊗ Submodule.Quotient.mk y.

Русский

Обратное отображение quotientTensorQuotientEquiv применённое к Submodule.Quotient.mk (x ⊗ y) возвращает Submodule.Quotient.mk x ⊗ Submodule.Quotient.mk y.

LaTeX

$$$(\\text{quotientTensorQuotientEquiv } m n)^{-1}(\\mathrm{Submodule.Quotient.mk}(x \\otimes y)) = \\mathrm{Submodule.Quotient.mk} x \\otimes_R \\mathrm{Submodule.Quotient.mk} y$$$

Lean4

/-- Let `M, N` be `R`-modules, `m ≤ M` be an `R`-submodule. Then we have a linear isomorphism between
tensor products of the quotient and the quotient of the tensor product:
`(M ⧸ m) ⊗[R] N ≃ₗ[R] (M ⊗[R] N) ⧸ (m ⊗ N)`.
-/
noncomputable def quotientTensorEquiv (m : Submodule R M) :
    (M ⧸ (m : Submodule R M)) ⊗[R] N ≃ₗ[R] (M ⊗[R] N) ⧸ (LinearMap.range (map m.subtype (LinearMap.id : N →ₗ[R] N))) :=
  congr (LinearEquiv.refl _ _) ((Submodule.quotEquivOfEqBot _ rfl).symm) ≪≫ₗ
      quotientTensorQuotientEquiv (N := N) m ⊥ ≪≫ₗ
    Submodule.Quotient.equiv _ _ (LinearEquiv.refl _ _)
      (by
        simp only [Submodule.map_sup]
        erw [Submodule.map_id, Submodule.map_id]
        simp only [sup_eq_left]
        rw [range_map_eq_span_tmul, range_map_eq_span_tmul]
        simp)

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