Extended ideals and annihilators under scalar extension

The scalar multiplication equivalence S ⊗[R] R ≃ₗ[S] S identifies the base change of an ideal with its extension along algebraMap R S. This permits kernel computations on tensor products to be read as membership statements in extended ideals. The extension of a module annihilator is contained in its annihilator after arbitrary scalar extension, without a flatness hypothesis. The coefficient algebra S need not be commutative; extended ideals are left ideals.

For an ideal I and a module M, injectivity of I ⊗ M → R ⊗ M is the vanishing of Tor₁(R ⧸ I, M). Ideal.sup_subtype_rTensor_injective propagates it from I and J to I ⊔ J, provided I M ∩ J M = (I ⊓ J) M. For an M-regular element x it holds for the ideal (x) (IsSMulRegular.span_singleton_subtype_rTensor_injective).

Along a flat ring map R → S the base change S ⊗[R] I is the extended ideal I S, so the fibres of I and I S at a field-valued point of S have the same dimension (Ideal.finrank_tensor_map_of_flat). Without flatness, over a commutative S, the map S ⊗[R] I → I S is still surjective (Ideal.liftBaseChange_idealMap_surjective) and its kernel is killed by I S (Ideal.isTorsionBySet_ker_liftBaseChange_idealMap). For an S-module M which is flat over R, it follows that I S ⊗[S] M → M is injective, that is Tor₁ˢ(S ⧸ I S, M) = 0 (Module.Flat.map_subtype_rTensor_injective). For an idempotent ideal I, I S • (S ⊗[R] I) = S ⊗[R] I (Ideal.smul_top_baseChange_eq_top), and it follows that S ⊗[R] (I ⊗[R] I) ≅ I S ⊗[S] I S (Ideal.baseChangeTensorSelfEquiv), which is how basic setups of almost mathematics base change (Gabber–Ramero, Almost ring theory, Remark 2.1.4(ii)).

For an ideal J of S with R → S ⧸ J surjective, every element of S ⊗[R] M is 1 ⊗ m modulo J (S ⊗[R] M) (TensorProduct.exists_sub_one_tmul_mem_smul_top). For an ideal J of R, m ∈ J M gives 1 ⊗ m ∈ (J S) (S ⊗[R] M) (TensorProduct.one_tmul_mem_map_smul_top).

theorem Ideal.map_eq_baseChange_map_rid {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] (I : Ideal R) : map (algebraMap R S) I = Submodule.map (↑(TensorProduct.AlgebraTensorModule.rid R S S)) (Submodule.baseChange S I)

The extended ideal is the image of its tensor base change under scalar multiplication.

theorem LinearMap.mem_map_ker_iff_of_flat {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommRing R] [Ring S] [Algebra R S] [AddCommGroup M] [Module R M] [Module.Flat R S] (f : R →ₗ[R] M) (s : S) : s ∈ Ideal.map (algebraMap R S) f.ker ↔ (baseChange S f) (s ⊗ₜ[R] 1) = 0

Flatness tests membership in an extended scalar-source kernel on s ⊗ₜ 1.

theorem TauCeti.annihilator_map_le_baseChange {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] : Ideal.map (algebraMap R S) (Module.annihilator R M) ≤ Module.annihilator S (TensorProduct R S M)

Extension of the annihilator is contained in the annihilator after arbitrary base change.

theorem Ideal.sup_subtype_rTensor_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I J : Ideal R} (hI : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))) (hJ : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype J))) (hIJ : I • ⊤ ⊓ J • ⊤ ≤ (I ⊓ J) • ⊤) : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (I ⊔ J)))

If I ⊗ M → R ⊗ M and J ⊗ M → R ⊗ M are injective, that is, if Tor₁(R ⧸ I, M) = Tor₁(R ⧸ J, M) = 0, and I M ∩ J M = (I ⊓ J) M, then (I ⊔ J) ⊗ M → R ⊗ M is injective as well.

theorem IsSMulRegular.span_singleton_subtype_rTensor_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : R} (reg : IsSMulRegular M x) : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (Ideal.span {x})))

If x is M-regular, then Tor₁ᴿ(R ⧸ (x), M) = 0: the map (x) ⊗[R] M → M is injective.

theorem Ideal.finrank_tensor_map_of_flat {R : Type u_1} {S : Type u_2} {F : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Field F] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Module.Flat R S] (I : Ideal R) : Module.finrank F (TensorProduct S F ↥(map (algebraMap R S) I)) = Module.finrank F (TensorProduct R F ↥I)

Along a flat ring map R → S, the fibre of the extended ideal I S at a field-valued point S → F has the same dimension as the fibre of I: by flatness, S ⊗[R] I is I S. The identification S ⊗[R] I ≃ I S follows the construction in the proof of Mathlib's Ideal.FG.of_FG_map_of_faithfullyFlat.

theorem Ideal.liftBaseChange_idealMap_surjective {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (I : Ideal R) : Function.Surjective ⇑(LinearMap.liftBaseChange S (Algebra.idealMap S I))

The map S ⊗[R] I → I S induced by I → I S is surjective.

theorem Ideal.isTorsionBySet_ker_liftBaseChange_idealMap {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (I : Ideal R) : Module.IsTorsionBySet S ↥(LinearMap.liftBaseChange S (Algebra.idealMap S I)).ker ↑(map (algebraMap R S) I)

The kernel of the surjection S ⊗[R] I → I S is killed by the extended ideal I S.

theorem Ideal.smul_top_baseChange_eq_top {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] {I : Ideal R} (hI : IsIdempotentElem I) : map (algebraMap R S) I • ⊤ = ⊤

For an idempotent ideal I, I S • (S ⊗[R] I) = S ⊗[R] I.

theorem Module.Flat.map_subtype_rTensor_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {S : Type u_3} [CommRing S] [Algebra R S] [Module S M] [IsScalarTower R S M] [Flat R M] (J : Ideal R) : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (Ideal.map (algebraMap R S) J)))

If an S-module M is flat over R, then Tor₁ˢ(S ⧸ J S, M) = 0 for every ideal J of R: the map J S ⊗[S] M → M is injective.

noncomputable def Ideal.baseChangeTensorSelfEquiv {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] {I : Ideal R} (hI : IsIdempotentElem I) : TensorProduct R S (TensorProduct R ↥I ↥I) ≃ₗ[S] TensorProduct S ↥(map (algebraMap R S) I) ↥(map (algebraMap R S) I)

For an idempotent ideal I, the base change of I ⊗[R] I is the tensor square of the extended ideal: S ⊗[R] (I ⊗[R] I) ≅ I S ⊗[S] I S (Gabber–Ramero Remark 2.1.4(ii)).

@[simp]

theorem Ideal.baseChangeTensorSelfEquiv_tmul {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] {I : Ideal R} (hI : IsIdempotentElem I) (s : S) (a b : ↥I) : (baseChangeTensorSelfEquiv S hI) (s ⊗ₜ[R] (a ⊗ₜ[R] b)) = s • (Algebra.idealMap S I) a ⊗ₜ[S] (Algebra.idealMap S I) b

theorem TensorProduct.exists_sub_one_tmul_mem_smul_top {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [Module R M] {J : Ideal S} (hJ : Function.Surjective ⇑((Ideal.Quotient.mk J).comp (algebraMap R S))) (x : TensorProduct R S M) : ∃ (m : M), x - 1 ⊗ₜ[R] m ∈ J • ⊤

If R → S ⧸ J is surjective, then every element of S ⊗[R] M is of the form 1 ⊗ m modulo J (S ⊗[R] M).

theorem TensorProduct.one_tmul_mem_map_smul_top {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [Module R M] {J : Ideal R} {m : M} (hm : m ∈ J • ⊤) : 1 ⊗ₜ[R] m ∈ Ideal.map (algebraMap R S) J • ⊤

If m ∈ J M for an ideal J of R, then 1 ⊗ m ∈ (J S) (S ⊗[R] M).