Documentation

TauCeti.RingTheory.TensorProduct.Pi

Tensor products of algebras and products #

Mathlib's Algebra.TensorProduct.prodRight distributes A ⊗[R] (B × C) over the product in the right factor. This file gives the algebra equivalence for a product in the left factor, (A₁ × A₂) ⊗[R] B ≃ₐ[R] (A₁ ⊗[R] B) × (A₂ ⊗[R] B): the algebra form of Mathlib's linear TensorProduct.prodLeft. It also evaluates the inverse of Mathlib's Algebra.TensorProduct.piScalarRight : A ⊗[R] (ι → R) ≃ₐ[S] (ι → A) on Pi.single i x, so that simp computes the matrix entries of a base change of an algebra map between function algebras. Base-changing a section factoring through a coordinate projection commutes with the same product decomposition (AlgHom.sectionBaseChange_comp_evalAlgHom).

Main declarations #

source
def TauCeti.Algebra.TensorProduct.prodLeft (R : Type u_1) (A₁ : Type u_2) (A₂ : Type u_3) (B : Type u_4) [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring B] [Algebra R A₁] [Algebra R A₂] [Algebra R B] :
TensorProduct R (A₁ × A₂) B ≃ₐ[R] TensorProduct R A₁ B × TensorProduct R A₂ B

The tensor product of algebras distributes over a product in the left factor: (A₁ × A₂) ⊗[R] B ≃ₐ[R] (A₁ ⊗[R] B) × (A₂ ⊗[R] B).

Instances For
    source
    @[simp]
    theorem TauCeti.Algebra.TensorProduct.prodLeft_tmul {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring B] [Algebra R A₁] [Algebra R A₂] [Algebra R B] (a₁ : A₁) (a₂ : A₂) (b : B) :
    (prodLeft R A₁ A₂ B) ((a₁, a₂) ⊗ₜ[R] b) = (a₁ ⊗ₜ[R] b, a₂ ⊗ₜ[R] b)

    prodLeft sends a pure tensor (a₁, a₂) ⊗ₜ b to the pair (a₁ ⊗ₜ b, a₂ ⊗ₜ b).

    source
    @[simp]
    theorem TauCeti.Algebra.TensorProduct.prodLeft_symm_tmul {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring B] [Algebra R A₁] [Algebra R A₂] [Algebra R B] (a₁ : A₁) (a₂ : A₂) (b : B) :
    (prodLeft R A₁ A₂ B).symm (a₁ ⊗ₜ[R] b, a₂ ⊗ₜ[R] b) = (a₁, a₂) ⊗ₜ[R] b

    The inverse of prodLeft sends (a₁ ⊗ₜ b, a₂ ⊗ₜ b) to (a₁, a₂) ⊗ₜ b.

    source
    @[simp]
    theorem TauCeti.Algebra.TensorProduct.piScalarRight_symm_single (R : Type u_5) (S : Type u_6) (A : Type u_7) {ι : Type u_8} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Fintype ι] [DecidableEq ι] (x : A) (i : ι) :
    (Algebra.TensorProduct.piScalarRight R S A ι).symm (Pi.single i x) = x ⊗ₜ[R] Pi.single i 1

    The inverse of piScalarRight sends Pi.single i x to x ⊗ₜ Pi.single i 1: the algebra form of Mathlib's TensorProduct.piScalarRight_symm_single.

    source
    @[simp]
    theorem AlgHom.sectionBaseChange_comp_evalAlgHom {A : Type u_1} [CommSemiring A] {κ : Type u_2} [Fintype κ] [DecidableEq κ] {B : κ → Type u_3} [(k : κ) → Semiring (B k)] [(k : κ) → Algebra A (B k)] {k : κ} (s : B k →ₐ[A] A) (T : Type u_4) [CommSemiring T] [Algebra A T] (x : TensorProduct A T ((k : κ) → B k)) :
    ((s.comp (Pi.evalAlgHom A B k)).sectionBaseChange T) x = (s.sectionBaseChange T) ((Algebra.TensorProduct.piRight A T T B) x k)

    Base change of a section factoring through one coordinate of a product agrees with the base-changed section on that coordinate of the base-changed product.