Interaction between quotients and tensor products for algebras

This file proves algebra analogs of the isomorphisms in Mathlib/LinearAlgebra/TensorProduct/Quotient.lean.

Main results

• Algebra.TensorProduct.quotIdealMapEquivTensorQuot: B ⧸ (I.map <| algebraMap A B) ≃ₐ[B] B ⊗[A] (A ⧸ I)

noncomputable def Algebra.TensorProduct.quotIdealMapEquivTensorQuotAux {A : Type u_1} (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (I : Ideal A) : (B ⧸ Ideal.map (algebraMap A B) I) ≃ₗ[B] TensorProduct A B (A ⧸ I)

(Implementation): Use Algebra.TensorProduct.quotIdealMapEquivTensorQuot instead.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebra.TensorProduct.quotIdealMapEquivTensorQuot {A : Type u_1} (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (I : Ideal A) : (B ⧸ Ideal.map (algebraMap A B) I) ≃ₐ[B] TensorProduct A B (A ⧸ I)

B ⊗[A] (A ⧸ I) is isomorphic as a B-algebra to B ⧸ I B.

Equations

• Algebra.TensorProduct.quotIdealMapEquivTensorQuot B I = AlgEquiv.ofLinearEquiv (Algebra.TensorProduct.quotIdealMapEquivTensorQuotAux B I) ⋯ ⋯

@[simp]

theorem Algebra.TensorProduct.quotIdealMapEquivTensorQuot_mk {A : Type u_1} (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (I : Ideal A) (b : B) : (quotIdealMapEquivTensorQuot B I) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) b) = b ⊗ₜ[A] 1

@[simp]

theorem Algebra.TensorProduct.quotIdealMapEquivTensorQuot_symm_tmul {A : Type u_1} (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (I : Ideal A) (b : B) (a : A) : (quotIdealMapEquivTensorQuot B I).symm (b ⊗ₜ[A] (Ideal.Quotient.mk I) a) = Submodule.Quotient.mk (a • b)

noncomputable def Algebra.TensorProduct.quotIdealMapEquivQuotTensor {A : Type u_1} (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (I : Ideal A) : (B ⧸ Ideal.map (algebraMap A B) I) ≃ₐ[A ⧸ I] TensorProduct A (A ⧸ I) B

(A ⧸ I) ⊗[A] B is isomorphic as an A ⧸ I-algebra to B ⧸ I B.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebra.TensorProduct.quotIdealMapEquivQuotTensor_mk {A : Type u_1} (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (I : Ideal A) (b : B) : (quotIdealMapEquivQuotTensor B I) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) b) = 1 ⊗ₜ[A] b

noncomputable def Algebra.TensorProduct.tensorQuotientEquiv {R : Type u_1} (S : Type u_2) (T : Type u_3) (A : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (I : Ideal T) : TensorProduct R A (T ⧸ I) ≃ₐ[S] TensorProduct R A T ⧸ Ideal.map includeRight I

The tensor product of an S-algebra A over R with the quotient of T by an ideal I is isomorphic (as an S-algebra) to the quotient of A ⊗[R] T by the extended ideal.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebra.TensorProduct.tensorQuotientEquiv_apply_tmul {R : Type u_1} (S : Type u_2) (T : Type u_3) (A : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (I : Ideal T) (a : A) (t : T) : (tensorQuotientEquiv S T A I) (a ⊗ₜ[R] (Ideal.Quotient.mk I) t) = (Ideal.Quotient.mk (Ideal.map includeRight I)) (a ⊗ₜ[R] t)

@[simp]

theorem Algebra.TensorProduct.tensorQuotientEquiv_symm_apply_tmul {R : Type u_1} (S : Type u_2) (T : Type u_3) (A : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (I : Ideal T) (a : A) (t : T) : (tensorQuotientEquiv S T A I).symm ((Ideal.Quotient.mk (Ideal.map includeRight I)) (a ⊗ₜ[R] t)) = a ⊗ₜ[R] (Ideal.Quotient.mk I) t

noncomputable def Algebra.TensorProduct.quotientTensorEquiv {R : Type u_1} (S : Type u_2) (T : Type u_3) (A : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (I : Ideal A) : TensorProduct R (A ⧸ I) T ≃ₐ[S] TensorProduct R A T ⧸ Ideal.map (algebraMap A (TensorProduct R A T)) I

The tensor product over R of the quotient of an S-algebra A by an ideal I with T is isomorphic (as an S-algebra) to the quotient of A ⊗[R] T by the extended ideal.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebra.TensorProduct.quotientTensorEquiv_apply_tmul {R : Type u_1} (S : Type u_2) (T : Type u_3) (A : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (I : Ideal A) (a : A) (t : T) : (quotientTensorEquiv S T A I) ((Ideal.Quotient.mk I) a ⊗ₜ[R] t) = (Ideal.Quotient.mk (Ideal.map (algebraMap A (TensorProduct R A T)) I)) (a ⊗ₜ[R] t)

@[simp]

theorem Algebra.TensorProduct.quotientTensorEquiv_symm_apply_tmul {R : Type u_1} (S : Type u_2) (T : Type u_3) (A : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (I : Ideal A) (a : A) (t : T) : (quotientTensorEquiv S T A I).symm ((Ideal.Quotient.mk (Ideal.map (algebraMap A (TensorProduct R A T)) I)) (a ⊗ₜ[R] t)) = (Ideal.Quotient.mk I) a ⊗ₜ[R] t

theorem Ideal.subtype_rTensor_range {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (I : Ideal R) : (↑(TensorProduct.lid R M) ∘ₗ LinearMap.rTensor M (Submodule.subtype I)).range = I • ⊤

theorem Ideal.Quotient.algHom_ext_iff {R₁ : Type u_1} {A : Type u_3} [CommSemiring R₁] [Ring A] [Algebra R₁ A] {I : Ideal A} [I.IsTwoSided] {S : Type u_5} [Semiring S] [Algebra R₁ S] {f g : A ⧸ I →ₐ[R₁] S} : f = g ↔ f.comp (mkₐ R₁ I) = g.comp (mkₐ R₁ I)

noncomputable def Algebra.tensorQuotientTensorEquiv {R : Type u_1} {R' : Type u_2} (R'' : Type u_3) {S : Type u_4} [CommRing R] [CommRing R'] [CommRing R''] [CommRing S] [Algebra R R'] [Algebra R R''] [Algebra R' R''] [IsScalarTower R R' R''] [Algebra R S] (e : TensorProduct R R' S) : TensorProduct R' R'' (TensorProduct R R' S ⧸ Ideal.span {e}) ≃ₐ[R''] TensorProduct R R'' S ⧸ Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}

Let e be an element of R' ⊗[R] S. Then R'' ⊗[R'] ((R' ⊗[R] S) / e) is isomorphic to (R'' ⊗[R] S) / e as R''-algebras.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebra.tensorQuotientTensorEquiv_tmul {R : Type u_1} {R' : Type u_2} {R'' : Type u_3} {S : Type u_4} [CommRing R] [CommRing R'] [CommRing R''] [CommRing S] [Algebra R R'] [Algebra R R''] [Algebra R' R''] [IsScalarTower R R' R''] [Algebra R S] (e : TensorProduct R R' S) (a : R'') (b : R') (c : S) : (tensorQuotientTensorEquiv R'' e) (a ⊗ₜ[R'] (Ideal.Quotient.mk (Ideal.span {e})) (b ⊗ₜ[R] c)) = (Ideal.Quotient.mk (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e})) ((a * (algebraMap R' R'') b) ⊗ₜ[R] c)

@[simp]

theorem Algebra.tensorQuotientTensorEquiv_symm_tmul {R : Type u_1} {R' : Type u_2} {R'' : Type u_3} {S : Type u_4} [CommRing R] [CommRing R'] [CommRing R''] [CommRing S] [Algebra R R'] [Algebra R R''] [Algebra R' R''] [IsScalarTower R R' R''] [Algebra R S] (e : TensorProduct R R' S) (a : R'') (b : S) : (tensorQuotientTensorEquiv R'' e).symm ((Ideal.Quotient.mk (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e})) (a ⊗ₜ[R] b)) = a ⊗ₜ[R'] (Ideal.Quotient.mk (Ideal.span {e})) (1 ⊗ₜ[R] b)