Tensor products of dual spaces

Main definitions

• PiTensorProduct.dualDistrib: The canonical linear map from ⨂[R] i, Dual R (M i) to Dual R (⨂[R] i, M i), sending ⨂ₜ[R] i, f i to the composition of PiTensorProduct.map f with the linear equivalence ⨂[R] i, R →ₗ R given by multiplication.

• PiTensorProduct.dualDistribEquiv: A linear equivalence between ⨂[R] i, Dual R (M i) and Dual R (⨂[R] i, M i) when all M i are finite free modules. If f : (i : ι) → Dual R (M i), then this equivalence sends ⨂ₜ[R] i, f i to the composition of PiTensorProduct.map f with the natural isomorphism ⨂[R] i, R ≃ R given by multiplication.

noncomputable def PiTensorProduct.dualDistrib {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [CommSemiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Finite ι] : (PiTensorProduct R fun (i : ι) => Module.Dual R (M i)) →ₗ[R] Module.Dual R (PiTensorProduct R fun (i : ι) => M i)

The canonical linear map from ⨂[R] i, Dual R (M i) to Dual R (⨂[R] i, M i), sending ⨂ₜ[R] i, f i to the composition of PiTensorProduct.map f with the linear equivalence ⨂[R] i, R →ₗ R given by multiplication.

@[simp]

theorem PiTensorProduct.dualDistrib_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [CommSemiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] (f : (i : ι) → Module.Dual R (M i)) (m : (i : ι) → M i) : (dualDistrib ((tprod R) fun (i : ι) => f i)) (⨂ₜ[R] (i : ι), m i) = ∏ i : ι, (f i) (m i)

noncomputable def PiTensorProduct.dualDistribInvOfBasis {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Finite ι] [∀ (i : ι), Finite (κ i)] (b : (i : ι) → Module.Basis (κ i) R (M i)) : Module.Dual R (PiTensorProduct R fun (i : ι) => M i) →ₗ[R] PiTensorProduct R fun (i : ι) => Module.Dual R (M i)

An inverse to PiTensorProduct.dualDistrib given bases.

@[simp]

theorem PiTensorProduct.dualDistribInvOfBasis_apply {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Fintype ι] [(i : ι) → Fintype (κ i)] (b : (i : ι) → Module.Basis (κ i) R (M i)) (f : Module.Dual R (PiTensorProduct R fun (i : ι) => M i)) : (dualDistribInvOfBasis b) f = ∑ p : (i : ι) → κ i, f (⨂ₜ[R] (i : ι), (b i) (p i)) • (tprod R) fun (i : ι) => (b i).dualBasis (p i)

theorem PiTensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Finite ι] [∀ (i : ι), Finite (κ i)] (b : (i : ι) → Module.Basis (κ i) R (M i)) : dualDistrib ∘ₗ dualDistribInvOfBasis b = LinearMap.id

theorem PiTensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Finite ι] [∀ (i : ι), Finite (κ i)] (b : (i : ι) → Module.Basis (κ i) R (M i)) : dualDistribInvOfBasis b ∘ₗ dualDistrib = LinearMap.id

noncomputable def PiTensorProduct.dualDistribEquivOfBasis {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Finite ι] [∀ (i : ι), Finite (κ i)] (b : (i : ι) → Module.Basis (κ i) R (M i)) : (PiTensorProduct R fun (i : ι) => Module.Dual R (M i)) ≃ₗ[R] Module.Dual R (PiTensorProduct R fun (i : ι) => M i)

A linear equivalence between ⨂[R] i, Dual R (M i) and Dual R (⨂[R] i, M i) given bases for all M i. If f : (i : ι) → Dual R (s i), then this equivalence sends ⨂ₜ[R] i, f i to the composition of PiTensorProduct.map f with the natural isomorphism ⨂[R] i, R ≃ R given by multipliccation (constantBaseRingEquiv).

@[simp]

theorem PiTensorProduct.dualDistribEquivOfBasis_apply_apply {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Finite ι] [∀ (i : ι), Finite (κ i)] (b : (i : ι) → Module.Basis (κ i) R (M i)) (a✝ : PiTensorProduct R fun (i : ι) => Module.Dual R (M i)) (a✝¹ : PiTensorProduct R fun (i : ι) => M i) : ((dualDistribEquivOfBasis b) a✝) a✝¹ = (constantBaseRingEquiv ι R) ((piTensorHomMap a✝) a✝¹)

@[simp]

theorem PiTensorProduct.dualDistribEquivOfBasis_symm_apply {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Finite ι] [∀ (i : ι), Finite (κ i)] (b : (i : ι) → Module.Basis (κ i) R (M i)) (a : Module.Dual R (PiTensorProduct R fun (i : ι) => M i)) : (dualDistribEquivOfBasis b).symm a = (dualDistribInvOfBasis b) a

noncomputable def PiTensorProduct.dualDistribEquiv {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Finite R (M i)] [∀ (i : ι), Module.Free R (M i)] [Finite ι] : (PiTensorProduct R fun (i : ι) => Module.Dual R (M i)) ≃ₗ[R] Module.Dual R (PiTensorProduct R fun (i : ι) => M i)

A linear equivalence between ⨂[R] i, Dual R (M i) and Dual R (⨂[R] i, M i) when all M i are finite free modules. If f : (i : ι) → Dual R (M i), then this equivalence sends ⨂ₜ[R] i, f i to the composition of PiTensorProduct.map f with the natural isomorphism ⨂[R] i, R ≃ R given by multipliccation (constantBaseRingEquiv).