The characteristice predicate of tensor product #
Main definitions #
is_tensor_product: A predicate onf : M₁ →ₗ[R] M₂ →ₗ[R] Mexpressing thatfrealizesMas the tensor product ofM₁ ⊗[R] M₂. This is defined by requiring the liftM₁ ⊗[R] M₂ → Mto be bijective.is_base_change: A predicate on anR-algebraSand a mapf : M →ₗ[R] NwithNbeing aS-module, expressing thatfrealizesNas the base change ofMalongR → S.
Main results #
tensor_product.is_base_change:S ⊗[R] Mis the base change ofMalongR → 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₂]
[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
theorem
tensor_product.is_tensor_product
(R : Type u_1)
[comm_ring R]
(M : Type u_4)
[add_comm_monoid M]
[module R M]
(N : Type u_8)
[add_comm_monoid N]
[module R N] :
is_tensor_product (tensor_product.mk R M 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₂]
[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
- h.equiv = linear_equiv.of_bijective (tensor_product.lift f) _ _
@[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₂) :
⇑(h.equiv) ᾰ = ⇑(tensor_product.lift f) ᾰ
@[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₂) :
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') :
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
- h.lift f' = (tensor_product.lift f').comp h.equiv.symm.to_linear_map
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₂) :
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
- hf.map hg i₁ i₂ = hg.equiv.to_linear_map.comp ((tensor_product.map i₁ i₂).comp hf.equiv.symm.to_linear_map)
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₂) :
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
- is_base_change S f = is_tensor_product (linear_map.restrict_scalars R (⇑((algebra.of_id S (module.End S (M →ₗ[R] N))).to_linear_map.flip) f))
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
- h.lift g = {to_fun := (is_tensor_product.lift h (linear_map.restrict_scalars R (⇑((algebra.of_id S (module.End S (M →ₗ[R] Q))).to_linear_map.flip) g))).to_fun, map_add' := _, map_smul' := _}
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) :
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) :
(linear_map.restrict_scalars R (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₃}
[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] :
is_base_change S (⇑(tensor_product.mk R S M) 1)
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) :
tensor_product R S 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₃}
[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) :
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) :
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) :
is_base_change S f
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) :
is_base_change T ((linear_map.restrict_scalars R g).comp f)
theorem
is_base_change.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 : is_base_change S (is_scalar_tower.to_alg_hom R R' S').to_linear_map) :
is_base_change R' (is_scalar_tower.to_alg_hom R S S').to_linear_map
theorem
is_base_change.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'] :
is_base_change S (is_scalar_tower.to_alg_hom R R' S').to_linear_map ↔ is_base_change R' (is_scalar_tower.to_alg_hom R S S').to_linear_map