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.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.
Instances For
    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 a B-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.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.
      Instances For
        source
        @[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
        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 (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.
        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
          source
          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.
          Instances For
            source
            @[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)
            source
            @[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
            source
            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 • ⊤