Cancelling a polynomial ring in a tensor product

If the C[X]-algebra structure on A extends its C-algebra structure, then base change from C[X] to S[X] is canonically the same as base change from C to S. This file constructs the resulting explicit S-algebra equivalence

S[X] ⊗[C[X]] A ≃ₐ[S] S ⊗[C] A

and records its values on pure tensors in both directions.

@[instance_reducible]

noncomputable def BGS.HasseWeil.coefficientPolynomialAlgebra (C : Type u_1) (S : Type u_2) [CommRing C] [CommRing S] [Algebra C S] : Algebra (Polynomial C) (Polynomial S)

The algebra structure from C[X] to S[X] used in the polynomial tensor cancel construction.

Equations

• BGS.HasseWeil.coefficientPolynomialAlgebra C S = Polynomial.algebra C S

theorem BGS.HasseWeil.coefficientPolynomialTower (C : Type u_1) (S : Type u_2) [CommRing C] [CommRing S] [Algebra C S] : IsScalarTower C (Polynomial C) (Polynomial S)

noncomputable def BGS.HasseWeil.polynomialTensorCancelEvaluationPoint (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] : TensorProduct C S A

The image of the polynomial variable in the constant tensor product.

Equations

• BGS.HasseWeil.polynomialTensorCancelEvaluationPoint C S A = Algebra.TensorProduct.includeRight ((algebraMap (Polynomial C) A) Polynomial.X)

noncomputable def BGS.HasseWeil.constantTensorPolynomialAlgHom (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] : Polynomial C →ₐ[C] TensorProduct C S A

Evaluate base polynomials in the constant tensor product.

Equations

• BGS.HasseWeil.constantTensorPolynomialAlgHom C S A = Polynomial.aeval (BGS.HasseWeil.polynomialTensorCancelEvaluationPoint C S A)

@[reducible]

noncomputable def BGS.HasseWeil.polynomialTensorCancelTargetPolynomialAlgebra (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] : Algebra (Polynomial C) (TensorProduct C S A)

The C[X]-algebra structure on S ⊗[C] A obtained by evaluating X at 1 ⊗ algebraMap C[X] A X.

Equations

• BGS.HasseWeil.polynomialTensorCancelTargetPolynomialAlgebra C S A = (BGS.HasseWeil.constantTensorPolynomialAlgHom C S A).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.constantTensorPolynomialAlgebra (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] : Algebra (Polynomial C) (TensorProduct C S A)

The algebra structure from C[X] to ((TensorProduct C S A)) used in the polynomial tensor cancel construction.

Equations

• BGS.HasseWeil.constantTensorPolynomialAlgebra C S A = BGS.HasseWeil.polynomialTensorCancelTargetPolynomialAlgebra C S A

@[reducible]

noncomputable def BGS.HasseWeil.polynomialTensorCancelTargetPolynomialExtensionAlgebra (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] : Algebra (Polynomial S) (TensorProduct C S A)

The S[X]-algebra structure on S ⊗[C] A obtained by evaluating X at 1 ⊗ algebraMap C[X] A X.

Equations

• BGS.HasseWeil.polynomialTensorCancelTargetPolynomialExtensionAlgebra C S A = (Polynomial.aeval (BGS.HasseWeil.polynomialTensorCancelEvaluationPoint C S A)).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.constantTensorPolynomialExtensionAlgebra (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] : Algebra (Polynomial S) (TensorProduct C S A)

The algebra structure from S[X] to ((TensorProduct C S A)) used in the polynomial tensor cancel construction.

Equations

• BGS.HasseWeil.constantTensorPolynomialExtensionAlgebra C S A = BGS.HasseWeil.polynomialTensorCancelTargetPolynomialExtensionAlgebra C S A

theorem BGS.HasseWeil.constantTensorPolynomialTower (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] : IsScalarTower C (Polynomial C) (TensorProduct C S A)

noncomputable def BGS.HasseWeil.rightFactorToConstantTensor (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] : A →ₐ[Polynomial C] TensorProduct C S A

Include the algebra factor in the constant tensor product over the polynomial base.

Equations

• BGS.HasseWeil.rightFactorToConstantTensor C S A = { toRingHom := Algebra.TensorProduct.includeRight.toRingHom, commutes' := ⋯ }

noncomputable def BGS.HasseWeil.leftFactorToConstantTensorOverS (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] : Polynomial S →ₐ[S] TensorProduct C S A

Evaluate coefficient polynomials in the constant tensor product.

Equations

• BGS.HasseWeil.leftFactorToConstantTensorOverS C S A = Polynomial.aeval (BGS.HasseWeil.polynomialTensorCancelEvaluationPoint C S A)

noncomputable def BGS.HasseWeil.leftFactorToConstantTensor (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] : Polynomial S →ₐ[Polynomial C] TensorProduct C S A

Evaluate coefficient polynomials as an algebra map over the polynomial base.

Equations

• BGS.HasseWeil.leftFactorToConstantTensor C S A = { toRingHom := (BGS.HasseWeil.leftFactorToConstantTensorOverS C S A).toRingHom, commutes' := ⋯ }

noncomputable def BGS.HasseWeil.polynomialTensorToConstantTensorOverPolynomial (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] : TensorProduct (Polynomial C) (Polynomial S) A →ₐ[Polynomial C] TensorProduct C S A

Cancel polynomial base change as an algebra homomorphism over the base polynomial ring.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGS.HasseWeil.polynomialTensorToConstantTensor (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] : TensorProduct (Polynomial C) (Polynomial S) A →ₐ[S] TensorProduct C S A

Cancel polynomial base change as an algebra homomorphism over the coefficient ring.

Equations

• BGS.HasseWeil.polynomialTensorToConstantTensor C S A = { toRingHom := (BGS.HasseWeil.polynomialTensorToConstantTensorOverPolynomial C S A).toRingHom, commutes' := ⋯ }

noncomputable def BGS.HasseWeil.constantsToPolynomialTensor (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra (Polynomial C) A] : S →ₐ[S] TensorProduct (Polynomial C) (Polynomial S) A

Include coefficient scalars in the polynomial tensor product.

Equations

• BGS.HasseWeil.constantsToPolynomialTensor C S A = Algebra.TensorProduct.includeLeft.comp Polynomial.CAlgHom

noncomputable def BGS.HasseWeil.rightFactorToPolynomialTensor (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] : A →ₐ[C] TensorProduct (Polynomial C) (Polynomial S) A

Include the algebra factor in the polynomial tensor product over the constant base.

Equations

• BGS.HasseWeil.rightFactorToPolynomialTensor C S A = AlgHom.restrictScalars C Algebra.TensorProduct.includeRight

noncomputable def BGS.HasseWeil.constantTensorToPolynomialTensor (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] : TensorProduct C S A →ₐ[S] TensorProduct (Polynomial C) (Polynomial S) A

Extend constant tensors to the polynomial tensor product.

Equations

• BGS.HasseWeil.constantTensorToPolynomialTensor C S A = Algebra.TensorProduct.lift (BGS.HasseWeil.constantsToPolynomialTensor C S A) (BGS.HasseWeil.rightFactorToPolynomialTensor C S A) ⋯

noncomputable def BGS.HasseWeil.constantTensorToPolynomialTensorOverPolynomial (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] : TensorProduct C S A →ₐ[Polynomial C] TensorProduct (Polynomial C) (Polynomial S) A

Extend constant tensors as an algebra homomorphism over the base polynomial ring.

Equations

• BGS.HasseWeil.constantTensorToPolynomialTensorOverPolynomial C S A = { toRingHom := (BGS.HasseWeil.constantTensorToPolynomialTensor C S A).toRingHom, commutes' := ⋯ }

noncomputable def BGS.HasseWeil.polynomialTensorToConstantTensorOverCoefficientPolynomial (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] : TensorProduct (Polynomial C) (Polynomial S) A →ₐ[Polynomial S] TensorProduct C S A

Cancel polynomial tensors over the coefficient polynomial ring.

Equations

• BGS.HasseWeil.polynomialTensorToConstantTensorOverCoefficientPolynomial C S A = { toRingHom := (BGS.HasseWeil.polynomialTensorToConstantTensor C S A).toRingHom, commutes' := ⋯ }

noncomputable def BGS.HasseWeil.constantTensorToPolynomialTensorOverCoefficientPolynomial (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] : TensorProduct C S A →ₐ[Polynomial S] TensorProduct (Polynomial C) (Polynomial S) A

Extend constant tensors over the coefficient polynomial ring.

Equations

• BGS.HasseWeil.constantTensorToPolynomialTensorOverCoefficientPolynomial C S A = { toRingHom := (BGS.HasseWeil.constantTensorToPolynomialTensor C S A).toRingHom, commutes' := ⋯ }

noncomputable def BGS.HasseWeil.polynomialTensorCancelOverPolynomial (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] : TensorProduct (Polynomial C) (Polynomial S) A ≃ₐ[Polynomial C] TensorProduct C S A

Polynomial tensor cancellation as a C[X]-algebra equivalence, where the target uses polynomialTensorCancelTargetPolynomialAlgebra.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGS.HasseWeil.polynomialTensorCancelOverCoefficientPolynomial (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] : TensorProduct (Polynomial C) (Polynomial S) A ≃ₐ[Polynomial S] TensorProduct C S A

Polynomial tensor cancellation as an S[X]-algebra equivalence, where the target uses polynomialTensorCancelTargetPolynomialExtensionAlgebra.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGS.HasseWeil.polynomialTensorCancel (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] : TensorProduct (Polynomial C) (Polynomial S) A ≃ₐ[S] TensorProduct C S A

Cancelling the polynomial base change in a tensor product.

Equations

• BGS.HasseWeil.polynomialTensorCancel C S A = AlgEquiv.ofAlgHom (BGS.HasseWeil.polynomialTensorToConstantTensor C S A) (BGS.HasseWeil.constantTensorToPolynomialTensor C S A) ⋯ ⋯

@[simp]

theorem BGS.HasseWeil.polynomialTensorCancelOverPolynomial_apply (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] (z : TensorProduct (Polynomial C) (Polynomial S) A) : (polynomialTensorCancelOverPolynomial C S A) z = (polynomialTensorCancel C S A) z

@[simp]

theorem BGS.HasseWeil.polynomialTensorCancelOverPolynomial_symm_apply (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] (z : TensorProduct C S A) : (polynomialTensorCancelOverPolynomial C S A).symm z = (polynomialTensorCancel C S A).symm z

@[simp]

theorem BGS.HasseWeil.polynomialTensorCancelOverCoefficientPolynomial_apply (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] (z : TensorProduct (Polynomial C) (Polynomial S) A) : (polynomialTensorCancelOverCoefficientPolynomial C S A) z = (polynomialTensorCancel C S A) z

@[simp]

theorem BGS.HasseWeil.polynomialTensorCancelOverCoefficientPolynomial_symm_apply (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] (z : TensorProduct C S A) : (polynomialTensorCancelOverCoefficientPolynomial C S A).symm z = (polynomialTensorCancel C S A).symm z

@[simp]

theorem BGS.HasseWeil.polynomialTensorCancel_tmul (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] (p : Polynomial S) (a : A) : (polynomialTensorCancel C S A) (p ⊗ₜ[Polynomial C] a) = (Polynomial.aeval (polynomialTensorCancelEvaluationPoint C S A)) p * 1 ⊗ₜ[C] a

@[simp]

theorem BGS.HasseWeil.polynomialTensorCancel_symm_tmul (C : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing C] [CommRing S] [CommRing A] [Algebra C S] [Algebra C A] [Algebra (Polynomial C) A] [IsScalarTower C (Polynomial C) A] (s : S) (a : A) : (polynomialTensorCancel C S A).symm (s ⊗ₜ[C] a) = Polynomial.C s ⊗ₜ[Polynomial C] a