# mathlibdocumentation

ring_theory.is_tensor_product

# The characteristice predicate of tensor product #

## Main definitions #

• is_tensor_product: A predicate on f : M₁ →ₗ[R] M₂ →ₗ[R] M expressing that f realizes M as the tensor product of M₁ ⊗[R] M₂. This is defined by requiring the lift M₁ ⊗[R] M₂ → M to be bijective.
• is_base_change: A predicate on an R-algebra S and a map f : M →ₗ[R] N with N being a S-module, expressing that f realizes N as the base change of M along R → S.

## Main results #

• tensor_product.is_base_change: S ⊗[R] M is the base change of M along R → S.
def is_tensor_product {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] [ M] (f : M₁ →ₗ[R] M₂ →ₗ[R] M) :
Prop

Given a bilinear map f : M₁ →ₗ[R] M₂ →ₗ[R] M, is_tensor_product 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
theorem tensor_product.is_tensor_product (R : Type u_1) [comm_ring R] (M : Type u_4) [ M] (N : Type u_8) [ N] :
noncomputable def is_tensor_product.equiv {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] [ M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : is_tensor_product f) :
M₁ M₂ ≃ₗ[R] M

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

Equations
@[simp]
theorem is_tensor_product.equiv_apply {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] [ M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : is_tensor_product f) (ᾰ : M₁ M₂) :
(h.equiv) ᾰ =
@[simp]
theorem is_tensor_product.equiv_to_linear_map {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] [ M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : is_tensor_product f) :
@[simp]
theorem is_tensor_product.equiv_symm_apply {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] [ M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : is_tensor_product f) (x₁ : M₁) (x₂ : M₂) :
(h.equiv.symm) ((f x₁) x₂) = x₁ ⊗ₜ[R] x₂
noncomputable def is_tensor_product.lift {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} {M' : Type u_5} [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M'] [ M₁] [ M₂] [ M] [ M'] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : is_tensor_product 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
theorem is_tensor_product.lift_eq {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} {M' : Type u_5} [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M'] [ M₁] [ M₂] [ M] [ M'] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : is_tensor_product f) (f' : M₁ →ₗ[R] M₂ →ₗ[R] M') (x₁ : M₁) (x₂ : M₂) :
(h.lift f') ((f x₁) x₂) = (f' x₁) x₂
noncomputable def is_tensor_product.map {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] [ M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [add_comm_monoid N₁] [add_comm_monoid N₂] [ N₁] [ N₂] [ N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : is_tensor_product f) (hg : is_tensor_product g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) :

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

Equations
theorem is_tensor_product.map_eq {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] [ M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [add_comm_monoid N₁] [add_comm_monoid N₂] [ N₁] [ N₂] [ N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : is_tensor_product f) (hg : is_tensor_product 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 is_tensor_product.induction_on {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] [ M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : is_tensor_product f) {C : M → Prop} (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 is_base_change {R : Type u_1} {M : Type v₁} {N : Type v₂} (S : Type v₃) [comm_ring R] [comm_ring S] [ S] [ M] [ N] [ N] [ N] (f : M →ₗ[R] N) :
Prop

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
noncomputable def is_base_change.lift {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [comm_ring R] [comm_ring S] [ S] [ M] [ N] [ N] [ N] {f : M →ₗ[R] N} (h : f) {Q : Type u_3} [ Q] [ Q] [ 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 thorugh f.

Equations
theorem is_base_change.lift_eq {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [comm_ring R] [comm_ring S] [ S] [ M] [ N] [ N] [ N] {f : M →ₗ[R] N} (h : f) {Q : Type u_3} [ Q] [ Q] [ Q] (g : M →ₗ[R] Q) (x : M) :
(h.lift g) (f x) = g x
theorem is_base_change.lift_comp {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [comm_ring R] [comm_ring S] [ S] [ M] [ N] [ N] [ N] {f : M →ₗ[R] N} (h : f) {Q : Type u_3} [ Q] [ Q] [ Q] (g : M →ₗ[R] Q) :
(h.lift g)).comp f = g
theorem is_base_change.induction_on {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [comm_ring R] [comm_ring S] [ S] [ M] [ N] [ N] [ N] {f : M →ₗ[R] N} (h : f) (x : N) (P : N → Prop) (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 is_base_change.alg_hom_ext {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [comm_ring R] [comm_ring S] [ S] [ M] [ N] [ N] [ N] {f : M →ₗ[R] N} (h : f) {Q : Type u_3} [ Q] (g₁ g₂ : N →ₗ[S] Q) (e : ∀ (x : M), g₁ (f x) = g₂ (f x)) :
g₁ = g₂
theorem is_base_change.alg_hom_ext' {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [comm_ring R] [comm_ring S] [ S] [ M] [ N] [ N] [ N] {f : M →ₗ[R] N} (h : f) {Q : Type u_3} [ Q] [ Q] [ Q] (g₁ g₂ : N →ₗ[S] Q) (e : .comp f = .comp f) :
g₁ = g₂
theorem tensor_product.is_base_change (R : Type u_1) (M : Type v₁) (S : Type v₃) [comm_ring R] [comm_ring S] [ S] [ M] :
( M) 1)
noncomputable def is_base_change.equiv {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [comm_ring R] [comm_ring S] [ S] [ M] [ N] [ N] [ N] {f : M →ₗ[R] N} (h : f) :
M ≃ₗ[R] N

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

Equations
theorem is_base_change.equiv_tmul {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [comm_ring R] [comm_ring S] [ S] [ M] [ N] [ N] [ N] {f : M →ₗ[R] N} (h : f) (s : S) (m : M) :
(h.equiv) (s ⊗ₜ[R] m) = s f m
theorem is_base_change.equiv_symm_apply {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [comm_ring R] [comm_ring S] [ S] [ M] [ N] [ N] [ N] {f : M →ₗ[R] N} (h : f) (m : M) :
(h.equiv.symm) (f m) = 1 ⊗ₜ[R] m
theorem is_base_change.of_lift_unique {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [comm_ring R] [comm_ring S] [ S] [ M] [ N] [ N] [ N] (f : M →ₗ[R] N) (h : ∀ (Q : Type (max v₁ v₂ v₃)) [_inst_14 : [_inst_15 : Q] [_inst_16 : Q] [_inst_15_1 : Q] (g : M →ₗ[R] Q), ∃! (g' : N →ₗ[S] Q), .comp f = g) :
theorem is_base_change.iff_lift_unique {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [comm_ring R] [comm_ring S] [ S] [ M] [ N] [ N] [ N] {f : M →ₗ[R] N} :
∀ (Q : Type (max v₁ v₂ v₃)) [_inst_14 : [_inst_15 : Q] [_inst_16 : Q] [_inst_15_1 : Q] (g : M →ₗ[R] Q), ∃! (g' : N →ₗ[S] Q), .comp f = g
theorem is_base_change.of_equiv {R : Type u_1} {M : Type v₁} {N : Type v₂} [comm_ring R] [ M] [ N] (e : M ≃ₗ[R] N) :
theorem is_base_change.comp {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [comm_ring R] [comm_ring S] [ S] [ M] [ N] [ N] [ N] {T : Type u_4} {O : Type u_5} [comm_ring T] [ T] [ T] [ T] [ O] [ O] [ O] [ O] [ O] [ O] {f : M →ₗ[R] N} (hf : f) {g : N →ₗ[S] O} (hg : g) :
.comp f)
theorem is_base_change.symm {R : Type u_1} {S : Type v₃} [comm_ring R] [comm_ring S] [ S] {R' : Type u_6} {S' : Type u_7} [comm_ring R'] [comm_ring S'] [ R'] [ S'] [algebra R' S'] [ S'] [ R' S'] [ S'] (h : S').to_linear_map) :
theorem is_base_change.comm (R : Type u_1) (S : Type v₃) [comm_ring R] [comm_ring S] [ S] (R' : Type u_6) (S' : Type u_7) [comm_ring R'] [comm_ring S'] [ R'] [ S'] [algebra R' S'] [ S'] [ R' S'] [ S'] :