Base change of a free module #
IsBaseChange.basis: the natural basis of the base change of a module with a basisIsBaseChange.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
Instances For
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 : ι)
:
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 : ι)
:
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)
:
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}
: