Base change for the dual of a module

• Module.Dual.congr : equivalent modules have equivalent duals.

If f : Module.Dual R V and Algebra R A, then

• Module.Dual.baseChange A f is the element of Module.Dual A (A ⊗[R] V) deduced by base change.

• Module.Dual.baseChangeHom is the R-linear map given by Module.Dual.baseChange.

• IsBaseChange.dual : for finite free modules, taking dual commutes with base change.

def Module.Dual.congr {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] {W : Type u_3} [AddCommMonoid W] [Module R W] (e : V ≃ₗ[R] W) : Dual R V ≃ₗ[R] Dual R W

Equivalent modules have equivalent duals.

Equations

• Module.Dual.congr e = LinearEquiv.congrLeft R R e

@[simp]

theorem Module.Dual.congr_apply_apply {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] {W : Type u_3} [AddCommMonoid W] [Module R W] (e : V ≃ₗ[R] W) (a✝ : V →ₗ[R] R) (a✝¹ : W) : ((congr e) a✝) a✝¹ = a✝ (e.symm a✝¹)

@[simp]

theorem Module.Dual.congr_symm_apply_apply {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] {W : Type u_3} [AddCommMonoid W] [Module R W] (e : V ≃ₗ[R] W) (a✝ : W →ₗ[R] R) (a✝¹ : V) : ((congr e).symm a✝) a✝¹ = a✝ (e a✝¹)

def Module.Dual.baseChange {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] (A : Type u_4) [CommSemiring A] [Algebra R A] : Dual R V →ₗ[R] Dual A (TensorProduct R A V)

LinearMap.baseChange for Module.Dual.

Equations

• Module.Dual.baseChange A = LinearMap.compRight R ↑(TensorProduct.AlgebraTensorModule.rid R A A) ∘ₗ LinearMap.baseChangeHom R A V R

@[simp]

theorem Module.Dual.baseChange_apply_tmul {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] (A : Type u_4) [CommSemiring A] [Algebra R A] (f : Dual R V) (a : A) (v : V) : ((baseChange A) f) (a ⊗ₜ[R] v) = f v • a

theorem Module.Dual.baseChange_baseChange {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] (A : Type u_4) [CommSemiring A] [Algebra R A] {B : Type u_5} [CommSemiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (f : Dual R V) : (baseChange B) ((baseChange A) f) = (congr (TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B V)).symm ((baseChange B) f)

noncomputable def IsBaseChange.toDual {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] {W : Type u_3} [AddCommMonoid W] [Module R W] {A : Type u_4} [CommSemiring A] [Algebra R A] [Module A W] [IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j) : Module.Dual R V →ₗ[R] Module.Dual A W

The base change of an element of the dual.

Equations

• ibc.toDual = ibc.linearMapLeftRightHom (Algebra.linearMap R A)

theorem IsBaseChange.toDual_comp_apply {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] {W : Type u_3} [AddCommMonoid W] [Module R W] {A : Type u_4} [CommSemiring A] [Algebra R A] [Module A W] [IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j) (f : Module.Dual R V) (v : V) : (ibc.toDual f) (j v) = (algebraMap R A) (f v)

theorem IsBaseChange.toDual_apply {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] {W : Type u_3} [AddCommMonoid W] [Module R W] {A : Type u_4} [CommSemiring A] [Algebra R A] [Module A W] [IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j) (f : Module.Dual R V) : ibc.toDual f = (Module.Dual.congr ibc.equiv) ((Module.Dual.baseChange A) f)

noncomputable def IsBaseChange.toDualBaseChange {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] {W : Type u_3} [AddCommMonoid W] [Module R W] {A : Type u_4} [CommSemiring A] [Algebra R A] [Module A W] [IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j) [Module.Free R V] [Module.Finite R V] : TensorProduct R A (Module.Dual R V) ≃ₗ[A] Module.Dual A W

The linear equivalence underlying IsBaseChange.dual.

Equations

• ibc.toDualBaseChange = LinearEquiv.ofBijective (IsBaseChange.toDualBaseChangeAux✝ ibc) ⋯

theorem IsBaseChange.toDualBaseChange_tmul {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] {W : Type u_3} [AddCommMonoid W] [Module R W] {A : Type u_4} [CommSemiring A] [Algebra R A] [Module A W] [IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j) [Module.Free R V] [Module.Finite R V] (a : A) (f : Module.Dual R V) (v : V) : (ibc.toDualBaseChange (a ⊗ₜ[R] f)) (j v) = a * (algebraMap R A) (f v)

theorem IsBaseChange.dual {R : Type u_1} [CommSemiring R] {V : Type u_2} [AddCommMonoid V] [Module R V] {W : Type u_3} [AddCommMonoid W] [Module R W] {A : Type u_4} [CommSemiring A] [Algebra R A] [Module A W] [IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j) [Module.Free R V] [Module.Finite R V] : IsBaseChange A ibc.toDual