Ideals in tensor products of algebras

For an ideal I of an R-algebra A and an R-algebra B, I.leftTensorIdeal R B is the ideal of A ⊗[R] B generated by the image of I under includeLeft. For an ideal J of B, J.rightTensorIdeal R A is generated by its image under includeRight. They represent the images of I ⊗[R] B and A ⊗[R] J.

The constructions preserve joins and arbitrary suprema and commute with tensor-product maps. Over a commutative ring, tensoring a quotient map has the corresponding tensor ideal as its kernel; tensoring two surjective algebra maps has the sum of the two tensor ideals as its kernel. Quotients of a noncommutative algebra require a two-sided ideal.

The kernel formulas use Mathlib's tensor-product right-exactness theorems.

def Ideal.leftTensorIdeal (R : Type u) {A : Type v} (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (I : Ideal A) : Ideal (TensorProduct R A B)

The ideal of A ⊗[R] B generated by the left inclusion of I, representing I ⊗ B.

theorem Ideal.leftTensorIdeal_def (R : Type u) {A : Type v} (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (I : Ideal A) : leftTensorIdeal R B I = map Algebra.TensorProduct.includeLeft.toRingHom I

I.leftTensorIdeal R B is the ideal map of I along the left tensor inclusion.

theorem Ideal.includeLeft_mem_leftTensorIdeal (R : Type u) {A : Type v} (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {I : Ideal A} {x : A} (hx : x ∈ I) : Algebra.TensorProduct.includeLeft x ∈ leftTensorIdeal R B I

The left tensor inclusion sends elements of I into I ⊗ B.

theorem Ideal.tmul_mem_leftTensorIdeal (R : Type u) {A : Type v} (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {I : Ideal A} {x : A} (hx : x ∈ I) (y : B) : x ⊗ₜ[R] y ∈ leftTensorIdeal R B I

A pure tensor x ⊗ₜ y with x ∈ I lies in I ⊗ B.

theorem Ideal.mem_leftTensorIdeal_iff (R : Type u) {A : Type v} (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {I : Ideal A} {x : TensorProduct R A B} : x ∈ leftTensorIdeal R B I ↔ x ∈ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype).range

Membership in I ⊗ B is membership in the range of tensoring the subtype of I on the right.

theorem Ideal.leftTensorIdeal_le_iff (R : Type u) {A : Type v} (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {I : Ideal A} {J : Ideal (TensorProduct R A B)} : leftTensorIdeal R B I ≤ J ↔ I ≤ comap Algebra.TensorProduct.includeLeft.toRingHom J

The order universal property for I ⊗ B.

theorem Ideal.leftTensorIdeal_mono (R : Type u) {A : Type v} (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {I J : Ideal A} (hIJ : I ≤ J) : leftTensorIdeal R B I ≤ leftTensorIdeal R B J

The construction I ↦ I ⊗ B is monotone.

@[simp]

theorem Ideal.leftTensorIdeal_iSup (R : Type u) {A : Type v} (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {ι : Sort u_1} (I : ι → Ideal A) : leftTensorIdeal R B (⨆ (i : ι), I i) = ⨆ (i : ι), leftTensorIdeal R B (I i)

The construction I ↦ I ⊗ B distributes over arbitrary suprema of ideals.

@[simp]

theorem Ideal.leftTensorIdeal_sup (R : Type u) {A : Type v} (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (I J : Ideal A) : leftTensorIdeal R B (I ⊔ J) = leftTensorIdeal R B I ⊔ leftTensorIdeal R B J

The construction I ↦ I ⊗ B distributes over joins of ideals.

def Ideal.rightTensorIdeal (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (I : Ideal B) : Ideal (TensorProduct R A B)

The ideal of A ⊗[R] B generated by the right inclusion of I, representing A ⊗ I.

theorem Ideal.rightTensorIdeal_def (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (I : Ideal B) : rightTensorIdeal R A I = map Algebra.TensorProduct.includeRight.toRingHom I

I.rightTensorIdeal R A is the ideal map of I along the right tensor inclusion.

theorem Ideal.includeRight_mem_rightTensorIdeal (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {I : Ideal B} {x : B} (hx : x ∈ I) : Algebra.TensorProduct.includeRight x ∈ rightTensorIdeal R A I

The right tensor inclusion sends elements of I into A ⊗ I.

theorem Ideal.tmul_mem_rightTensorIdeal (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {I : Ideal B} (x : A) {y : B} (hy : y ∈ I) : x ⊗ₜ[R] y ∈ rightTensorIdeal R A I

A pure tensor x ⊗ₜ y with y ∈ I lies in A ⊗ I.

theorem Ideal.mem_rightTensorIdeal_iff (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {I : Ideal B} {x : TensorProduct R A B} : x ∈ rightTensorIdeal R A I ↔ x ∈ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype).range

Membership in A ⊗ I is membership in the range of tensoring the subtype of I on the left.

theorem Ideal.rightTensorIdeal_le_iff (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {I : Ideal B} {J : Ideal (TensorProduct R A B)} : rightTensorIdeal R A I ≤ J ↔ I ≤ comap Algebra.TensorProduct.includeRight.toRingHom J

The order universal property for A ⊗ I.

theorem Ideal.rightTensorIdeal_mono (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {I J : Ideal B} (hIJ : I ≤ J) : rightTensorIdeal R A I ≤ rightTensorIdeal R A J

The construction I ↦ A ⊗ I is monotone.

@[simp]

theorem Ideal.rightTensorIdeal_iSup (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {ι : Sort u_1} (I : ι → Ideal B) : rightTensorIdeal R A (⨆ (i : ι), I i) = ⨆ (i : ι), rightTensorIdeal R A (I i)

The construction I ↦ A ⊗ I distributes over arbitrary suprema of ideals.

@[simp]

theorem Ideal.rightTensorIdeal_sup (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (I J : Ideal B) : rightTensorIdeal R A (I ⊔ J) = rightTensorIdeal R A I ⊔ rightTensorIdeal R A J

The construction I ↦ A ⊗ I distributes over joins of ideals.

theorem Ideal.ker_tensorProduct_map_id_quotient {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (I : Ideal B) [I.IsTwoSided] : RingHom.ker (Algebra.TensorProduct.map (AlgHom.id R A) (Quotient.mkₐ R I)) = rightTensorIdeal R A I

The kernel of tensoring the quotient map on the right is the right tensor ideal.

theorem Ideal.ker_tensorProduct_map_quotient_id {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (I : Ideal A) [I.IsTwoSided] : RingHom.ker (Algebra.TensorProduct.map (Quotient.mkₐ R I) (AlgHom.id R B)) = leftTensorIdeal R B I

The kernel of tensoring the quotient map on the left is the left tensor ideal.

@[simp]

theorem AlgHom.map_tensor_leftTensorIdeal {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Semiring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] (f : A →ₐ[R] C) (g : B →ₐ[R] D) (I : Ideal A) : Ideal.map (↑(Algebra.TensorProduct.map f g)) (Ideal.leftTensorIdeal R B I) = Ideal.leftTensorIdeal R D (Ideal.map f.toRingHom I)

A tensor-product map carries the left tensor ideal generated by I onto the left tensor ideal generated by its image in the left codomain factor.

@[simp]

theorem AlgHom.map_tensor_rightTensorIdeal {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Semiring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] (f : A →ₐ[R] C) (g : B →ₐ[R] D) (I : Ideal B) : Ideal.map (↑(Algebra.TensorProduct.map f g)) (Ideal.rightTensorIdeal R A I) = Ideal.rightTensorIdeal R C (Ideal.map g.toRingHom I)

A tensor-product map carries the right tensor ideal generated by I onto the right tensor ideal generated by its image in the right codomain factor.

theorem AlgHom.ker_tensorProduct_map_eq_leftTensorIdeal_sup_rightTensorIdeal {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommRing R] [Ring A] [Ring B] [Ring C] [Ring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] (f : A →ₐ[R] C) (g : B →ₐ[R] D) (hf : Function.Surjective ⇑f) (hg : Function.Surjective ⇑g) : RingHom.ker (Algebra.TensorProduct.map f g) = Ideal.leftTensorIdeal R B (RingHom.ker f) ⊔ Ideal.rightTensorIdeal R A (RingHom.ker g)

The kernel of a tensor product of two surjective algebra maps is the sum of the tensor ideals generated by their kernels.