congr — Mathlib

English

Let f be a family of linear equivalences; then congr f sends a tensor of elements m_i to the tensor of f_i(m_i).

Русский

Пусть f_i — линейные эквивалентности; congr f отправляет тензор m_i в тензор f_i(m_i).

LaTeX

$$$\text{congr } f\ (tprod\ R\ m) = tprod\ R (\lambda i. f_i(m_i))$$$

Lean4

/-- If `s i` and `t i` are linearly equivalent for every `i` in `ι`, then `⨂[R] i, s i` and
`⨂[R] i, t i` are linearly equivalent.

This is the n-ary version of `TensorProduct.congr`
-/
noncomputable def congr (f : Π i, s i ≃ₗ[R] t i) : (⨂[R] i, s i) ≃ₗ[R] ⨂[R] i, t i :=
  .ofLinear (map (fun i ↦ f i)) (map (fun i ↦ (f i).symm)) (by ext; simp) (by ext; simp)

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