English
Any linear equivalence giving the base change yields IsBaseChange condition for the underlying maps.
Русский
Любое линейное эквивалентное отображение, задающее базовое изменение, удовлетворяет условию IsBaseChange для соответствующих отображений.
LaTeX
$$$ IsBaseChange.ofEquiv \; e \; (\forall x, e(x) = ...) $$
Lean4
/-- If `N` is the base change of `M` to `A`, then `N ⊗[R] P` is the base change
of `M ⊗[R] P` to `A`. This is simply the isomorphism
`A ⊗[S] (M ⊗[R] P) ≃ₗ[A] (A ⊗[S] M) ⊗[R] P`. -/
theorem isBaseChange_tensorProduct_map {f : M →ₗ[S] N} (hf : IsBaseChange A f) :
IsBaseChange A (AlgebraTensorModule.map f (LinearMap.id (R := R) (M := P))) :=
by
let e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
(AlgebraTensorModule.assoc R S A A M P).symm.trans (AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P))
refine IsBaseChange.of_equiv e (fun x ↦ ?_)
induction x with
| zero => simp
| tmul => simp [e, IsBaseChange.equiv_tmul]
| add _ _ h1 h2 => simp [tmul_add, h1, h2]
