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