feat(linear_algebra/basis): if R ≃ R', map a basis for R-module `…

…M` to `R'`-module `M` (#8699)

If `R` and `R'` are isomorphic rings that act identically on a module `M`, then a basis for `M` as `R`-module is also a basis for `M` as `R'`-module.

src/data/equiv/ring.lean

@@ -242,6 +242,12 @@ lemma map_ne_one_iff : f x ≠ 1 ↔ x ≠ 1 := (f : R ≃* S).map_ne_one_iff
 noncomputable def of_bijective (f : R →+* S) (hf : function.bijective f) : R ≃+* S :=
 { .. equiv.of_bijective f hf, .. f }
 
+@[simp] lemma coe_of_bijective (f : R →+* S) (hf : function.bijective f) :
+  (of_bijective f hf : R → S) = f := rfl
+
+lemma of_bijective_apply (f : R →+* S) (hf : function.bijective f) (x : R) :
+  of_bijective f hf x = f x := rfl
+
 end semiring
 
 section

src/linear_algebra/basis.lean

@@ -247,6 +247,35 @@ of_repr (f.symm.trans b.repr)
 
 end map
 
+section map_coeffs
+
+variables {R' : Type*} [semiring R'] [module R' M] (f : R ≃+* R') (h : ∀ c (x : M), f c • x = c • x)
+
+include f h b
+
+/-- If `R` and `R'` are isomorphic rings that act identically on a module `M`,
+then a basis for `M` as `R`-module is also a basis for `M` as `R'`-module.
+
+See also `basis.algebra_map_coeffs` for the case where `f` is equal to `algebra_map`.
+-/
+@[simps {simp_rhs := tt}]
+def map_coeffs : basis ι R' M :=
+begin
+  letI : module R' R := module.comp_hom R (↑f.symm : R' →+* R),
+  haveI : is_scalar_tower R' R M :=
+  { smul_assoc := λ x y z, begin dsimp [(•)],  rw [mul_smul, ←h, f.apply_symm_apply], end },
+  exact (of_repr $ (b.repr.restrict_scalars R').trans $
+    finsupp.map_range.linear_equiv (module.comp_hom.to_linear_equiv f.symm).symm )
+end
+
+lemma map_coeffs_apply (i : ι) : b.map_coeffs f h i = b i :=
+apply_eq_iff.mpr $ by simp [f.to_add_equiv_eq_coe]
+
+@[simp] lemma coe_map_coeffs : (b.map_coeffs f h : ι → M) = b :=
+funext $ b.map_coeffs_apply f h
+
+end map_coeffs
+
 section reindex
 
 variables (b' : basis ι' R M')

src/ring_theory/algebra_tower.lean

@@ -121,6 +121,26 @@ by rw [finset.coe_union, finset.coe_image, algebra.adjoin_union_eq_under,
   subalgebra.res_top]⟩
 end
 
+section algebra_map_coeffs
+
+variables {R} (A) {ι M : Type*} [comm_semiring R] [semiring A] [add_comm_monoid M]
+variables [algebra R A] [module A M] [module R M] [is_scalar_tower R A M]
+variables (b : basis ι R M) (h : function.bijective (algebra_map R A))
+
+/-- If `R` and `A` have a bijective `algebra_map R A` and act identically on `M`,
+then a basis for `M` as `R`-module is also a basis for `M` as `R'`-module. -/
+@[simps]
+noncomputable def basis.algebra_map_coeffs : basis ι A M :=
+b.map_coeffs (ring_equiv.of_bijective _ h) (λ c x, by simp)
+
+lemma basis.algebra_map_coeffs_apply (i : ι) : b.algebra_map_coeffs A h i = b i :=
+b.map_coeffs_apply _ _ _
+
+@[simp] lemma basis.coe_algebra_map_coeffs : (b.algebra_map_coeffs A h : ι → M) = b :=
+b.coe_map_coeffs _ _
+
+end algebra_map_coeffs
+
 section ring
 
 open finsupp