Interaction between quotients and tensor products for algebras

This files proves algebra analogs of the isomorphisms in Mathlib.LinearAlgebra.TensorProduct.Quotient.

Main results

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

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 an A-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)