Documentation

Mathlib.RingTheory.TensorProduct.Quotient

Interaction between quotients and tensor products for algebras #

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

Main results #

source
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
Instances For
    source
    @[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
    source
    @[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)
    source
    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 to the quotient of A ⊗[R] T by the extended ideal, as an S-algebra.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[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)
      source
      @[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