Documentation

Mathlib.RingTheory.IsTensorProduct

The characteristic predicate of tensor product #

Main definitions #

Main results #

def IsTensorProduct {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] (f : M₁ →ₗ[R] M₂ →ₗ[R] M) :

Given a bilinear map f : M₁ →ₗ[R] M₂ →ₗ[R] M, IsTensorProduct f means that M is the tensor product of M₁ and M₂ via f. This is defined by requiring the lift M₁ ⊗[R] M₂ → M to be bijective.

Equations
Instances For
    @[simp]
    theorem IsTensorProduct.equiv_apply {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) :
    ∀ (a : TensorProduct R M₁ M₂), h.equiv a = (TensorProduct.lift f) a
    noncomputable def IsTensorProduct.equiv {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) :
    TensorProduct R M₁ M₂ ≃ₗ[R] M

    If M is the tensor product of M₁ and M₂, it is linearly equivalent to M₁ ⊗[R] M₂.

    Equations
    Instances For
      @[simp]
      theorem IsTensorProduct.equiv_toLinearMap {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) :
      h.equiv = TensorProduct.lift f
      @[simp]
      theorem IsTensorProduct.equiv_symm_apply {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) (x₁ : M₁) (x₂ : M₂) :
      h.equiv.symm ((f x₁) x₂) = x₁ ⊗ₜ[R] x₂
      noncomputable def IsTensorProduct.lift {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} {M' : Type u_5} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [AddCommMonoid M'] [Module R M₁] [Module R M₂] [Module R M] [Module R M'] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) (f' : M₁ →ₗ[R] M₂ →ₗ[R] M') :
      M →ₗ[R] M'

      If M is the tensor product of M₁ and M₂, we may lift a bilinear map M₁ →ₗ[R] M₂ →ₗ[R] M' to a M →ₗ[R] M'.

      Equations
      Instances For
        theorem IsTensorProduct.lift_eq {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} {M' : Type u_5} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [AddCommMonoid M'] [Module R M₁] [Module R M₂] [Module R M] [Module R M'] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) (f' : M₁ →ₗ[R] M₂ →ₗ[R] M') (x₁ : M₁) (x₂ : M₂) :
        (h.lift f') ((f x₁) x₂) = (f' x₁) x₂
        noncomputable def IsTensorProduct.map {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N] [Module R N₁] [Module R N₂] [Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) :

        The tensor product of a pair of linear maps between modules.

        Equations
        • hf.map hg i₁ i₂ = hg.equiv ∘ₗ TensorProduct.map i₁ i₂ ∘ₗ hf.equiv.symm
        Instances For
          theorem IsTensorProduct.map_eq {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N] [Module R N₁] [Module R N₂] [Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (x₁ : M₁) (x₂ : M₂) :
          (hf.map hg i₁ i₂) ((f x₁) x₂) = (g (i₁ x₁)) (i₂ x₂)
          theorem IsTensorProduct.inductionOn {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) {C : MProp} (m : M) (h0 : C 0) (htmul : ∀ (x : M₁) (y : M₂), C ((f x) y)) (hadd : ∀ (x y : M), C xC yC (x + y)) :
          C m
          def IsBaseChange {R : Type u_1} {M : Type v₁} {N : Type v₂} (S : Type v₃) [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) :

          Given an R-algebra S and an R-module M, an S-module N together with a map f : M →ₗ[R] N is the base change of M to S if the map S × M → N, (s, m) ↦ s • f m is the tensor product.

          Equations
          Instances For
            noncomputable def IsBaseChange.lift {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] [Module R Q] [IsScalarTower R S Q] (g : M →ₗ[R] Q) :

            Suppose f : M →ₗ[R] N is the base change of M along R → S. Then any R-linear map from M to an S-module factors through f.

            Equations
            Instances For
              theorem IsBaseChange.lift_eq {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] [Module R Q] [IsScalarTower R S Q] (g : M →ₗ[R] Q) (x : M) :
              (h.lift g) (f x) = g x
              theorem IsBaseChange.lift_comp {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] [Module R Q] [IsScalarTower R S Q] (g : M →ₗ[R] Q) :
              R (h.lift g) ∘ₗ f = g
              theorem IsBaseChange.inductionOn {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) (x : N) (P : NProp) (h₁ : P 0) (h₂ : ∀ (m : M), P (f m)) (h₃ : ∀ (s : S) (n : N), P nP (s n)) (h₄ : ∀ (n₁ n₂ : N), P n₁P n₂P (n₁ + n₂)) :
              P x
              theorem IsBaseChange.algHom_ext {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] (g₁ : N →ₗ[S] Q) (g₂ : N →ₗ[S] Q) (e : ∀ (x : M), g₁ (f x) = g₂ (f x)) :
              g₁ = g₂
              theorem IsBaseChange.algHom_ext' {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] [Module R Q] [IsScalarTower R S Q] (g₁ : N →ₗ[S] Q) (g₂ : N →ₗ[S] Q) (e : R g₁ ∘ₗ f = R g₂ ∘ₗ f) :
              g₁ = g₂
              theorem TensorProduct.isBaseChange (R : Type u_1) (M : Type v₁) (S : Type v₃) [AddCommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] :
              noncomputable def IsBaseChange.equiv {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) :

              The base change of M along R → S is linearly equivalent to S ⊗[R] M.

              Equations
              • h.equiv = let __src := IsTensorProduct.equiv h; { toAddHom := (__src).toAddHom, map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
              Instances For
                theorem IsBaseChange.equiv_tmul {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) (s : S) (m : M) :
                h.equiv (s ⊗ₜ[R] m) = s f m
                theorem IsBaseChange.equiv_symm_apply {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) (m : M) :
                h.equiv.symm (f m) = 1 ⊗ₜ[R] m
                theorem IsBaseChange.of_lift_unique {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) (h : ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q] [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g' : N →ₗ[S] Q, R g' ∘ₗ f = g) :
                theorem IsBaseChange.iff_lift_unique {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} :
                IsBaseChange S f ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q] [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g' : N →ₗ[S] Q, R g' ∘ₗ f = g
                theorem IsBaseChange.ofEquiv {R : Type u_1} {M : Type v₁} {N : Type v₂} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [Module R M] [Module R N] (e : M ≃ₗ[R] N) :
                theorem IsBaseChange.comp {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {T : Type u_4} {O : Type u_5} [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [AddCommMonoid O] [Module R O] [Module S O] [Module T O] [IsScalarTower S T O] [IsScalarTower R S O] [IsScalarTower R T O] {f : M →ₗ[R] N} (hf : IsBaseChange S f) {g : N →ₗ[S] O} (hg : IsBaseChange T g) :
                IsBaseChange T (R g ∘ₗ f)
                theorem Algebra.isPushout_iff (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (R' : Type u_6) (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] :
                Algebra.IsPushout R S R' S' IsBaseChange S (IsScalarTower.toAlgHom R R' S').toLinearMap
                class Algebra.IsPushout (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (R' : Type u_6) (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] :

                A type-class stating that the following diagram of scalar towers R → S ↓ ↓ R' → S' is a pushout diagram (i.e. S' = S ⊗[R] R')

                Instances
                  theorem Algebra.IsPushout.out {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} {S' : Type u_7} [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [self : Algebra.IsPushout R S R' S'] :
                  IsBaseChange S (IsScalarTower.toAlgHom R R' S').toLinearMap
                  theorem Algebra.IsPushout.symm {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} {S' : Type u_7} [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (h : Algebra.IsPushout R S R' S') :
                  theorem Algebra.IsPushout.comm (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (R' : Type u_6) (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] :
                  instance TensorProduct.isPushout {R : Type u_8} {S : Type u_9} {T : Type u_10} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] :
                  Equations
                  • =
                  instance TensorProduct.isPushout' {R : Type u_8} {S : Type u_9} {T : Type u_10} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] :
                  Equations
                  • =
                  theorem Algebra.pushoutDesc_apply {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [H : Algebra.IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (hf : ∀ (x : S) (y : R'), f x * g y = g y * f x) (a : S') :
                  (Algebra.pushoutDesc S' f g hf) a = (.lift g.toLinearMap) a
                  noncomputable def Algebra.pushoutDesc {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [H : Algebra.IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (hf : ∀ (x : S) (y : R'), f x * g y = g y * f x) :
                  S' →ₐ[R] A

                  If S' = S ⊗[R] R', then any pair of R-algebra homomorphisms f : S → A and g : R' → A such that f x and g y commutes for all x, y descends to a (unique) homomorphism S' → A.

                  Equations
                  Instances For
                    @[simp]
                    theorem Algebra.pushoutDesc_left {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [H : Algebra.IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H : ∀ (x : S) (y : R'), f x * g y = g y * f x) (x : S) :
                    (Algebra.pushoutDesc S' f g H) ((algebraMap S S') x) = f x
                    theorem Algebra.lift_algHom_comp_left {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [Algebra.IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H : ∀ (x : S) (y : R'), f x * g y = g y * f x) :
                    (Algebra.pushoutDesc S' f g H).comp (IsScalarTower.toAlgHom R S S') = f
                    @[simp]
                    theorem Algebra.pushoutDesc_right {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [H : Algebra.IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H : ∀ (x : S) (y : R'), f x * g y = g y * f x) (x : R') :
                    (Algebra.pushoutDesc S' f g H) ((algebraMap R' S') x) = g x
                    theorem Algebra.lift_algHom_comp_right {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [Algebra.IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H : ∀ (x : S) (y : R'), f x * g y = g y * f x) :
                    (Algebra.pushoutDesc S' f g H).comp (IsScalarTower.toAlgHom R R' S') = g
                    theorem Algebra.IsPushout.algHom_ext {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [H : Algebra.IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] {f : S' →ₐ[R] A} {g : S' →ₐ[R] A} (h₁ : f.comp (IsScalarTower.toAlgHom R R' S') = g.comp (IsScalarTower.toAlgHom R R' S')) (h₂ : f.comp (IsScalarTower.toAlgHom R S S') = g.comp (IsScalarTower.toAlgHom R S S')) :
                    f = g