quotTensorEquivQuotSMul_symm_comp_mkQ

English

The composition of the symmetric quotient-equivalence with the mkQ map yields the canonical flip map at 1.

Русский

Сочетание симметрического эквививалента квоты с mkQ даёт каноническое отображение разворота на 1.

LaTeX

$$$$ (\text{tensorQuotEquivQuotSMul M I}).symm \circ (I \top).mkQ = \text{TensorProduct.mk } R (R / I) M \; 1. $$$$

Lean4

theorem quotTensorEquivQuotSMul_symm_comp_mkQ (I : Ideal R) :
    (quotTensorEquivQuotSMul M I).symm ∘ₗ (I • ⊤ : Submodule R M).mkQ = TensorProduct.mk R (R ⧸ I) M 1 :=
  LinearMap.ext (quotTensorEquivQuotSMul_symm_mk I)

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