lTensor_mkQ
theorem lTensor_mkQ :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (Q : Type u_5)
[inst_3 : AddCommGroup Q] [inst_4 : Module R Q] (N : Submodule R M),
LinearMap.ker (LinearMap.lTensor Q N.mkQ) = LinearMap.range (LinearMap.lTensor Q N.subtype)
This theorem states the right-exactness of the tensor product. Specifically, for any commutative ring `R`, additively commutative group `M` and `Q`, and `M` and `Q` as modules over `R`, and for any submodule `N` of `M`, the kernel of the linear map obtained by tensoring the quotient map `N.mkQ` with `Q`, is equal to the range of the linear map obtained by tensoring the subtype map of `N` with `Q`. This property is fundamental in the theory of modules and tensor products.
More concisely: For any commutative ring `R`, additively commutative groups `M` and `Q`, and submodule `N` of `M`, the kernel of `N.mkQ ⊗ Q` is equal to the image of `N ⊗ Q` in `M ⊗ Q`.
|
lTensor_exact
theorem lTensor_exact :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q]
[inst_8 : Module R Q],
Function.Exact ⇑f ⇑g →
Function.Surjective ⇑g → Function.Exact ⇑(LinearMap.lTensor Q f) ⇑(LinearMap.lTensor Q g)
The theorem `lTensor_exact` states that for any exact pair of functions `f` and `g` in the context of commutative rings and additive commutative groups, tensoring the pair on the left with a linear map gives another exact pair. Here, an exact pair of functions `f` and `g` means that for every element `y` of the domain of `g`, `g y` equals zero if and only if `y` belongs to the image of `f`. Furthermore, `g` is surjective, meaning that every element in its codomain is the image of some element in its domain. The theorem then claims that if this condition holds, then applying the tensor product to `f` and `g` forms an exact pair as well.
More concisely: If `f` and `g` form an exact pair of functions between commutative rings and additive commutative groups with `g` being surjective, then the tensor product of `f` with a linear map is an exact pair.
|
Ideal.map_includeLeft_eq
theorem Ideal.map_includeLeft_eq :
∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} {B : Type u_3} [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal A),
Submodule.restrictScalars R (Ideal.map Algebra.TensorProduct.includeLeft I) =
LinearMap.range (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype)
This theorem states that, for a commutative semiring `R` and semirings `A` and `B` with `R`-algebra structures, given an ideal `I` in `A`, the ideal of the tensor product `A ⊗[R] B` generated by `I` is the same as the image of `I ⊗[R] B` under the inclusion of `I` into `A`. This is expressed formally by stating that the restriction of the ideal mapped by the left inclusion of `A` in `A ⊗[R] B` to scalars in `R` is equal to the range of the tensor product of `I` and `B` subject to the restriction of `I` to scalars from `R`.
More concisely: For a commutative semiring `R`, and `R`-algebra structures on semirings `A` and `B`, the ideal of `A ⊗[R] B` generated by `I ⊆ A` is equal to the image of `I ⊗[R] B` under the inclusion map from `A` to `A ⊗[R] B`, when restricted to scalars in `R`.
|
rTensor_mkQ
theorem rTensor_mkQ :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (Q : Type u_5)
[inst_3 : AddCommGroup Q] [inst_4 : Module R Q] (N : Submodule R M),
LinearMap.ker (LinearMap.rTensor Q N.mkQ) = LinearMap.range (LinearMap.rTensor Q N.subtype)
The theorem `rTensor_mkQ` states that for any type `R` with a commutative ring structure, type `M` with an additive commutative group structure and a module structure over `R`, and type `Q` with an additive commutative group structure and a module structure over `R`, and for any submodule `N` of `M`, the kernel of the right-tensor product of `Q` with the quotient map `N.mkQ` is equal to the range of the right-tensor product of `Q` with the subtype inclusion map of `N`. This theorem is a statement about the right-exactness of the tensor product.
More concisely: For any commutative ring R, additive commutative groups M and Q with R-module structures, and a submodule N of M, the kernel of Q ⊗\_R (N.quot_map) equals the image of Q ⊗\_R (N.subtype.inclusion).
|
Algebra.TensorProduct.lTensor_ker
theorem Algebra.TensorProduct.lTensor_ker :
∀ {R : Type u_4} [inst : CommRing R] {A : Type u_5} {C : Type u_7} {D : Type u_8} [inst_1 : Ring A]
[inst_2 : Ring C] [inst_3 : Ring D] [inst_4 : Algebra R A] [inst_5 : Algebra R C] [inst_6 : Algebra R D]
(g : C →ₐ[R] D),
Function.Surjective ⇑g →
RingHom.ker (Algebra.TensorProduct.map (AlgHom.id R A) g) =
Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)
The theorem `Algebra.TensorProduct.lTensor_ker` states that for any commutative ring `R` and rings `A`, `C`, `D` with `A`, `C`, `D` being `R`-algebras, if we have a surjective algebra homomorphism `g` from `C` to `D`, then the kernel of the algebra homomorphism formed by taking the tensor product of the identity on `A` and `g`, is equal to the ideal generated by taking the image of the kernel of `g` under the algebra homomorphism that maps an element `b` in `B` to `1 ⊗ₜ b` in the tensor product of `R`, `A` and `B`. In other words, the theorem shows a relationship between the kernel of an algebra homomorphism involving a tensor product and the kernel of the original algebra homomorphism.
More concisely: For any commutative ring R and R-algebras A, C, D with a surjective algebra homomorphism g from C to D, the kernel of the tensor product homomorphism Idₗ(A) ⊗ g is equal to the ideal generated by the images of the kernel of g under the homomorphism mapping b to 1 ⊗ b in the tensor product of R, A, and B.
|
Algebra.TensorProduct.map_ker
theorem Algebra.TensorProduct.map_ker :
∀ {R : Type u_4} [inst : CommRing R] {A : Type u_5} {B : Type u_6} {C : Type u_7} {D : Type u_8} [inst_1 : Ring A]
[inst_2 : Ring B] [inst_3 : Ring C] [inst_4 : Ring D] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
[inst_7 : Algebra R C] [inst_8 : Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D),
Function.Surjective ⇑f →
Function.Surjective ⇑g →
RingHom.ker (Algebra.TensorProduct.map f g) =
Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f) ⊔
Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)
The theorem `Algebra.TensorProduct.map_ker` states that if `f` and `g` are surjective algebra morphisms (maps that preserve the operations of addition and multiplication, as well as the multiplicative identity and the distribution of multiplication over addition), then the kernel of the map induced by `f` and `g` on the tensor product of the algebras is generated by the kernels of `f` and `g`. Here, the kernel of a morphism is the ideal (a subset of the ring that is closed under addition and multiplication by any element of the ring) of elements that are mapped to zero, and a map is said to be surjective if every element in the target is the image of some element in the domain. The tensor product of two algebras over a common ring `R` is a way of combining the algebras to get a new one, while preserving the operations of the algebras and their interaction with `R`. The theorem is saying that the elements that get mapped to zero in the tensor product are exactly those that come from elements that get mapped to zero in the original algebras.
More concisely: If `f` and `g` are surjective algebra morphisms, then the kernel of their composite map on the tensor product of the algebras is the ideal generated by the kernels of `f` and `g`.
|
rTensor_exact
theorem rTensor_exact :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q]
[inst_8 : Module R Q],
Function.Exact ⇑f ⇑g →
Function.Surjective ⇑g → Function.Exact ⇑(LinearMap.rTensor Q f) ⇑(LinearMap.rTensor Q g)
The theorem `rTensor_exact` states that, given any commutative ring `R` and additive commutative groups `M`, `N`, `P`, and `Q`, wherein `M`, `N`, `P` are modules over `R`. If the maps `f: M -> N` and `g: N -> P` made up an exact pair and `g` was surjective, then tensoring `f` and `g` on the right with `Q` would also result in an exact pair. That is, the image of `f` tensor `Q` is exactly the preimage of `0` under `g` tensor `Q`.
In other words, for any element in the domain of `g` tensor `Q`, it maps to `0` if and only if it is in the range of `f` tensor `Q`. This theorem emphasizes the preservation of the exactness property under the tensor operation.
More concisely: Given commutative rings R, additive commutative groups M, N, P, and Q, and surjective map g : N -> P, if the pair (M -> N) x (N -> P) forms an exact sequence and g tensor Q : N tensor Q -> P tensor Q is surjective, then the tensor product M tensor Q -> P tensor Q is an exact functor.
|
TensorProduct.map_ker
theorem TensorProduct.map_ker :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P},
Function.Exact ⇑f ⇑g →
Function.Surjective ⇑g →
∀ {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} [inst_7 : AddCommGroup M'] [inst_8 : AddCommGroup N']
[inst_9 : AddCommGroup P'] [inst_10 : Module R M'] [inst_11 : Module R N'] [inst_12 : Module R P']
{f' : M' →ₗ[R] N'} {g' : N' →ₗ[R] P'},
Function.Exact ⇑f' ⇑g' →
Function.Surjective ⇑g' →
LinearMap.ker (TensorProduct.map g g') =
LinearMap.range (LinearMap.lTensor N f') ⊔ LinearMap.range (LinearMap.rTensor N' f)
This theorem, named `TensorProduct.map_ker`, states that in the context of a commutative ring `R` and additive commutative groups `M`, `N`, `P`, `M'`, `N'`, `P'`, which are modules over `R`, given two linear maps `f: M →ₗ[R] N` and `g: N →ₗ[R] P` such that `f` and `g` form an exact pair (i.e., `g y = 0` if and only if `y` belongs to the image of `f`) and `g` is surjective, then for any two other linear maps `f': M' →ₗ[R] N'` and `g': N' →ₗ[R] P'` that also form an exact pair and with `g'` being surjective, the kernel of the tensor product of `g` and `g'` is equal to the union of the image of the left tensor product of `N` and `f'` and the image of the right tensor product of `N'` and `f`. This theorem is essentially about the right exactness property of tensor product in the context of linear maps and modules.
More concisely: Given commutative rings `R`, additive commutative groups `M`, `N`, `P`, `M'`, `N'`, `P'` as `R`-modules, and linear maps `f: M → N`, `g: N → P`, `f': M' → N'`, `g': N' → P'` satisfying `g y = 0` if and only if `y ∈ im(f)` and `g' y' = 0` if and only if `y' ∈ im(f')`, with `g` and `g'` being surjective, the kernel of `g ⊗ g'` equals `im(N ⊗_[R] f') ∪ im(N' ⊗_[R] f)`.
|
Ideal.map_includeRight_eq
theorem Ideal.map_includeRight_eq :
∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} {B : Type u_3} [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal B),
Submodule.restrictScalars R (Ideal.map Algebra.TensorProduct.includeRight I) =
LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype)
The theorem `Ideal.map_includeRight_eq` states that for commutative semiring `R`, semirings `A` and `B`, with `A` and `B` being an algebra over `R`, and an ideal `I` of `B`, the ideal of the tensor product `A ⊗[R] B` generated by `I` is equal to the image of `A ⊗[R] I`. In other words, if we consider the ideal of `B` as a scalar in the tensor product and map it using the function `Algebra.TensorProduct.includeRight`, the resulting ideal is equivalent to the range of the linear map induced by the natural inclusion of `I` into `B`, tensored with `A`. This equality is obtained when restricting scalars over `R`.
More concisely: The ideal of the tensor product of an algebra over a commutative semiring generated by an ideal of another algebra is equal to the image of the ideal mapped using the `includeRight` function.
|
Algebra.TensorProduct.rTensor_ker
theorem Algebra.TensorProduct.rTensor_ker :
∀ {R : Type u_4} [inst : CommRing R] {A : Type u_5} {B : Type u_6} {C : Type u_7} [inst_1 : Ring A]
[inst_2 : Ring B] [inst_3 : Ring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
(f : A →ₐ[R] B),
Function.Surjective ⇑f →
RingHom.ker (Algebra.TensorProduct.map f (AlgHom.id R C)) =
Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f)
The theorem `Algebra.TensorProduct.rTensor_ker` states that for any commutative ring `R` and rings `A`, `B`, `C`, which are algebras over `R`, and a surjective algebra homomorphism `f` from `A` to `B`, the kernel of the ring homomorphism given by the tensor product of `f` and the identity on `C` is generated by the image under the tensor product map of the kernel of `f`. In simpler terms, if `f` is a function that covers all elements of `B`, then the elements that get mapped to zero under the tensor product of `f` and the identity function on `C`, come from the set of elements that get mapped to zero by `f` under a certain mapping.
More concisely: The kernel of the tensor product homomorphism from `A ⊗\_R C` to `B ⊗\_R C`, induced by a surjective algebra homomorphism `f : A → B`, is equal to the image under the tensor product map of the kernel of `f`.
|