mathlib3 documentation

ring_theory.is_tensor_product

The characteristice predicate of tensor product #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

Main results #

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₂] [add_comm_monoid M] [module R M₁] [module R M₂] [module R 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
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₂] [add_comm_monoid M] [module R M₁] [module R M₂] [module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : is_tensor_product f) :
tensor_product R 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₂] [add_comm_monoid M] [module R M₁] [module R M₂] [module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : is_tensor_product f) (ᾰ : tensor_product R M₁ M₂) :
@[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₂] [add_comm_monoid M] [module R M₁] [module R M₂] [module R 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₂] [add_comm_monoid M] [module R M₁] [module R M₂] [module R 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] [add_comm_monoid M'] [module R M₁] [module R M₂] [module R M] [module R 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] [add_comm_monoid M'] [module R M₁] [module R M₂] [module R M] [module R 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₂] [add_comm_monoid 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} [add_comm_monoid N₁] [add_comm_monoid N₂] [add_comm_monoid N] [module R N₁] [module R N₂] [module R 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₂] [add_comm_monoid 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} [add_comm_monoid N₁] [add_comm_monoid N₂] [add_comm_monoid N] [module R N₁] [module R N₂] [module R 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₂] [add_comm_monoid M] [module R M₁] [module R M₂] [module R 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 x C y C (x + y)) :
C m
def is_base_change {R : Type u_1} {M : Type v₁} {N : Type v₂} (S : Type v₃) [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [comm_ring S] [algebra R S] [module R M] [module R N] [module S N] [is_scalar_tower R S 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₃} [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [comm_ring S] [algebra R S] [module R M] [module R N] [module S N] [is_scalar_tower R S N] {f : M →ₗ[R] N} (h : is_base_change S f) {Q : Type u_3} [add_comm_monoid Q] [module S Q] [module R Q] [is_scalar_tower 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 thorugh f.

Equations
theorem is_base_change.lift_eq {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [comm_ring S] [algebra R S] [module R M] [module R N] [module S N] [is_scalar_tower R S N] {f : M →ₗ[R] N} (h : is_base_change S f) {Q : Type u_3} [add_comm_monoid Q] [module S Q] [module R Q] [is_scalar_tower R S 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₃} [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [comm_ring S] [algebra R S] [module R M] [module R N] [module S N] [is_scalar_tower R S N] {f : M →ₗ[R] N} (h : is_base_change S f) {Q : Type u_3} [add_comm_monoid Q] [module S Q] [module R Q] [is_scalar_tower R S Q] (g : M →ₗ[R] Q) :
theorem is_base_change.induction_on {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [comm_ring S] [algebra R S] [module R M] [module R N] [module S N] [is_scalar_tower R S N] {f : M →ₗ[R] N} (h : is_base_change S f) (x : N) (P : N Prop) (h₁ : P 0) (h₂ : (m : M), P (f m)) (h₃ : (s : S) (n : N), P n P (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₃} [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [comm_ring S] [algebra R S] [module R M] [module R N] [module S N] [is_scalar_tower R S N] {f : M →ₗ[R] N} (h : is_base_change S f) {Q : Type u_3} [add_comm_monoid Q] [module S 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₃} [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [comm_ring S] [algebra R S] [module R M] [module R N] [module S N] [is_scalar_tower R S N] {f : M →ₗ[R] N} (h : is_base_change S f) {Q : Type u_3} [add_comm_monoid Q] [module S Q] [module R Q] [is_scalar_tower R S Q] (g₁ g₂ : N →ₗ[S] Q) (e : (linear_map.restrict_scalars R g₁).comp f = (linear_map.restrict_scalars R g₂).comp f) :
g₁ = g₂
theorem tensor_product.is_base_change (R : Type u_1) (M : Type v₁) (S : Type v₃) [add_comm_monoid M] [comm_ring R] [comm_ring S] [algebra R S] [module R M] :
noncomputable def is_base_change.equiv {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [comm_ring S] [algebra R S] [module R M] [module R N] [module S N] [is_scalar_tower R S N] {f : M →ₗ[R] N} (h : is_base_change S f) :

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₃} [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [comm_ring S] [algebra R S] [module R M] [module R N] [module S N] [is_scalar_tower R S N] {f : M →ₗ[R] N} (h : is_base_change S 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₃} [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [comm_ring S] [algebra R S] [module R M] [module R N] [module S N] [is_scalar_tower R S N] {f : M →ₗ[R] N} (h : is_base_change S 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₃} [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [comm_ring S] [algebra R S] [module R M] [module R N] [module S N] [is_scalar_tower R S N] (f : M →ₗ[R] N) (h : (Q : Type (max v₁ v₂ v₃)) [_inst_14 : add_comm_monoid Q] [_inst_15 : module R Q] [_inst_16 : module S Q] [_inst_15_1 : is_scalar_tower R S Q] (g : M →ₗ[R] Q), ∃! (g' : N →ₗ[S] Q), (linear_map.restrict_scalars R g').comp f = g) :
theorem is_base_change.iff_lift_unique {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [comm_ring S] [algebra R S] [module R M] [module R N] [module S N] [is_scalar_tower R S N] {f : M →ₗ[R] N} :
is_base_change S f (Q : Type (max v₁ v₂ v₃)) [_inst_14 : add_comm_monoid Q] [_inst_15 : module R Q] [_inst_16 : module S Q] [_inst_15_1 : is_scalar_tower R S Q] (g : M →ₗ[R] Q), ∃! (g' : N →ₗ[S] Q), (linear_map.restrict_scalars R g').comp f = g
theorem is_base_change.of_equiv {R : Type u_1} {M : Type v₁} {N : Type v₂} [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [module R M] [module R N] (e : M ≃ₗ[R] N) :
theorem is_base_change.comp {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [add_comm_monoid M] [add_comm_monoid N] [comm_ring R] [comm_ring S] [algebra R S] [module R M] [module R N] [module S N] [is_scalar_tower R S N] {T : Type u_4} {O : Type u_5} [comm_ring T] [algebra R T] [algebra S T] [is_scalar_tower R S T] [add_comm_monoid O] [module R O] [module S O] [module T O] [is_scalar_tower S T O] [is_scalar_tower R S O] [is_scalar_tower R T O] {f : M →ₗ[R] N} (hf : is_base_change S f) {g : N →ₗ[S] O} (hg : is_base_change T g) :
@[class]
structure algebra.is_pushout (R : Type u_1) (S : Type v₃) [comm_ring R] [comm_ring S] [algebra R S] (R' : Type u_6) (S' : Type u_7) [comm_ring R'] [comm_ring S'] [algebra R R'] [algebra S S'] [algebra R' S'] [algebra R S'] [is_scalar_tower R R' S'] [is_scalar_tower R S S'] :
Prop

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 of this typeclass
theorem algebra.is_pushout_iff (R : Type u_1) (S : Type v₃) [comm_ring R] [comm_ring S] [algebra R S] (R' : Type u_6) (S' : Type u_7) [comm_ring R'] [comm_ring S'] [algebra R R'] [algebra S S'] [algebra R' S'] [algebra R S'] [is_scalar_tower R R' S'] [is_scalar_tower R S S'] :
theorem algebra.is_pushout.symm {R : Type u_1} {S : Type v₃} [comm_ring R] [comm_ring S] [algebra R S] {R' : Type u_6} {S' : Type u_7} [comm_ring R'] [comm_ring S'] [algebra R R'] [algebra S S'] [algebra R' S'] [algebra R S'] [is_scalar_tower R R' S'] [is_scalar_tower R S S'] (h : algebra.is_pushout R S R' S') :
theorem algebra.is_pushout.comm (R : Type u_1) (S : Type v₃) [comm_ring R] [comm_ring S] [algebra R S] (R' : Type u_6) (S' : Type u_7) [comm_ring R'] [comm_ring S'] [algebra R R'] [algebra S S'] [algebra R' S'] [algebra R S'] [is_scalar_tower R R' S'] [is_scalar_tower R S S'] :
@[protected, instance]
def tensor_product.is_pushout {R : Type u_1} {S : Type u_2} {T : Type u_3} [comm_ring R] [comm_ring S] [comm_ring T] [algebra R S] [algebra R T] :
@[protected, instance]
def tensor_product.is_pushout' {R : Type u_1} {S : Type u_2} {T : Type u_3} [comm_ring R] [comm_ring S] [comm_ring T] [algebra R S] [algebra R T] :
theorem algebra.pushout_desc_apply {R : Type u_1} {S : Type v₃} [comm_ring R] [comm_ring S] [algebra R S] {R' : Type u_6} (S' : Type u_7) [comm_ring R'] [comm_ring S'] [algebra R R'] [algebra S S'] [algebra R' S'] [algebra R S'] [is_scalar_tower R R' S'] [is_scalar_tower R S S'] [H : algebra.is_pushout R S R' S'] {A : Type u_2} [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') :
noncomputable def algebra.pushout_desc {R : Type u_1} {S : Type v₃} [comm_ring R] [comm_ring S] [algebra R S] {R' : Type u_6} (S' : Type u_7) [comm_ring R'] [comm_ring S'] [algebra R R'] [algebra S S'] [algebra R' S'] [algebra R S'] [is_scalar_tower R R' S'] [is_scalar_tower R S S'] [H : algebra.is_pushout R S R' S'] {A : Type u_2} [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) homomoprhism S' → A.

Equations
@[simp]
theorem algebra.pushout_desc_left {R : Type u_1} {S : Type v₃} [comm_ring R] [comm_ring S] [algebra R S] {R' : Type u_6} (S' : Type u_7) [comm_ring R'] [comm_ring S'] [algebra R R'] [algebra S S'] [algebra R' S'] [algebra R S'] [is_scalar_tower R R' S'] [is_scalar_tower R S S'] [H : algebra.is_pushout R S R' S'] {A : Type u_2} [semiring A] [algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H_1 : (x : S) (y : R'), f x * g y = g y * f x) (x : S) :
(algebra.pushout_desc S' f g H_1) ((algebra_map S S') x) = f x
theorem algebra.lift_alg_hom_comp_left {R : Type u_1} {S : Type v₃} [comm_ring R] [comm_ring S] [algebra R S] {R' : Type u_6} (S' : Type u_7) [comm_ring R'] [comm_ring S'] [algebra R R'] [algebra S S'] [algebra R' S'] [algebra R S'] [is_scalar_tower R R' S'] [is_scalar_tower R S S'] [H : algebra.is_pushout R S R' S'] {A : Type u_2} [semiring A] [algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H_1 : (x : S) (y : R'), f x * g y = g y * f x) :
@[simp]
theorem algebra.pushout_desc_right {R : Type u_1} {S : Type v₃} [comm_ring R] [comm_ring S] [algebra R S] {R' : Type u_6} (S' : Type u_7) [comm_ring R'] [comm_ring S'] [algebra R R'] [algebra S S'] [algebra R' S'] [algebra R S'] [is_scalar_tower R R' S'] [is_scalar_tower R S S'] [H : algebra.is_pushout R S R' S'] {A : Type u_2} [semiring A] [algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H_1 : (x : S) (y : R'), f x * g y = g y * f x) (x : R') :
(algebra.pushout_desc S' f g H_1) ((algebra_map R' S') x) = g x
theorem algebra.lift_alg_hom_comp_right {R : Type u_1} {S : Type v₃} [comm_ring R] [comm_ring S] [algebra R S] {R' : Type u_6} (S' : Type u_7) [comm_ring R'] [comm_ring S'] [algebra R R'] [algebra S S'] [algebra R' S'] [algebra R S'] [is_scalar_tower R R' S'] [is_scalar_tower R S S'] [H : algebra.is_pushout R S R' S'] {A : Type u_2} [semiring A] [algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H_1 : (x : S) (y : R'), f x * g y = g y * f x) :
@[ext]
theorem algebra.is_pushout.alg_hom_ext {R : Type u_1} {S : Type v₃} [comm_ring R] [comm_ring S] [algebra R S] {R' : Type u_6} (S' : Type u_7) [comm_ring R'] [comm_ring S'] [algebra R R'] [algebra S S'] [algebra R' S'] [algebra R S'] [is_scalar_tower R R' S'] [is_scalar_tower R S S'] [H : algebra.is_pushout R S R' S'] {A : Type u_2} [semiring A] [algebra R A] {f g : S' →ₐ[R] A} (h₁ : f.comp (is_scalar_tower.to_alg_hom R R' S') = g.comp (is_scalar_tower.to_alg_hom R R' S')) (h₂ : f.comp (is_scalar_tower.to_alg_hom R S S') = g.comp (is_scalar_tower.to_alg_hom R S S')) :
f = g