Tensor powers of an algebra with surjective structure map

If algebraMap R A is surjective, as for a quotient ring R ⧸ I or for ZMod n over ℤ, then every element of A is the image of a scalar. Consequently all embeddings of A as a tensor factor of ⨂[R] _ : ι, A agree, and for a nonempty finite index type the tensor power is again A, by multiplication of the tensor factors. This is the indexed analogue of LinearMap.mul'_bijective_of_surjective. For ZMod n over ℤ it is the coefficient calculation used when tensor induction is applied to the trivial ZMod n-representation.

Main definitions

• PiTensorProduct.constantAlgEquivOfSurjective: multiplication of the tensor factors, PiTensorProduct.mulAlgHom, as an algebra equivalence from a nonempty finite tensor power of A to A.

Main results

• PiTensorProduct.singleAlgHom_eq_of_surjective: the factor embeddings all agree.
• PiTensorProduct.constantAlgEquivOfSurjective_tprod: the equivalence multiplies the factors of a pure tensor.
• PiTensorProduct.constantAlgEquivOfSurjective_symm_apply: its inverse is the embedding of A as any one of the tensor factors.

theorem PiTensorProduct.singleAlgHom_eq_of_surjective {R : Type u_1} {A : Type u_2} {ι : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq ι] (h : Function.Surjective ⇑(algebraMap R A)) (i j : ι) : singleAlgHom i = singleAlgHom j

If algebraMap R A is surjective, then the embeddings of A as the different tensor factors of ⨂[R] _ : ι, A all agree, since every element of A is the image of a scalar.

noncomputable def PiTensorProduct.constantAlgEquivOfSurjective {R : Type u_1} {A : Type u_2} {ι : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [Fintype ι] [Nonempty ι] (h : Function.Surjective ⇑(algebraMap R A)) : (PiTensorProduct R fun (x : ι) => A) ≃ₐ[R] A

If algebraMap R A is surjective, then a nonempty finite tensor power of A over R is canonically A, by multiplying the tensor factors.

@[simp]

theorem PiTensorProduct.constantAlgEquivOfSurjective_tprod {R : Type u_1} {A : Type u_2} {ι : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [Fintype ι] [Nonempty ι] (h : Function.Surjective ⇑(algebraMap R A)) (x : ι → A) : (constantAlgEquivOfSurjective h) ((tprod R) x) = ∏ i : ι, x i

The tensor-power equivalence multiplies the factors of a pure tensor.

theorem PiTensorProduct.constantAlgEquivOfSurjective_symm_apply {R : Type u_1} {A : Type u_2} {ι : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [Fintype ι] [Nonempty ι] [DecidableEq ι] (h : Function.Surjective ⇑(algebraMap R A)) (i : ι) (a : A) : (constantAlgEquivOfSurjective h).symm a = (singleAlgHom i) a

The inverse of the tensor-power equivalence embeds A as any one of the tensor factors.