Base change of endomorphisms of a scalar extension

Let M be a module over a commutative semiring R, and let f : A →ₐ[R] B be a morphism of commutative R-algebras. Scalar extension of M is compared by the f-semilinear map

LinearMap.rTensor M f.toLinearMap : A ⊗[R] M → B ⊗[R] M.

An A-linear endomorphism of A ⊗[R] M transports along this comparison to a unique B-linear endomorphism of B ⊗[R] M. This file constructs that transport, mapValue, proves that the transport square characterizes it, and records that it is additive and multiplicative in the endomorphism, and functorial in the value algebra. It also transports the two compatibilities needed for monoidal arguments: naturality in M and the tensor comparison (A ⊗ M) ⊗[A] (A ⊗ N) ≃ A ⊗ (M ⊗ N).

The name follows TauCeti.AlgHom.mapValue, which transports an algebra-valued point along a morphism of value algebras; the two are compatible in TauCeti.Comodule.rTensor_comp_endOfPoint.

Main declarations

• TauCeti.rTensor_algHom_smul: the comparison map is semilinear over f.
• Module.End.mapValue: the transported endomorphism.
• Module.End.mapValue_comp_rTensor: the defining transport square.
• Module.End.eq_mapValue: the transport square characterizes the transport.
• Module.End.mapValue_algebraMap: transport preserves scalar endomorphisms.
• Module.End.mapValue_aeval: polynomial evaluation commutes with transport.
• Module.End.mapValueRingHom: the transport as a ring homomorphism.
• Module.End.mapValueGL: the transport on general linear groups.
• Module.End.baseChange_comp_mapValue: transport preserves naturality in the module.
• Module.End.distribBaseChange_comp_mapValue: transport preserves the tensor comparison.

theorem TauCeti.rTensor_algHom_smul {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) (a : A) (z : TensorProduct R A M) : (LinearMap.rTensor M f.toLinearMap) (a • z) = f a • (LinearMap.rTensor M f.toLinearMap) z

The comparison A ⊗[R] M → B ⊗[R] M of scalar extensions induced by a morphism f of value algebras is semilinear over f.

noncomputable def Module.End.mapValue {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) (φ : End A (TensorProduct R A M)) : End B (TensorProduct R B M)

Base change of an endomorphism of a scalar extension along a morphism f : A →ₐ[R] B of value algebras: the unique B-linear endomorphism of B ⊗[R] M compatible with φ along the comparison map.

Equations

• Module.End.mapValue f φ = LinearMap.liftBaseChange B (LinearMap.rTensor M f.toLinearMap ∘ₗ ↑R φ ∘ₗ (TensorProduct.mk R A M) 1)

@[simp]

theorem Module.End.mapValue_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) (φ : End A (TensorProduct R A M)) (b : B) (m : M) : (mapValue f φ) (b ⊗ₜ[R] m) = b • (LinearMap.rTensor M f.toLinearMap) (φ (1 ⊗ₜ[R] m))

Evaluation of a base-changed endomorphism on a pure tensor.

theorem Module.End.mapValue_comp_rTensor {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) (φ : End A (TensorProduct R A M)) : ↑R (mapValue f φ) ∘ₗ LinearMap.rTensor M f.toLinearMap = LinearMap.rTensor M f.toLinearMap ∘ₗ ↑R φ

The transport square defining base change of an endomorphism: transporting and then comparing scalar extensions agrees with comparing and then applying the original endomorphism.

@[simp]

theorem Module.End.mapValue_rTensor_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) (φ : End A (TensorProduct R A M)) (z : TensorProduct R A M) : (mapValue f φ) ((LinearMap.rTensor M f.toLinearMap) z) = (LinearMap.rTensor M f.toLinearMap) (φ z)

Evaluation form of the transport square.

theorem Module.End.eq_mapValue {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) (φ : End A (TensorProduct R A M)) (ψ : End B (TensorProduct R B M)) (h : ↑R ψ ∘ₗ LinearMap.rTensor M f.toLinearMap = LinearMap.rTensor M f.toLinearMap ∘ₗ ↑R φ) : ψ = mapValue f φ

The transport square characterizes base change of an endomorphism: the comparison map generates B ⊗[R] M over B.

@[simp]

theorem Module.End.mapValue_one {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) : mapValue f 1 = 1

Base change preserves the identity endomorphism.

@[simp]

theorem Module.End.mapValue_mul {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) (φ ψ : End A (TensorProduct R A M)) : mapValue f (φ * ψ) = mapValue f φ * mapValue f ψ

Base change is multiplicative: it turns composition into composition.

@[simp]

theorem Module.End.mapValue_zero {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) : mapValue f 0 = 0

Base change preserves the zero endomorphism.

@[simp]

theorem Module.End.mapValue_add {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) (φ ψ : End A (TensorProduct R A M)) : mapValue f (φ + ψ) = mapValue f φ + mapValue f ψ

Base change is additive.

@[simp]

theorem Module.End.mapValue_algebraMap {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) (a : A) : mapValue f ((algebraMap A (End A (TensorProduct R A M))) a) = (algebraMap B (End B (TensorProduct R B M))) (f a)

Scalar extension carries scalar endomorphisms to the corresponding scalar endomorphisms.

noncomputable def Module.End.mapValueRingHom {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) : End A (TensorProduct R A M) →+* End B (TensorProduct R B M)

Base change of endomorphisms of a scalar extension, as a ring homomorphism.

Equations

• Module.End.mapValueRingHom f = { toFun := Module.End.mapValue f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Module.End.mapValueRingHom_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) (φ : End A (TensorProduct R A M)) : (mapValueRingHom f) φ = mapValue f φ

The bundled base-change homomorphism acts by mapValue.

@[simp]

theorem Module.End.mapValue_aeval {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) (φ : End A (TensorProduct R A M)) (p : Polynomial A) : mapValue f ((Polynomial.aeval φ) p) = (Polynomial.aeval (mapValue f φ)) (Polynomial.map f.toRingHom p)

Evaluating a polynomial at an endomorphism and then extending scalars is the same as mapping the polynomial coefficients and evaluating at the extended endomorphism.

noncomputable def Module.End.mapValueGL {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) : LinearMap.GeneralLinearGroup A (TensorProduct R A M) →* LinearMap.GeneralLinearGroup B (TensorProduct R B M)

Base change of automorphisms of a scalar extension, as a group homomorphism.

Equations

• Module.End.mapValueGL f = Units.map ↑(Module.End.mapValueRingHom f)

@[simp]

theorem Module.End.mapValueGL_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) (φ : LinearMap.GeneralLinearGroup A (TensorProduct R A M)) : ↑((mapValueGL f) φ) = mapValue f ↑φ

The underlying endomorphism of a base-changed automorphism is the base-changed endomorphism.

@[simp]

theorem Module.End.mapValue_id {R : Type u_1} {A : Type u_2} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (φ : End A (TensorProduct R A M)) : mapValue (AlgHom.id R A) φ = φ

Base change along the identity morphism of value algebras is the identity.

@[simp]

theorem Module.End.mapValue_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {M : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [CommSemiring C] [Algebra R C] [AddCommMonoid M] [Module R M] (f : A →ₐ[R] B) (g : B →ₐ[R] C) (φ : End A (TensorProduct R A M)) : mapValue (g.comp f) φ = mapValue g (mapValue f φ)

Base change along a composite of morphisms of value algebras is the composite of base changes.

theorem Module.End.baseChange_comp_mapValue {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} {N : Type u_6} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : A →ₐ[R] B) (u : M →ₗ[R] N) (φ : End A (TensorProduct R A M)) (ψ : End A (TensorProduct R A N)) (h : LinearMap.baseChange A u ∘ₗ φ = ψ ∘ₗ LinearMap.baseChange A u) : LinearMap.baseChange B u ∘ₗ mapValue f φ = mapValue f ψ ∘ₗ LinearMap.baseChange B u

Base change preserves naturality in the module: a square over A transports to the corresponding square over B.

theorem Module.End.distribBaseChange_comp_mapValue {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_5} {N : Type u_6} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : A →ₐ[R] B) (φ : End A (TensorProduct R A M)) (ψ : End A (TensorProduct R A N)) (χ : End A (TensorProduct R A (TensorProduct R M N))) (h : ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A M N).symm ∘ₗ TensorProduct.map φ ψ = χ ∘ₗ ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A M N).symm) : ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R B M N).symm ∘ₗ TensorProduct.map (mapValue f φ) (mapValue f ψ) = mapValue f χ ∘ₗ ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R B M N).symm

Base change preserves the tensor comparison: a tensor-compatibility square over A transports to the corresponding square over B.