ofTensorProductEquivOfFiniteNoetherian_symm_of

English

A compatibility relation expresses that a left-tensor map equals the conjugation of the map by canonical equivalences.

Русский

Справедливость совместимости: левосторонняя карта тензорного отображения равна конъюгированию отображения каноническими эквивалентностями.

LaTeX

$$$\mathrm{AlgebraTensorModule.map}(\mathrm{id}, f) = (\mathrm{AdicCompletion.ofTensorProductEquivOfFiniteNoetherian}\ I\ N)^{-1} \circ (\mathrm{AdicCompletion.map}\ I\ f) \circ (\mathrm{AdicCompletion.ofTensorProductEquivOfFiniteNoetherian}\ I\ M)$$$

Lean4

@[simp]
theorem ofTensorProductEquivOfFiniteNoetherian_symm_of [Module.Finite R M] (x : M) :
    (ofTensorProductEquivOfFiniteNoetherian I M).symm ((of I M) x) = 1 ⊗ₜ x :=
  by
  have h : (of I M) x = ofTensorProductEquivOfFiniteNoetherian I M (1 ⊗ₜ x) := by simp
  rw [h, LinearEquiv.symm_apply_apply]

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