Documentation

TauCeti.Algebra.CrossedProduct.TensorProduct

Tensor products of crossed-product algebras #

The pointwise product of two Galois 2-cocycles is again a 2-cocycle (TauCeti.TwoCocycle.instCommGroup). This file proves that its crossed product represents the product of the two original Brauer classes.

The algebra-level argument is the standard matrix stabilization. If c and d are cocycles of G = Aut_K(L), the two crossed products act by commuting monomial matrices over the crossed product for c * d. In row r, the first action is supported on the single column r * g; in column s, the second is supported on the single row h * s. The cocycle identity says that these are algebra maps and commute. They therefore induce

CrossedProduct c ⊗[K] CrossedProduct d ≃ₐ[K] Matrix G G (CrossedProduct (c * d)).

The equality of dimensions makes the induced injective map an equivalence. Reindexing by G ≃ Fin #G exhibits the tensor product as a matrix algebra over CrossedProduct (c * d), so the two sides have the same Brauer class.

Main results #

References #

source
@[instance_reducible]
noncomputable def TauCeti.CrossedProduct.instDecidableEqAlgEquiv {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] :
DecidableEq Gal(L/K)

Decidable equality on the finite Galois group, used to form its matrix algebra.

Equations
Instances For
    source
    noncomputable def TauCeti.CrossedProduct.tensorProductAlgEquivMatrix {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (c d : TwoCocycle K L) :
    TensorProduct K (CrossedProduct c) (CrossedProduct d) ≃ₐ[K] Matrix Gal(L/K) Gal(L/K) (CrossedProduct (c * d))

    The tensor product of the crossed products for c and d is a matrix algebra over the crossed product for their pointwise product.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.CrossedProduct.tensorProductAlgEquivMatrix_smul_basis_tmul_one_apply {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (c d : TwoCocycle K L) (σ : Gal(L/K)) (x : L) (ρ τ : Gal(L/K)) :
      (tensorProductAlgEquivMatrix c d) ((x • (basis c) σ) ⊗ₜ[K] 1) ρ τ = if τ = ρ * σ then (inc (c * d)) (ρ x * ↑(c.toFun ρ σ)) else 0

      The matrix of (x • u_σ) ⊗ 1 under tensorProductAlgEquivMatrix: row ρ is supported on the single column ρ * σ, where the entry is ρ(x) · c(ρ, σ).

      source
      @[simp]
      theorem TauCeti.CrossedProduct.tensorProductAlgEquivMatrix_one_tmul_smul_basis_apply {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (c d : TwoCocycle K L) (σ : Gal(L/K)) (y : L) (ρ τ : Gal(L/K)) :
      (tensorProductAlgEquivMatrix c d) (1 ⊗ₜ[K] (y • (basis d) σ)) ρ τ = if ρ = σ * τ then (inc (c * d)) (y * ↑(c.toFun σ τ)⁻¹) * (basis (c * d)) σ else 0

      The matrix of 1 ⊗ (y • u_σ) under tensorProductAlgEquivMatrix: column τ is supported on the single row σ * τ, where the entry is (y · c(σ, τ)⁻¹) · u_σ.

      source
      theorem TauCeti.BrauerGroup.crossedProductClass_mul_eq_mk_tensorProduct {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (c d : TwoCocycle K L) :
      crossedProductClass (c * d) = mk (CSA.tensorProduct (crossedProductCSA c) (crossedProductCSA d))

      The crossed product of the pointwise product of two Galois 2-cocycles is Brauer equivalent to the tensor product of the two crossed products. This is the universe-polymorphic form of crossedProductClass_mul, which can only be stated when L lives in the universe of K, the universe in which BrauerGroup carries its multiplication.

      source
      @[simp]
      theorem TauCeti.BrauerGroup.crossedProductClass_mul {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (c d : TwoCocycle K L) :
      crossedProductClass (c * d) = crossedProductClass c * crossedProductClass d

      Multiplication of crossed-product classes. The pointwise product of two Galois 2-cocycles presents the product of the Brauer classes presented by the two cocycles.