English
If there is a linear equivalence e giving a base change, then f is a base change; the proof uses the equivalence to build the lift.
Русский
Если существует линейное эквивалентное отображение e, задающее базовое изменение, то f является базовым изменением; доказательство строит подъем через эквивалентность.
LaTeX
$$$ IsBaseChange S f \Rightarrow \text{exists } e: M \cong N \Rightarrow IsBaseChange S f $$$
Lean4
theorem ofEquiv (e : M ≃ₗ[R] N) : IsBaseChange R e.toLinearMap :=
by
apply IsBaseChange.of_lift_unique
intro Q I₁ I₂ I₃ I₄ g
have : I₂ = I₃ := by
ext r q
change (by let _ := I₂; exact r • q) = (by let _ := I₃; exact r • q)
dsimp
rw [← one_smul R q, smul_smul, ← @smul_assoc _ _ _ (id _) (id _) (id _) I₄, smul_eq_mul]
cases this
refine
⟨g.comp e.symm.toLinearMap, by
ext
simp, ?_⟩
rintro y (rfl : _ = _)
ext
simp
