Base change of a free module

• IsBaseChange.basis : the natural basis of the base change of a module with a basis

• IsBaseChange.free : a base change of a free module is free.

noncomputable def IsBaseChange.basis {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {V : Type u_3} [AddCommMonoid V] [Module R V] {W : Type u_4} [AddCommMonoid W] [Module R W] [Module S W] [IsScalarTower R S W] {ι : Type u_5} {ε : V →ₗ[R] W} (b : Module.Basis ι R V) (ibc : IsBaseChange S ε) : Module.Basis ι S W

The basis of a module deduced by base change from a free module with a basis.

Equations

• IsBaseChange.basis b ibc = { repr := (ibc.equiv.symm.trans (LinearEquiv.baseChange R S V (ι →₀ R) b.repr)).trans ⋯.equiv }

theorem IsBaseChange.basis_apply {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {V : Type u_3} [AddCommMonoid V] [Module R V] {W : Type u_4} [AddCommMonoid W] [Module R W] [Module S W] [IsScalarTower R S W] {ι : Type u_5} {ε : V →ₗ[R] W} (b : Module.Basis ι R V) (ibc : IsBaseChange S ε) (i : ι) : (basis b ibc) i = ε (b i)

theorem IsBaseChange.basis_repr_comp_apply {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {V : Type u_3} [AddCommMonoid V] [Module R V] {W : Type u_4} [AddCommMonoid W] [Module R W] [Module S W] [IsScalarTower R S W] {ι : Type u_5} {ε : V →ₗ[R] W} (b : Module.Basis ι R V) (ibc : IsBaseChange S ε) (v : V) (i : ι) : ((basis b ibc).repr (ε v)) i = (algebraMap R S) ((b.repr v) i)

theorem IsBaseChange.basis_repr_comp {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {V : Type u_3} [AddCommMonoid V] [Module R V] {W : Type u_4} [AddCommMonoid W] [Module R W] [Module S W] [IsScalarTower R S W] {ι : Type u_5} {ε : V →ₗ[R] W} (b : Module.Basis ι R V) (ibc : IsBaseChange S ε) (v : V) : (basis b ibc).repr (ε v) = (Finsupp.mapRange.linearMap (Algebra.linearMap R S)) (b.repr v)

theorem IsBaseChange.free {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {V : Type u_3} [AddCommMonoid V] [Module R V] {W : Type u_4} [AddCommMonoid W] [Module R W] [Module S W] [IsScalarTower R S W] {ε : V →ₗ[R] W} (ibc : IsBaseChange S ε) [Module.Free R V] : Module.Free S W