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

theorem IsBaseChange.of_basis {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] (A : Type u_3) [CommSemiring A] [Algebra A R] [Module A V] [IsScalarTower A R V] {ι : Type u_4} (b : Module.Basis ι R V) : IsBaseChange R (Finsupp.linearCombination A ⇑b)

theorem IsBaseChange.of_fintype_basis {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] (A : Type u_3) [CommSemiring A] [Algebra A R] [Module A V] [IsScalarTower A R V] {ι : Type u_4} (b : Module.Basis ι R V) [Fintype ι] : IsBaseChange R (Fintype.linearCombination A ⇑b)

Any finite basis of a module can express it as the base change of a finite free module from any under-ring.

theorem IsBaseChange.of_fintype_basis_eq {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] {A : Type u_3} [CommSemiring A] [Algebra A R] [Module A V] [IsScalarTower A R V] {ι : Type u_4} {b : Module.Basis ι R V} [Fintype ι] {a : ι → A} {v : V} : (Fintype.linearCombination A ⇑b) a = v ↔ ⇑(algebraMap A R) ∘ a = b.equivFun v