Base change is compatible with ⊗, with ᵐᵒᵖ, and with itself

Scalar extension along a commutative K-algebra L distributes over the tensor product, commutes with passing to the opposite algebra, and composes in stages:

• TauCeti.lid_rTensor_distribBaseChange_symm: pairing against a linear functional commutes with distributing scalar extension over a tensor product.
• TauCeti.Algebra.TensorProduct.baseChangeTensorAlgEquiv: L ⊗[K] (A ⊗[K] B) ≃ₐ[L] (L ⊗[K] A) ⊗[L] (L ⊗[K] B);
• TauCeti.Algebra.TensorProduct.baseChangeOpAlgEquiv: L ⊗[K] Aᵐᵒᵖ ≃ₐ[L] (L ⊗[K] A)ᵐᵒᵖ;
• TauCeti.Algebra.TensorProduct.baseChangeTowerAlgEquiv: M ⊗[L] (L ⊗[K] A) ≃ₐ[M] M ⊗[K] A for a tower K → L → M.
• TauCeti.Algebra.TensorProduct.baseChangeTowerRingEquiv: the same tower comparison with tensor factors in coordinate-ring order, (L ⊗[K] A) ⊗[L] M ≃+* A ⊗[K] M.
• TauCeti.ScalarAut.semilinearMap: the scalar action as a semilinear map over L.
• TauCeti.ScalarAut.instMulSemiringAction: scalar automorphisms act on a scalar extension through its scalar factor.
• TauCeti.ScalarAut.baseChangeMap_smul: scalar extension of an algebra map is equivariant for scalar automorphisms.

Implementation notes

All four equivalences are opaque: their bodies are not @[expose]d, and the _tmul and _symm_tmul simp lemmas below are the whole public interface, in both directions.

Mathlib's Algebra.TensorProduct.cancelBaseChange is the third equivalence for a commutative algebra being extended; the algebras this file exists to serve are central simple, so they are not commutative in general, and the hypothesis has to go along with the chance to reuse that definition.

These are statements about scalar extension as such, with no central-simplicity hypotheses. They supply the compatibility isomorphisms needed to extend central simple algebras, Brauer classes, and coordinate rings along base field extensions.

References

P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, Section 2.2.

theorem TauCeti.lid_rTensor_distribBaseChange_symm {R : Type u} {A : Type v} {M : Type w} {N : Type x} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (l : A →ₗ[R] R) (y : TensorProduct R A M) (n : N) : (TensorProduct.lid R (TensorProduct R M N)) ((LinearMap.rTensor (TensorProduct R M N) l) ((TensorProduct.AlgebraTensorModule.distribBaseChange R A M N).symm (y ⊗ₜ[A] (1 ⊗ₜ[R] n)))) = (TensorProduct.lid R M) ((LinearMap.rTensor M l) y) ⊗ₜ[R] n

Pairing the scalar factor against an R-linear functional commutes with distributing scalar extension over a tensor product.

def TauCeti.Algebra.TensorProduct.baseChangeTensorAlgEquiv (K : Type u_1) (L : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] : TensorProduct K L (TensorProduct K A B) ≃ₐ[L] TensorProduct L (TensorProduct K L A) (TensorProduct K L B)

Base change distributes over the tensor product: extending A ⊗[K] B to L is the same as extending each factor and tensoring over L.

Neither factor has to be commutative, central, or simple. The underlying linear equivalence is TensorProduct.AlgebraTensorModule.distribBaseChange.

Equations

• TauCeti.Algebra.TensorProduct.baseChangeTensorAlgEquiv K L A B = Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (TensorProduct.AlgebraTensorModule.distribBaseChange K L A B) ⋯ ⋯

@[simp]

theorem TauCeti.Algebra.TensorProduct.baseChangeTensorAlgEquiv_tmul (K : Type u_1) (L : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (l : L) (a : A) (b : B) : (baseChangeTensorAlgEquiv K L A B) (l ⊗ₜ[K] (a ⊗ₜ[K] b)) = l ⊗ₜ[K] a ⊗ₜ[L] (1 ⊗ₜ[K] b)

Base change distribution sends pure tensors to pure tensors.

@[simp]

theorem TauCeti.Algebra.TensorProduct.baseChangeTensorAlgEquiv_symm_tmul (K : Type u_1) (L : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (l₁ l₂ : L) (a : A) (b : B) : (baseChangeTensorAlgEquiv K L A B).symm (l₁ ⊗ₜ[K] a ⊗ₜ[L] (l₂ ⊗ₜ[K] b)) = (l₁ * l₂) ⊗ₜ[K] (a ⊗ₜ[K] b)

The inverse base change distribution sends pure tensors to pure tensors.

def TauCeti.Algebra.TensorProduct.baseChangeOpAlgEquiv (K : Type u_1) (L : Type u_2) (A : Type u_3) [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Algebra K A] : TensorProduct K L Aᵐᵒᵖ ≃ₐ[L] (TensorProduct K L A)ᵐᵒᵖ

Base change commutes with passing to the opposite algebra. Together with TauCeti.Algebra.TensorProduct.baseChangeTensorAlgEquiv this is what makes base change respect both the multiplication and the inversion of Brauer classes.

Equations

• TauCeti.Algebra.TensorProduct.baseChangeOpAlgEquiv K L A = (Algebra.TensorProduct.congr (AlgEquiv.toOpposite L L) AlgEquiv.refl).trans (Algebra.TensorProduct.opAlgEquiv K L L A)

@[simp]

theorem TauCeti.Algebra.TensorProduct.baseChangeOpAlgEquiv_tmul (K : Type u_1) (L : Type u_2) (A : Type u_3) [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Algebra K A] (l : L) (a : Aᵐᵒᵖ) : (baseChangeOpAlgEquiv K L A) (l ⊗ₜ[K] a) = MulOpposite.op (l ⊗ₜ[K] MulOpposite.unop a)

@[simp]

theorem TauCeti.Algebra.TensorProduct.baseChangeOpAlgEquiv_symm_tmul (K : Type u_1) (L : Type u_2) (A : Type u_3) [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Algebra K A] (l : L) (a : A) : (baseChangeOpAlgEquiv K L A).symm (MulOpposite.op (l ⊗ₜ[K] a)) = l ⊗ₜ[K] MulOpposite.op a

Base change in stages

def TauCeti.Algebra.TensorProduct.baseChangeTowerAlgEquiv (K : Type u_1) (L : Type u_2) (A : Type u_3) [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Algebra K A] (M : Type u_5) [CommSemiring M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] : TensorProduct L M (TensorProduct K L A) ≃ₐ[M] TensorProduct K M A

Base change composes in stages: for a tower K → L → M, extending A first to L and then to M is extending it to M in one step, M ⊗[L] (L ⊗[K] A) ≃ₐ[M] M ⊗[K] A.

The underlying linear equivalence is TensorProduct.AlgebraTensorModule.cancelBaseChange. Unlike Algebra.TensorProduct.cancelBaseChange, this allows noncommutative A.

Equations

• TauCeti.Algebra.TensorProduct.baseChangeTowerAlgEquiv K L A M = (AlgEquiv.ofLinearEquiv (TensorProduct.AlgebraTensorModule.cancelBaseChange K L M M A).symm ⋯ ⋯).symm

@[simp]

theorem TauCeti.Algebra.TensorProduct.baseChangeTowerAlgEquiv_tmul (K : Type u_1) (L : Type u_2) (A : Type u_3) [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Algebra K A] (M : Type u_5) [CommSemiring M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (m : M) (l : L) (a : A) : (baseChangeTowerAlgEquiv K L A M) (m ⊗ₜ[L] (l ⊗ₜ[K] a)) = (l • m) ⊗ₜ[K] a

@[simp]

theorem TauCeti.Algebra.TensorProduct.baseChangeTowerAlgEquiv_symm_tmul (K : Type u_1) (L : Type u_2) (A : Type u_3) [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Algebra K A] (M : Type u_5) [CommSemiring M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (m : M) (a : A) : (baseChangeTowerAlgEquiv K L A M).symm (m ⊗ₜ[K] a) = m ⊗ₜ[L] (1 ⊗ₜ[K] a)

noncomputable def TauCeti.Algebra.TensorProduct.baseChangeTowerRingEquiv (K : Type u_5) (L : Type u_6) (A : Type u_7) (M : Type u_8) [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Algebra K A] [CommSemiring M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] : TensorProduct L (TensorProduct K L A) M ≃+* TensorProduct K A M

Successive scalar extension, with tensor factors in coordinate-ring order, agrees with direct scalar extension, also for noncommutative A.

Equations

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

@[simp]

theorem TauCeti.Algebra.TensorProduct.baseChangeTowerRingEquiv_tmul_tmul (K : Type u_5) (L : Type u_6) (A : Type u_7) (M : Type u_8) [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Algebra K A] [CommSemiring M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (l : L) (a : A) (m : M) : (baseChangeTowerRingEquiv K L A M) (l ⊗ₜ[K] a ⊗ₜ[L] m) = a ⊗ₜ[K] (l • m)

The coordinate-ring-order tower comparison sends nested pure tensors to pure tensors.

@[simp]

theorem TauCeti.Algebra.TensorProduct.baseChangeTowerRingEquiv_symm_tmul (K : Type u_5) (L : Type u_6) (A : Type u_7) (M : Type u_8) [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Algebra K A] [CommSemiring M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (a : A) (m : M) : (baseChangeTowerRingEquiv K L A M).symm (a ⊗ₜ[K] m) = 1 ⊗ₜ[K] a ⊗ₜ[L] m

The inverse coordinate-ring-order tower comparison sends pure tensors to nested pure tensors.

@[simp]

theorem TauCeti.ScalarAut.smul_tmul {K : Type u_1} {L : Type u_2} {A : Type u_3} [CommSemiring K] [Semiring L] [Algebra K L] [AddCommMonoid A] [Module K A] (σ : L ≃ₐ[K] L) (a : L) (x : A) : σ • a ⊗ₜ[K] x = σ a ⊗ₜ[K] x

Scalar multiplication on a pure tensor acts through the first factor.

theorem TauCeti.ScalarAut.smul_smulₛₗ {K : Type u_1} {L : Type u_2} {A : Type u_3} [CommSemiring K] [Semiring L] [Algebra K L] [AddCommMonoid A] [Module K A] (σ : L ≃ₐ[K] L) (a : L) (x : TensorProduct K L A) : σ • a • x = σ a • σ • x

The scalar-factor action is semilinear for the corresponding automorphism of L.

noncomputable def TauCeti.ScalarAut.semilinearMap {K : Type u_1} {L : Type u_2} {A : Type u_3} [CommSemiring K] [Semiring L] [Algebra K L] [AddCommMonoid A] [Module K A] (σ : L ≃ₐ[K] L) : TensorProduct K L A →ₛₗ[σ.toRingEquiv.toRingHom] TensorProduct K L A

The scalar action as a semilinear map over L.

Equations

• TauCeti.ScalarAut.semilinearMap σ = { toFun := fun (x : TensorProduct K L A) => σ • x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.ScalarAut.semilinearMap_apply {K : Type u_1} {L : Type u_2} {A : Type u_3} [CommSemiring K] [Semiring L] [Algebra K L] [AddCommMonoid A] [Module K A] (σ : L ≃ₐ[K] L) (x : TensorProduct K L A) : (semilinearMap σ) x = σ • x

The semilinear scalar map agrees pointwise with the scalar action.

@[instance_reducible]

noncomputable instance TauCeti.ScalarAut.instMulSemiringAction {K : Type u_1} {L : Type u_2} {A : Type u_3} [CommSemiring K] [Semiring L] [Algebra K L] [Semiring A] [Algebra K A] : MulSemiringAction (L ≃ₐ[K] L) (TensorProduct K L A)

Scalar automorphisms act on a scalar extension through the scalar factor.

Equations

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

theorem TauCeti.ScalarAut.smul_def {K : Type u_1} {L : Type u_2} {A : Type u_3} [CommSemiring K] [Semiring L] [Algebra K L] [Semiring A] [Algebra K A] (σ : L ≃ₐ[K] L) (x : TensorProduct K L A) : σ • x = (Algebra.TensorProduct.congr σ AlgEquiv.refl) x

Scalar multiplication on a base change is the tensor-product congruence.

@[simp]

theorem TauCeti.ScalarAut.baseChangeMap_smul {K : Type u_1} {L : Type u_2} {A : Type u_3} [CommSemiring K] [Semiring L] [Algebra K L] [Semiring A] [Algebra K A] {B : Type u_4} [Semiring B] [Algebra K B] (f : A →ₐ[K] B) (σ : L ≃ₐ[K] L) (x : TensorProduct K L A) : (Algebra.TensorProduct.map (AlgHom.id K L) f) (σ • x) = σ • (Algebra.TensorProduct.map (AlgHom.id K L) f) x

Scalar extension of an algebra morphism commutes with the scalar-factor action.