English
Freeness is preserved under ring equivalence: if R ≃+* R' and M ≃ₛₗ M' with M free, then M' is free.
Русский
Свобода сохраняется при кольцевом эквиваленте: если R ≃+* R' и M ≃_р M' т.е. линейно подобна, и M свободен, то M' свободен.
LaTeX
$$$$ (e_1:\ R \simeq_+* R') \; (e_2:\ M \simeq_\RingHomClass.toRingHom e_1) \; \Big[ \mathrm{Module.Free } R M \Big] \Rightarrow \mathrm{Module.Free } R' M' $$$$
Lean4
theorem of_ringEquiv {R R' M M'} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R'] [AddCommMonoid M']
[Module R' M'] (e₁ : R ≃+* R') (e₂ : M ≃ₛₗ[RingHomClass.toRingHom e₁] M') [Module.Free R M] : Module.Free R' M' :=
by
let I := Module.Free.ChooseBasisIndex R M
obtain ⟨e₃ : M ≃ₗ[R] I →₀ R⟩ := Module.Free.chooseBasis R M
let e : M' ≃+ (I →₀ R') := (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv (α := I) e₁.toAddEquiv)
have he (x) : e x = Finsupp.mapRange.addEquiv (α := I) e₁.toAddEquiv (e₃ (e₂.symm x)) := rfl
let e' : M' ≃ₗ[R'] (I →₀ R') := { __ := e, map_smul' := fun m x ↦ Finsupp.ext fun i ↦ by simp [he, map_smulₛₗ] }
exact of_basis (.ofRepr e')
