tensorEqLocusEquiv_apply — Mathlib

English

If T is flat then tensorEqLocusEquiv provides an algebra isomorphism between M ⊗ eqLocus f g and eqLocus (lTensor f) (lTensor g).

Русский

Если T плоский, то tensorEqLocusEquiv задаёт алгебра-подобный изоморфизм между M ⊗ eqLocus f g и eqLocus (lTensor f) (lTensor g).

LaTeX

$$$\text{tensorEqLocusEquiv} [Module.Flat R M] : M ⊗_R eqLocus f g \cong_S eqLocus( lTensor S M f, lTensor S M g )$$$

Lean4

@[simp]
theorem tensorEqLocusEquiv_apply [Module.Flat R M] (x : M ⊗[R] LinearMap.eqLocus f g) :
    LinearMap.tensorEqLocusEquiv S M f g x = LinearMap.tensorEqLocus S M f g x :=
  rfl

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