lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm

English

The coefficient map of tensorEqualizer coincides with the corresponding algebraic tensor map on the underlying elements.

Русский

Коэффициентная карта tensorEqualizer совпадает с соответствующим алгебра-тензорным отображением на базовых элементах.

LaTeX

$$coe_tensorEqualizer (x) = Algebra.TensorProduct.map (AlgHom.id S T) (AlgHom.equalizer f g).val x$$

Lean4

@[simp]
theorem lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm [Module.Flat R M]
    (x : eqLocus (AlgebraTensorModule.lTensor S M f) (AlgebraTensorModule.lTensor S M g)) :
    (lTensor M (eqLocus f g).subtype) ((tensorEqLocusEquiv S M f g).symm x) = x :=
  lTensor_eqLocus_subtype_tensorEqLocusInv S M f g x

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