of_equiv — Mathlib

English

If there is a linear equivalence e exhibiting the base-change, then f is a base change along R → S.

Русский

Если существует линейное эквивалентное отображение e, которое демонстрирует базовое изменение, то f является базовым изменением вдоль R → S.

LaTeX

$$$ IsBaseChange\, S\, f = IsBaseChange( S, e^{-1} \circ f ) $$$

Lean4

theorem of_equiv (e : S ⊗[R] M ≃ₗ[S] N) (he : ∀ x, e (1 ⊗ₜ x) = f x) : IsBaseChange S f :=
  by
  apply IsTensorProduct.of_equiv (e.restrictScalars R)
  intro x y
  simp [show x ⊗ₜ[R] y = x • (1 ⊗ₜ[R] y) by simp [smul_tmul'], he]

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