Maps between tensor products of algebras

The base change Algebra.TensorProduct.map (AlgHom.id R S) f : S ⊗[R] B → S ⊗[R] C of an algebra map f : B →ₐ[R] C agrees with LinearMap.lTensor S applied to the underlying linear map of f, and similarly on the right with LinearMap.rTensor S. This lets results about base change of linear maps, such as flatness preserving injectivity and exactness, be applied to base change of algebra maps.

For an S-algebra B over R which need not be commutative, the multiplication maps S ⊗[R] B → B and B ⊗[R] S → B are S-algebra maps, because S acts through its central image in B. Mathlib's Algebra.TensorProduct.lmul'' and Algebra.TensorProduct.productMap require a commutative target.

For commutative R-algebras A and B, the tensor product A ⊗[R] B is the pushout of A ← R → B in commutative semirings. Mathlib's Algebra.TensorProduct.productMap expresses this universal property for algebra homomorphisms into an R-algebra, and Algebra.TensorProduct.ringHom_ext is its uniqueness half for ring homomorphisms. Algebra.TensorProduct.liftRingHom is the existence half for ring homomorphisms: ring homomorphisms x : A →+* T and y : B →+* T into a commutative semiring T which agree on R induce a ⊗ b ↦ x a * y b, even for noncommutative A and B, with no R-algebra structure on T involved. This is the form needed when T already carries an R-algebra structure which x and y do not respect, for instance when T is itself a tensor product over R and x twists the first factor by a ring automorphism.

Mathlib's LinearMap.tensorProduct and LinearMap.tensorProductEnd send a ⊗ f to a times the base change of f, but their generated computation lemmas unfold to TensorProduct.liftAux; this file records their values on pure tensors as simp lemmas of higher priority than the generated ones, so the public LinearMap.baseChange API applies.

Main declarations

• Subalgebra.toSubmodule_baseChange: the underlying submodule of C.baseChange T is (Subalgebra.toSubmodule C).baseChange T.
• AlgHom.lTensor_toLinearMap_apply: f.toLinearMap.lTensor S is Algebra.TensorProduct.map (AlgHom.id R S) f.
• AlgHom.rTensor_toLinearMap_apply: f.toLinearMap.rTensor S is Algebra.TensorProduct.map f (AlgHom.id R S).
• AlgHom.lTensor_rTensor_comm: scalar extension of an algebra map commutes with changing the coefficient algebra.
• LinearMap.tensorProduct_tmul, LinearMap.tensorProductEnd_tmul: the extension of linear maps and of endomorphisms sends a ⊗ f to a • f.baseChange A.
• Algebra.TensorProduct.mulLeft, Algebra.TensorProduct.mulRight: the multiplication maps s ⊗ b ↦ s • b and b ⊗ t ↦ b * t.
• Algebra.TensorProduct.liftRingHom x y h: the ring homomorphism a ⊗ b ↦ x a * y b.
• Algebra.TensorProduct.map_productMap_eq_zero_of_comp_eq: if p : T → U equalizes f, g : S → T, then p kills productMap f g e (s ⊗ t ↦ f s * g t) for every e in the kernel of multiplication S ⊗[R] S → S.
• Algebra.TensorProduct.productMap_mem_of_comp_eq: if f, g agree modulo an ideal J of T, then productMap f g e ∈ J for every such e.
• AlgHom.comp_productMap, AlgHom.productMap_comp_includeLeft_includeRight: post-composition distributes over productMap, and an algebra map g out of H₁ ⊗[R] H₂ is the productMap of its restrictions along the two canonical inclusions; H₁ and H₂ need not be commutative.
• Algebra.TensorProduct.mulLeft_map, Algebra.TensorProduct.mulLeft_map_includeRight: naturality of tensor multiplication and cancellation of an inserted middle factor 1.
• Algebra.TensorProduct.map_rTensor_eq_rTensor_lTensor: g ⊗ φ after f ⊗ id is (g ∘ f) ⊗ id after id ⊗ φ, for algebra maps g, φ and a linear map f.
• Algebra.TensorProduct.map_assoc_tmul_one: applying f : B ⊗[R] C → D after reassociating y ⊗ 1 is the base change of b ↦ f (b ⊗ 1).
• Algebra.TensorProduct.assoc_comp_includeLeft_comp_includeLeft, Algebra.TensorProduct.assoc_comp_includeLeft_comp_includeRight, Algebra.TensorProduct.assoc_comp_includeRight: the associator restricted to each of the three tensor factors.
• Algebra.TensorProduct.mapRingHom_id_eq_map, Algebra.TensorProduct.mapRingHom_id_surjective, Algebra.TensorProduct.ker_mapRingHom_id: over the identity of the base, mapRingHom is Algebra.TensorProduct.map; for surjective maps it is surjective, and its kernel is generated by the two kernels.
• AlgHom.sectionBaseChange: the base change T ⊗[A] B →ₐ[T] T of an A-algebra map s : B →ₐ[A] A, that is, the pullback to Spec T of the section of Spec B → Spec A given by s, with its value AlgHom.sectionBaseChange_sum_tmul on sums of pure tensors, its naturality AlgHom.sectionBaseChange_rTensor in T, and its transitivity AlgHom.sectionBaseChange_sectionBaseChange along A → A' → T.
• AlgHom.semilinearTwist y σ φ hφ: the twist (σ⁻¹ ⊗ T) ∘ y ∘ φ of an algebra map y : D →ₐ[C] C ⊗[A] T by a ring homomorphism φ semilinear over an automorphism σ of C.

theorem Subalgebra.toSubmodule_baseChange {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] (T : Type u_3) [CommSemiring T] [Algebra R T] (C : Subalgebra R S) : toSubmodule (baseChange T C) = Submodule.baseChange T (toSubmodule C)

The underlying submodule of a base-changed subalgebra is the base change of its underlying submodule.

theorem AlgHom.lTensor_toLinearMap_apply {R : Type u_1} {B : Type u_2} {C : Type u_3} (S : Type u_4) [CommSemiring R] [Semiring S] [Algebra R S] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : B →ₐ[R] C) (x : TensorProduct R S B) : (LinearMap.lTensor S f.toLinearMap) x = (Algebra.TensorProduct.map (AlgHom.id R S) f) x

Base change of the underlying linear map of an algebra map is the base change of the algebra map.

theorem AlgHom.rTensor_toLinearMap_apply {R : Type u_1} {B : Type u_2} {C : Type u_3} (S : Type u_4) [CommSemiring R] [Semiring S] [Algebra R S] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : B →ₐ[R] C) (x : TensorProduct R B S) : (LinearMap.rTensor S f.toLinearMap) x = (Algebra.TensorProduct.map f (AlgHom.id R S)) x

Right base change of the underlying linear map of an algebra map is the right base change of the algebra map.

@[simp]

theorem LinearMap.tensorProduct_tmul {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (a : A) (f : M →ₗ[R] N) : (tensorProduct R A M N) (a ⊗ₜ[R] f) = a • baseChange A f

The natural map A ⊗[R] (M →ₗ[R] N) → (A ⊗[R] M →ₗ[A] A ⊗[R] N) sends a ⊗ f to a • f.baseChange A, so that LinearMap.baseChange_tmul computes its values on pure tensors.

@[simp]

theorem LinearMap.tensorProductEnd_tmul {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (a : A) (f : Module.End R M) : (tensorProductEnd R A M) (a ⊗ₜ[R] f) = a • baseChange A f

The natural algebra map A ⊗[R] Module.End R M → Module.End A (A ⊗[R] M) sends a ⊗ f to a • f.baseChange A.

theorem AlgHom.lTensor_rTensor_comm {R : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} {E : Type u_5} [CommSemiring R] [CommSemiring B] [Algebra R B] [CommSemiring C] [Algebra R C] [Semiring D] [Algebra R D] [Semiring E] [Algebra R E] (φ : D →ₐ[R] E) (ρ : B →ₐ[R] C) (x : TensorProduct R B D) : (Algebra.TensorProduct.lTensor C φ) ((Algebra.TensorProduct.rTensor D ρ) x) = (Algebra.TensorProduct.rTensor E ρ) ((Algebra.TensorProduct.lTensor B φ) x)

Extension of scalars of an algebra map commutes with changing the coefficient algebra.

noncomputable def Algebra.TensorProduct.liftRingHom {R : Type u_1} {A : Type u_2} {B : Type u_3} {T : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CommSemiring T] (x : A →+* T) (y : B →+* T) (h : x.comp (algebraMap R A) = y.comp (algebraMap R B)) : TensorProduct R A B →+* T

The ring homomorphism A ⊗[R] B →+* T, a ⊗ b ↦ x a * y b, induced by ring homomorphisms x : A →+* T and y : B →+* T which agree on R. The sources A and B need not be commutative, and no R-algebra structure on T is involved.

@[simp]

theorem Algebra.TensorProduct.liftRingHom_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} {T : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CommSemiring T] (x : A →+* T) (y : B →+* T) (h : x.comp (algebraMap R A) = y.comp (algebraMap R B)) (a : A) (b : B) : (liftRingHom x y h) (a ⊗ₜ[R] b) = x a * y b

@[simp]

theorem Algebra.TensorProduct.liftRingHom_comp_includeLeftRingHom {R : Type u_1} {A : Type u_2} {B : Type u_3} {T : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CommSemiring T] (x : A →+* T) (y : B →+* T) (h : x.comp (algebraMap R A) = y.comp (algebraMap R B)) : (liftRingHom x y h).comp includeLeftRingHom = x

@[simp]

theorem Algebra.TensorProduct.liftRingHom_comp_includeRight {R : Type u_1} {A : Type u_2} {B : Type u_3} {T : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CommSemiring T] (x : A →+* T) (y : B →+* T) (h : x.comp (algebraMap R A) = y.comp (algebraMap R B)) : (liftRingHom x y h).comp ↑includeRight = y

theorem Algebra.TensorProduct.map_assoc_tmul_one {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {C : Type u_5} {D : Type u_6} [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : TensorProduct R B C →ₐ[R] D) (y : TensorProduct R A B) : (map (AlgHom.id R A) f) ((TensorProduct.assoc R R R A B C) (y ⊗ₜ[R] 1)) = (map (AlgHom.id R A) (f.comp includeLeft)) y

Reassociating y ⊗ 1 ∈ (A ⊗[R] B) ⊗[R] C and applying f : B ⊗[R] C → D to the last two factors is the base change of b ↦ f (b ⊗ 1).

theorem Algebra.TensorProduct.map_rTensor_eq_rTensor_lTensor {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {M : Type u_5} {C : Type u_6} {D : Type u_7} [AddCommMonoid M] [Module R M] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (g : A →ₐ[R] C) (φ : B →ₐ[R] D) (f : M →ₗ[R] A) (z : TensorProduct R M B) : (map g φ) ((LinearMap.rTensor B f) z) = (LinearMap.rTensor D (g.toLinearMap ∘ₗ f)) ((LinearMap.lTensor M φ.toLinearMap) z)

Applying g ⊗ φ after f ⊗ id, for algebra maps g, φ and a linear map f into the source of g, is applying id ⊗ φ and then (g ∘ f) ⊗ id. For g the identity this lets tensor constructions on the image of f pass through a change of the coefficient algebra.

theorem Algebra.TensorProduct.assoc_comp_includeLeft_comp_includeLeft {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {C : Type u_5} [Semiring C] [Algebra R C] : ((↑(TensorProduct.assoc R R R A B C)).comp includeLeft).comp includeLeft = includeLeft

Restricting the associator (A ⊗[R] B) ⊗[R] C ≃ A ⊗[R] (B ⊗[R] C) to the left factor A gives the inclusion of the left factor.

theorem Algebra.TensorProduct.assoc_comp_includeLeft_comp_includeRight {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {C : Type u_5} [Semiring C] [Algebra R C] : ((↑(TensorProduct.assoc R R R A B C)).comp includeLeft).comp includeRight = includeRight.comp includeLeft

Restricting the associator (A ⊗[R] B) ⊗[R] C ≃ A ⊗[R] (B ⊗[R] C) to the middle factor B gives the inclusion of B into the left factor of B ⊗[R] C.

theorem Algebra.TensorProduct.assoc_comp_includeRight {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {C : Type u_5} [Semiring C] [Algebra R C] : (↑(TensorProduct.assoc R R R A B C)).comp includeRight = includeRight.comp includeRight

Restricting the associator (A ⊗[R] B) ⊗[R] C ≃ A ⊗[R] (B ⊗[R] C) to the right factor C gives the inclusion of C into the right factor of B ⊗[R] C.

theorem Algebra.TensorProduct.commute_one_tmul_algebraMap {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Algebra S B] (x : TensorProduct R A B) (t : S) : Commute x (1 ⊗ₜ[R] (algebraMap S B) t)

The image of S in the right factor is central in A ⊗[R] B.

noncomputable def Algebra.TensorProduct.mulLeft {R : Type u_1} {S : Type u_2} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring B] [Algebra R B] [Algebra S B] [Algebra R S] [IsScalarTower R S B] : TensorProduct R S B →ₐ[S] B

The multiplication map S ⊗[R] B →ₐ[S] B, s ⊗ b ↦ s • b, for an S-algebra B which need not be commutative.

@[simp]

theorem Algebra.TensorProduct.mulLeft_tmul {R : Type u_1} {S : Type u_2} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring B] [Algebra R B] [Algebra S B] [Algebra R S] [IsScalarTower R S B] (s : S) (b : B) : mulLeft (s ⊗ₜ[R] b) = (algebraMap S B) s * b

@[simp]

theorem Algebra.TensorProduct.mulLeft_map {R : Type u_1} {S : Type u_2} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring B] [Algebra R B] [Algebra S B] [Algebra R S] [IsScalarTower R S B] {C : Type u_5} [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] (f : B →ₐ[S] C) (x : TensorProduct R S B) : mulLeft ((map (AlgHom.id R S) (AlgHom.restrictScalars R f)) x) = f (mulLeft x)

Tensor multiplication commutes with an algebra map over S.

@[simp]

theorem Algebra.TensorProduct.mulLeft_map_includeRight {R : Type u_1} {S : Type u_2} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring B] [Algebra R B] [Algebra R S] (x : TensorProduct R S B) : mulLeft ((map (AlgHom.id R S) includeRight) x) = x

Multiplying the first two factors cancels insertion of 1 in the middle factor.

noncomputable def Algebra.TensorProduct.mulRight {R : Type u_1} {S : Type u_2} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring B] [Algebra R B] [Algebra S B] [Algebra R S] [IsScalarTower R S B] : TensorProduct R B S →ₐ[S] B

The multiplication map B ⊗[R] S →ₐ[S] B, b ⊗ t ↦ b * t, for an S-algebra B which need not be commutative.

@[simp]

theorem Algebra.TensorProduct.mulRight_tmul {R : Type u_1} {S : Type u_2} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring B] [Algebra R B] [Algebra S B] [Algebra R S] [IsScalarTower R S B] (b : B) (t : S) : mulRight (b ⊗ₜ[R] t) = b * (algebraMap S B) t

theorem Algebra.TensorProduct.lmul'_surjective (R : Type u_5) (A : Type u_6) [CommSemiring R] [CommSemiring A] [Algebra R A] : Function.Surjective ⇑(lmul' R)

Multiplication on a self-tensor product is surjective.

@[simp]

theorem Algebra.TensorProduct.lmul'_map_self {R : Type u_5} {A : Type u_6} {C : Type u_7} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Algebra R A] [Algebra R C] (f : A →ₐ[R] C) (x : TensorProduct R A A) : (lmul' R) ((map f f) x) = f ((lmul' R) x)

Multiplication on a self-tensor product is natural in the algebra.

theorem Algebra.TensorProduct.map_productMap_eq_zero_of_comp_eq {R : Type u_5} {S : Type u_6} {T : Type u_7} {U : Type u_8} [CommSemiring R] [CommSemiring S] [CommSemiring T] [Semiring U] [Algebra R S] [Algebra R T] [Algebra R U] {e : TensorProduct R S S} (he : (lmul' R) e = 0) {f g : S →ₐ[R] T} (p : T →ₐ[R] U) (hfg : p.comp f = p.comp g) : p ((productMap f g) e) = 0

If two algebra maps f, g : S → T agree after composing with p : T → U, then p kills productMap f g e (the map s ⊗ t ↦ f s * g t applied to e) for every element e of the kernel of multiplication S ⊗[R] S → S.

theorem Algebra.TensorProduct.productMap_mem_of_comp_eq {R : Type u_5} {S : Type u_6} {T : Type u_7} [CommSemiring R] [CommSemiring S] [CommRing T] [Algebra R S] [Algebra R T] {e : TensorProduct R S S} (he : (lmul' R) e = 0) (J : Ideal T) {f g : S →ₐ[R] T} (hfg : (Ideal.Quotient.mkₐ R J).comp f = (Ideal.Quotient.mkₐ R J).comp g) : (productMap f g) e ∈ J

If two algebra maps f, g : S → T agree modulo an ideal J of T, then productMap f g (the map s ⊗ t ↦ f s * g t) sends every element of the kernel of multiplication S ⊗[R] S → S into J.

theorem Algebra.TensorProduct.mapRingHom_id_eq_map {R : Type u_5} {S : Type u_6} {S' : Type u_7} {T : Type u_8} {T' : Type u_9} [CommRing R] [CommRing S] [CommRing S'] [CommRing T] [CommRing T'] [Algebra R S] [Algebra R S'] [Algebra R T] [Algebra R T'] {fS : S →+* S'} {fT : T →+* T'} (HS : fS.comp (algebraMap R S) = algebraMap R S') (HT : fT.comp (algebraMap R T) = algebraMap R T') : mapRingHom (RingHom.id R) fS fT HS HT = ↑(map { toRingHom := fS, commutes' := ⋯ } { toRingHom := fT, commutes' := ⋯ })

Over the identity of R, the ring homomorphism mapRingHom of ring homomorphisms commuting with the structure maps is Algebra.TensorProduct.map of the corresponding R-algebra maps.

theorem Algebra.TensorProduct.mapRingHom_id_surjective {R : Type u_5} {S : Type u_6} {S' : Type u_7} {T : Type u_8} {T' : Type u_9} [CommRing R] [CommRing S] [CommRing S'] [CommRing T] [CommRing T'] [Algebra R S] [Algebra R S'] [Algebra R T] [Algebra R T'] {fS : S →+* S'} {fT : T →+* T'} (HS : fS.comp (algebraMap R S) = algebraMap R S') (HT : fT.comp (algebraMap R T) = algebraMap R T') (hS : Function.Surjective ⇑fS) (hT : Function.Surjective ⇑fT) : Function.Surjective ⇑(mapRingHom (RingHom.id R) fS fT HS HT)

mapRingHom of surjective ring homomorphisms over the identity of R is surjective.

theorem Algebra.TensorProduct.ker_mapRingHom_id {R : Type u_5} {S : Type u_6} {S' : Type u_7} {T : Type u_8} {T' : Type u_9} [CommRing R] [CommRing S] [CommRing S'] [CommRing T] [CommRing T'] [Algebra R S] [Algebra R S'] [Algebra R T] [Algebra R T'] {fS : S →+* S'} {fT : T →+* T'} (HS : fS.comp (algebraMap R S) = algebraMap R S') (HT : fT.comp (algebraMap R T) = algebraMap R T') (hS : Function.Surjective ⇑fS) (hT : Function.Surjective ⇑fT) : RingHom.ker (mapRingHom (RingHom.id R) fS fT HS HT) = Ideal.map includeLeft (RingHom.ker fS) ⊔ Ideal.map includeRight (RingHom.ker fT)

Right exactness of the tensor product for ring homomorphisms. The kernel of mapRingHom of surjective ring homomorphisms fS, fT over the identity of R is generated by the images of ker fS and ker fT (Algebra.TensorProduct.map_ker).

theorem AlgHom.comp_productMap {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [Semiring H₁] [Semiring H₂] [CommSemiring A] [CommSemiring B] [Algebra R H₁] [Algebra R H₂] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (f₁ : H₁ →ₐ[R] A) (f₂ : H₂ →ₐ[R] A) : φ.comp (Algebra.TensorProduct.productMap f₁ f₂) = Algebra.TensorProduct.productMap (φ.comp f₁) (φ.comp f₂)

Post-composition distributes over the tensor-product map induced by a pair of algebra maps.

@[simp]

theorem AlgHom.productMap_comp_includeLeft_includeRight {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring H₁] [Semiring H₂] [CommSemiring A] [Algebra R H₁] [Algebra R H₂] [Algebra R A] (g : TensorProduct R H₁ H₂ →ₐ[R] A) : Algebra.TensorProduct.productMap (g.comp Algebra.TensorProduct.includeLeft) (g.comp Algebra.TensorProduct.includeRight) = g

An algebra map out of a tensor product is recovered from its two restrictions.

noncomputable def AlgHom.sectionBaseChange {A : Type u_1} {B : Type u_2} [CommSemiring A] [Semiring B] [Algebra A B] (s : B →ₐ[A] A) (T : Type u_3) [CommSemiring T] [Algebra A T] : TensorProduct A T B →ₐ[T] T

The base change T ⊗[A] B →ₐ[T] T, t ⊗ b ↦ t * s b, of an A-algebra map s : B →ₐ[A] A. Geometrically, s is a section of Spec B → Spec A, and this is its pullback along Spec T → Spec A.

@[simp]

theorem AlgHom.sectionBaseChange_tmul {A : Type u_1} {B : Type u_2} [CommSemiring A] [Semiring B] [Algebra A B] (s : B →ₐ[A] A) {T : Type u_3} [CommSemiring T] [Algebra A T] (t : T) (b : B) : (s.sectionBaseChange T) (t ⊗ₜ[A] b) = t * (algebraMap A T) (s b)

theorem AlgHom.sectionBaseChange_sum_tmul {A : Type u_1} {B : Type u_2} [CommSemiring A] [Semiring B] [Algebra A B] (s : B →ₐ[A] A) {T : Type u_3} [CommSemiring T] [Algebra A T] {κ : Type u_4} (u : Finset κ) (t : κ → T) (b : κ → B) : (s.sectionBaseChange T) (∑ j ∈ u, t j ⊗ₜ[A] b j) = ∑ j ∈ u, s (b j) • t j

The base change of a section s takes ∑ j ∈ u, tⱼ ⊗ bⱼ to ∑ j ∈ u, s(bⱼ) • tⱼ; for tⱼ = Xⱼ and a basis b, the generic element goes to the linear form with coefficients s(bⱼ).

@[simp]

theorem AlgHom.sectionBaseChange_rTensor {A : Type u_1} {B : Type u_2} [CommSemiring A] [Semiring B] [Algebra A B] (s : B →ₐ[A] A) {T : Type u_3} {T' : Type u_4} [CommSemiring T] [Algebra A T] [CommSemiring T'] [Algebra A T'] (φ : T →ₐ[A] T') (x : TensorProduct A T B) : (s.sectionBaseChange T') ((Algebra.TensorProduct.rTensor B φ) x) = φ ((s.sectionBaseChange T) x)

The base change of a section is natural in the base: it commutes with Algebra.TensorProduct.rTensor B φ for an A-algebra map φ : T →ₐ[A] T'.

@[simp]

theorem AlgHom.sectionBaseChange_sectionBaseChange {A : Type u_1} [CommSemiring A] {B : Type u_3} [CommSemiring B] [Algebra A B] (s : B →ₐ[A] A) {A' : Type u_4} {T : Type u_5} [CommSemiring A'] [Algebra A A'] [CommSemiring T] [Algebra A T] [Algebra A' T] [IsScalarTower A A' T] (x : TensorProduct A' T (TensorProduct A A' B)) : ((s.sectionBaseChange A').sectionBaseChange T) x = (s.sectionBaseChange T) ((Algebra.TensorProduct.cancelBaseChange A A' T T B) x)

Base change of a section is transitive: along A → A' → T, base changing s to A' and then to T is base changing s to T, through the identification T ⊗[A'] (A' ⊗[A] B) ≃ T ⊗[A] B.

noncomputable def AlgHom.semilinearTwist {A : Type u_1} [CommSemiring A] {C : Type u_3} {D : Type u_4} {T : Type u_5} [CommSemiring C] [Algebra A C] [Semiring D] [Semiring T] [Algebra A T] [Algebra C D] {E : Type u_6} [Semiring E] [Algebra C E] (y : D →ₐ[C] TensorProduct A C T) (σ : C ≃ₐ[A] C) (φ : E →+* D) (hφ : ∀ (c : C), φ ((algebraMap C E) c) = (algebraMap C D) (σ c)) : E →ₐ[C] TensorProduct A C T

The semilinear twist of an algebra map y : D →ₐ[C] C ⊗[A] T, where C is a commutative A-algebra, by a ring homomorphism φ : E →+* D semilinear over an A-algebra automorphism σ of C, in the sense that φ (c • e) = σ c • φ e: the composite (σ⁻¹ ⊗ T) ∘ y ∘ φ. Neither y ∘ φ nor σ⁻¹ ⊗ T is C-linear, but their composite is.

@[simp]

theorem AlgHom.semilinearTwist_apply {A : Type u_1} [CommSemiring A] {C : Type u_3} {D : Type u_4} {T : Type u_5} [CommSemiring C] [Algebra A C] [Semiring D] [Semiring T] [Algebra A T] [Algebra C D] {E : Type u_6} [Semiring E] [Algebra C E] (y : D →ₐ[C] TensorProduct A C T) (σ : C ≃ₐ[A] C) (φ : E →+* D) (hφ : ∀ (c : C), φ ((algebraMap C E) c) = (algebraMap C D) (σ c)) (e : E) : (y.semilinearTwist σ φ hφ) e = (Algebra.TensorProduct.rTensor T ↑σ.symm) (y (φ e))