Documentation

TauCeti.RingTheory.TensorProduct.IsBaseChange

Base change of a tensor product, and injectivity of base-change maps #

If f : M →ₗ[R] N and g : M' →ₗ[R] N' exhibit the S-modules N and N' as base changes of M and M' along R → S, then m ⊗ m' ↦ f m ⊗ g m' exhibits N ⊗[S] N' as the base change of M ⊗[R] M'. On the concrete models this is Mathlib's TensorProduct.AlgebraTensorModule.distribBaseChange, S ⊗[R] (M ⊗[R] M') ≃ (S ⊗[R] M) ⊗[S] (S ⊗[R] M'); the statement here is its form for the abstract IsBaseChange interface, alongside Mathlib's IsBaseChange.prodMap for products. Mathlib's isBaseChange_tensorProduct_map is the analogous statement when only one factor is base changed and the tensor product stays over the base ring.

If f : M →ₗ[R] N exhibits N as the base change of M along R → S, then the S-linear map S ⊗[R] M →ₗ[S] N it induces, Mathlib's LinearMap.liftBaseChange, is bijective: it is the equivalence IsBaseChange.equiv. Conversely, this bijectivity characterizes base changes. A linear map between two base changes of M that is compatible with the base-change maps is bijective. The original map f is also injective whenever the scalar-unit map m ↦ 1 ⊗ m is injective.

Base change of linear maps is compatible with the induced maps S ⊗[R] M →ₗ[S] N: a commutative square of R-linear maps gives a commutative square of the induced S-linear maps. The map induced on a finite product is injective as soon as each factor induces an injective map.

For any localization, extension also preserves injectivity of a linear map into a module over the localized semiring, without requiring its image to span the target.

The image of a base change map spans its target over the extended scalars.

Main results #

source
theorem IsBaseChange.tensorProduct {R : Type u_1} {S : Type u_2} {M : Type u_3} {M' : Type u_4} {N : Type u_5} {N' : Type u_6} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] [AddCommMonoid N'] [Module R N'] [Module S N'] [IsScalarTower R S N'] {f : M →ₗ[R] N} {g : M' →ₗ[R] N'} (hf : IsBaseChange S f) (hg : IsBaseChange S g) :
IsBaseChange S (TensorProduct.mapOfCompatibleSMul S R R N N' ∘ₗ TensorProduct.map f g)

Base change commutes with tensor products. If f and g exhibit N and N' as base changes of M and M' along R → S, then m ⊗ m' ↦ f m ⊗ g m' exhibits N ⊗[S] N' as the base change of M ⊗[R] M'.

source
theorem IsBaseChange.liftBaseChange_bijective {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (hf : IsBaseChange S f) :
Function.Bijective ⇑(LinearMap.liftBaseChange S f)

If f exhibits N as the base change of M along R → S, then the induced S-linear map f.liftBaseChange S : S ⊗[R] M →ₗ[S] N is bijective, since it is the equivalence hf.equiv.

source
theorem IsBaseChange.iff_liftBaseChange_bijective {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} :
IsBaseChange S f ↔ Function.Bijective ⇑(LinearMap.liftBaseChange S f)

A linear map f exhibits N as the base change of M along R → S exactly when the induced S-linear map f.liftBaseChange S : S ⊗[R] M →ₗ[S] N is bijective.

source
theorem IsBaseChange.bijective_of_comp_eq {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_5} {N' : Type u_6} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] [AddCommMonoid N'] [Module R N'] [Module S N'] [IsScalarTower R S N'] {f : M →ₗ[R] N} (hf : IsBaseChange S f) {g : M →ₗ[R] N'} (hg : IsBaseChange S g) (φ : N →ₗ[S] N') (h : ∀ (m : M), φ (f m) = g m) :
Function.Bijective ⇑φ

Comparison of two base changes. If f : M →ₗ[R] N and g : M →ₗ[R] N' both exhibit base changes of M along R → S, then every S-linear map φ : N →ₗ[S] N' with φ ∘ f = g is bijective: it is the composite hg.equiv ∘ hf.equiv.symm of the two base-change equivalences.

source
theorem IsBaseChange.liftBaseChange_injective {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (hf : IsBaseChange S f) :
Function.Injective ⇑(LinearMap.liftBaseChange S f)

If f exhibits N as the base change of M along R → S, then the induced S-linear map f.liftBaseChange S : S ⊗[R] M →ₗ[S] N is injective, since it is the equivalence hf.equiv.

source
theorem IsBaseChange.injective_of_tensorProduct_mk_injective {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (hf : IsBaseChange S f) (hinj : Function.Injective ⇑((TensorProduct.mk R S M) 1)) :
Function.Injective ⇑f

A base-change map is injective whenever the scalar-unit map m ↦ 1 ⊗ m is injective, since the original map factors through this map and the base-change equivalence.

source
theorem LinearMap.liftBaseChange_comp_baseChange {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] {M₁ : Type u_7} {M₂ : Type u_8} {N₁ : Type u_9} {N₂ : Type u_10} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] [Module S N₁] [Module S N₂] [IsScalarTower R S N₁] [IsScalarTower R S N₂] {h₁ : M₁ →ₗ[R] N₁} {h₂ : M₂ →ₗ[R] N₂} {f : M₁ →ₗ[R] M₂} {f' : N₁ →ₗ[S] N₂} (comm : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁) :
liftBaseChange S h₂ ∘ₗ baseChange S f = f' ∘ₗ liftBaseChange S h₁

The base change of f followed by the map induced by h₂ is the map induced by h₁ followed by f', whenever h₂ ∘ f = f' ∘ h₁.

source
theorem LinearMap.liftBaseChange_pi_injective {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] {ι : Type u_11} [Finite ι] {M : ι → Type u_12} {N : ι → Type u_13} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (M i)] [(i : ι) → Module R (N i)] [(i : ι) → Module S (N i)] [∀ (i : ι), IsScalarTower R S (N i)] (f : (i : ι) → M i →ₗ[R] N i) (hf : ∀ (i : ι), Function.Injective ⇑(liftBaseChange S (f i))) :
Function.Injective ⇑(liftBaseChange S (pi fun (i : ι) => f i ∘ₗ proj i))

The map S ⊗[R] (∀ i, M i) → ∀ i, N i induced by a finite product of maps f i : M i → N i is injective if each S ⊗[R] M i → N i is.

source
theorem LinearMap.liftBaseChange_injective {R : Type u_7} {K : Type u_8} {M : Type u_9} {V : Type u_10} [CommSemiring R] [CommSemiring K] [Algebra R K] [AddCommMonoid M] [Module R M] [AddCommMonoid V] [Module R V] [Module K V] [IsScalarTower R K V] (f : M →ₗ[R] V) (S : Submonoid R) [IsLocalization S K] (hf : Function.Injective ⇑f) :
Function.Injective ⇑(liftBaseChange K f)

For a localization K = S⁻¹R, extension of an injective R-linear map into a K-module remains injective. Neither freeness, finite generation nor a full-span hypothesis is needed.

source
theorem IsBaseChange.span_range_eq_top {R : Type u_7} {R' : Type u_8} {M : Type u_9} {M' : Type u_10} [CommSemiring R] [CommSemiring R'] [Algebra R R'] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] [Module R' M'] [IsScalarTower R R' M'] {f : M →ₗ[R] M'} (hf : IsBaseChange R' f) :
Submodule.span R' (Set.range ⇑f) = ⊤

The image of a base change map f : M →ₗ[R] M' spans M' over the extended scalars R'.