Linear maps over a localization tensored with an algebra

Let K be a localization of R and let A be an R-algebra. Mathlib's IsLocalization.linearMap_compatibleSMul says that an R-linear map between K-modules is automatically K-linear. This file records the analogue for the ring K ⊗[R] A: on modules where q ⊗ₜ a acts as q • a • _, every A-linear map is K ⊗[R] A-linear.

The ordinary-localization base-change isomorphism also agrees with the localized coefficient inclusion on every localized element.

Main results

• TauCeti.IsLocalization.linearMap_compatibleSMul_tensorProduct: A-linear maps between such modules commute with the action of K ⊗[R] A.

theorem TauCeti.IsLocalization.linearMap_compatibleSMul_tensorProduct {R : Type u_1} [CommSemiring R] (S : Submonoid R) (K : Type u_2) [CommSemiring K] [Algebra R K] [IsLocalization S K] {A : Type u_3} [Semiring A] [Algebra R A] {V : Type u_4} {W : Type u_5} [AddCommMonoid V] [Module R V] [Module K V] [Module A V] [Module (TensorProduct R K A) V] [IsScalarTower R K V] [IsScalarTower R A V] [AddCommMonoid W] [Module R W] [Module K W] [Module A W] [Module (TensorProduct R K A) W] [IsScalarTower R K W] [IsScalarTower R A W] (hV : ∀ (q : K) (a : A) (v : V), q ⊗ₜ[R] a • v = q • a • v) (hW : ∀ (q : K) (a : A) (w : W), q ⊗ₜ[R] a • w = q • a • w) : LinearMap.CompatibleSMul V W (TensorProduct R K A) A

Let K be a localization of R and A an R-algebra. Between modules on which q ⊗ₜ a ∈ K ⊗[R] A acts as q • a • _, an A-linear map is K ⊗[R] A-linear: it is K-linear because K is a localization of R (IsLocalization.linearMap_compatibleSMul).

@[simp]

theorem IsLocalization.Away.tensorProductEquivTMulRight_one_tmul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Type u_3) [CommSemiring S] [Algebra R S] (f : A) (B : Type u_4) [CommSemiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Away f B] (z : B) : (tensorProductEquivTMulRight R S f B) (1 ⊗ₜ[R] z) = (map B (Localization.Away (Algebra.TensorProduct.includeRight.toRingHom f)) Algebra.TensorProduct.includeRight.toRingHom f) z

Ordinary-localization base change extends an arbitrary localized element by the localized coefficient inclusion.