Multiplying the factors of a tensor product of commutative algebras along fibres

A finite tensor product of commutative R-algebras is their coproduct, so a map f : σ → τ of finite index types induces an algebra map

⨂_{i : σ} A (f i) → ⨂_{j : τ} A j,     ⨂ₜ xᵢ ↦ ∏ᵢ (1 ⊗ ⋯ ⊗ xᵢ ⊗ ⋯ ⊗ 1),

placing xᵢ in the slot f i. It multiplies together the factors in each fibre of f and puts 1 in the slots outside the range of f. When f is a bijection it is the reindexing equivalence; when f collapses two indices it is the multiplication of those two factors, and when a slot is not hit it is the unit there. These are the merge and birth maps of a commutative Frobenius algebra acting on tensor products indexed by finite sets of circles.

For a finite tensor power of a single commutative algebra B, multiplying all the factors together gives an algebra map from ⨂_{i : σ} B to B itself. It is the indexed analogue of Algebra.TensorProduct.lmul'.

Main definitions

• PiTensorProduct.fiberwiseMul: the algebra map along f : σ → τ.
• PiTensorProduct.mulAlgHom: multiplication of all the factors of a finite tensor power of a commutative algebra.

Main results

• PiTensorProduct.fiberwiseMul_tprod, PiTensorProduct.fiberwiseMul_singleAlgHom: its values on pure tensors and on the factor inclusions.
• PiTensorProduct.fiberwiseMul_id, PiTensorProduct.fiberwiseMul_comp: functoriality in f.
• PiTensorProduct.mulAlgHom_tprod, PiTensorProduct.mulAlgHom_singleAlgHom: the values of PiTensorProduct.mulAlgHom on pure tensors and on the factor inclusions.
• PiTensorProduct.tprod_eq_prod_singleAlgHom: a pure tensor is the product of its factors.
• PiTensorProduct.fiberwiseMul_tprod_eq_tprod_prod: for a constant family, the image of a pure tensor is the pure tensor of the products over the fibres.
• PiTensorProduct.toLinearMap_fiberwiseMul_equiv: along a bijection it is PiTensorProduct.reindex.
• PiTensorProduct.reindex_fiberwiseMul: it commutes with reindexing along a commuting square of index maps.
• PiTensorProduct.fiberwiseMul_sum_map: multiplication on a disjoint union is the tensor product of the multiplications on its two summands.
• PiTensorProduct.fiberwiseMul_fiberwiseMul_surjInv: along a surjection it has a right inverse, multiplication along a section.

noncomputable def PiTensorProduct.fiberwiseMul {R : Type u_1} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} {A : τ → Type u_5} [(j : τ) → CommSemiring (A j)] [(j : τ) → Algebra R (A j)] [Fintype σ] [DecidableEq τ] (f : σ → τ) : (PiTensorProduct R fun (i : σ) => A (f i)) →ₐ[R] PiTensorProduct R fun (j : τ) => A j

The algebra map ⨂_{i : σ} A (f i) → ⨂_{j : τ} A j induced by a map f : σ → τ of finite index types: it sends ⨂ₜ x to the product over i of x i placed in the slot f i. The factors in each fibre of f are multiplied together, and slots outside the range of f get 1.

@[simp]

theorem PiTensorProduct.fiberwiseMul_tprod {R : Type u_1} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} {A : τ → Type u_5} [(j : τ) → CommSemiring (A j)] [(j : τ) → Algebra R (A j)] [Fintype σ] [DecidableEq τ] (f : σ → τ) (x : (i : σ) → A (f i)) : (fiberwiseMul f) ((tprod R) x) = ∏ i : σ, (singleAlgHom (f i)) (x i)

PiTensorProduct.fiberwiseMul f places each factor of a pure tensor in its slot and multiplies the results.

@[simp]

theorem PiTensorProduct.fiberwiseMul_singleAlgHom {R : Type u_1} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} {A : τ → Type u_5} [(j : τ) → CommSemiring (A j)] [(j : τ) → Algebra R (A j)] [Fintype σ] [DecidableEq τ] [DecidableEq σ] (f : σ → τ) (i : σ) (a : A (f i)) : (fiberwiseMul f) ((singleAlgHom i) a) = (singleAlgHom (f i)) a

PiTensorProduct.fiberwiseMul f sends the factor inclusion at i to the factor inclusion at f i. It is a pre-simp lemma since singleAlgHom_apply would otherwise rewrite the inner factor inclusion first.

@[simp]

theorem PiTensorProduct.fiberwiseMul_id (R : Type u_1) [CommSemiring R] {τ : Type u_3} (A : τ → Type u_5) [(j : τ) → CommSemiring (A j)] [(j : τ) → Algebra R (A j)] [DecidableEq τ] [Fintype τ] : fiberwiseMul id = AlgHom.id R (PiTensorProduct R fun (j : τ) => A j)

PiTensorProduct.fiberwiseMul along the identity is the identity.

theorem PiTensorProduct.fiberwiseMul_comp {R : Type u_1} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} {υ : Type u_4} [Fintype σ] [DecidableEq τ] [Fintype τ] [DecidableEq υ] {A : υ → Type u_6} [(k : υ) → CommSemiring (A k)] [(k : υ) → Algebra R (A k)] (g : τ → υ) (f : σ → τ) : (fiberwiseMul g).comp (fiberwiseMul f) = fiberwiseMul (g ∘ f)

PiTensorProduct.fiberwiseMul is functorial: multiplying along the fibres of f and then along those of g is multiplying along the fibres of g ∘ f.

theorem PiTensorProduct.tprod_eq_prod_singleAlgHom {R : Type u_1} [CommSemiring R] {τ : Type u_3} {A : τ → Type u_5} [(j : τ) → CommSemiring (A j)] [(j : τ) → Algebra R (A j)] [DecidableEq τ] [Fintype τ] (x : (j : τ) → A j) : (tprod R) x = ∏ j : τ, (singleAlgHom j) (x j)

A pure tensor of a finite tensor product of commutative algebras is the product of its factors, each placed in its own slot.

noncomputable def PiTensorProduct.mulAlgHom {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] {B : Type u_6} [CommSemiring B] [Algebra R B] : (PiTensorProduct R fun (x : σ) => B) →ₐ[R] B

Multiplication of the tensor factors, as an algebra map from a finite tensor power of B to B. It is the indexed analogue of Algebra.TensorProduct.lmul'.

@[simp]

theorem PiTensorProduct.mulAlgHom_tprod {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] {B : Type u_6} [CommSemiring B] [Algebra R B] (x : σ → B) : mulAlgHom ((tprod R) x) = ∏ i : σ, x i

PiTensorProduct.mulAlgHom multiplies the factors of a pure tensor.

@[simp]

theorem PiTensorProduct.mulAlgHom_singleAlgHom {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] {B : Type u_6} [CommSemiring B] [Algebra R B] [DecidableEq σ] (i : σ) (b : B) : mulAlgHom ((singleAlgHom i) b) = b

PiTensorProduct.mulAlgHom is a left inverse of each factor inclusion. It is a pre-simp lemma since singleAlgHom_apply would otherwise rewrite the factor inclusion first.

theorem PiTensorProduct.fiberwiseMul_tprod_eq_tprod_prod {R : Type u_1} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} [Fintype σ] [DecidableEq τ] {B : Type u_6} [CommSemiring B] [Algebra R B] [Finite τ] (f : σ → τ) (x : σ → B) : (fiberwiseMul f) ((tprod R) x) = (tprod R) fun (j : τ) => ∏ i : σ with f i = j, x i

For a constant family, PiTensorProduct.fiberwiseMul f sends a pure tensor to the pure tensor of the products of its factors over the fibres of f. In particular, an index j outside the range of f receives the empty product 1.

theorem PiTensorProduct.toLinearMap_fiberwiseMul_equiv {R : Type u_1} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} [Fintype σ] [DecidableEq τ] {B : Type u_6} [CommSemiring B] [Algebra R B] (e : σ ≃ τ) : (fiberwiseMul ⇑e).toLinearMap = ↑(reindex R (fun (x : σ) => B) e)

Along a bijection, PiTensorProduct.fiberwiseMul is the reindexing equivalence.

theorem PiTensorProduct.reindex_fiberwiseMul {R : Type u_1} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} [Fintype σ] [DecidableEq τ] {B : Type u_6} [CommSemiring B] [Algebra R B] {σ' : Type u_7} {τ' : Type u_8} [Fintype σ'] [Finite τ] [DecidableEq τ'] (eσ : σ ≃ σ') (eτ : τ ≃ τ') {f : σ → τ} {f' : σ' → τ'} (h : ⇑eτ ∘ f = f' ∘ ⇑eσ) (x : PiTensorProduct R fun (x : σ) => B) : (reindex R (fun (x : τ) => B) eτ) ((fiberwiseMul f) x) = (fiberwiseMul f') ((reindex R (fun (x : σ) => B) eσ) x)

PiTensorProduct.fiberwiseMul is natural in the index map: reindexing along bijections of the source and target carries multiplication along f to multiplication along f' when the square eτ ∘ f = f' ∘ eσ commutes.

theorem PiTensorProduct.fiberwiseMul_sum_map {R : Type u_1} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} [Fintype σ] [DecidableEq τ] {B : Type u_6} [CommSemiring B] [Algebra R B] {σ' : Type u_7} {τ' : Type u_8} [Fintype σ'] [Finite τ] [Finite τ'] [DecidableEq τ'] (f : σ → τ) (g : σ' → τ') (x : PiTensorProduct R fun (x : σ) => B) (y : PiTensorProduct R fun (x : σ') => B) : (fiberwiseMul (Sum.map f g)) ((tmulEquiv R B) (x ⊗ₜ[R] y)) = (tmulEquiv R B) ((fiberwiseMul f) x ⊗ₜ[R] (fiberwiseMul g) y)

Multiplication along a disjoint union of index maps acts separately on its two tensor factors, through the native sum-indexed tensor equivalence.

@[simp]

theorem PiTensorProduct.fiberwiseMul_fiberwiseMul_surjInv {R : Type u_1} [CommSemiring R] {σ : Type u_2} {τ : Type u_3} [Fintype σ] [DecidableEq τ] {B : Type u_6} [CommSemiring B] [Algebra R B] [Fintype τ] [DecidableEq σ] {f : σ → τ} (hf : Function.Surjective f) (x : PiTensorProduct R fun (x : τ) => B) : (fiberwiseMul f) ((fiberwiseMul (Function.surjInv hf)) x) = x

For a constant family, multiplying along a section of a surjection f and then along f is the identity. In particular, multiplication along a surjection is surjective.