Crossed products are central simple

For a commutative semiring K, a K-algebra L and a 2-cocycle c of Aut_K(L) with values in Lˣ, this file proves that the crossed product (L, Aut_K(L), c) is a simple ring when L is a field, and that it is central over K when L has no zero divisors and every element of L fixed by Aut_K(L) comes from K (Algebra.IsInvariant), as is the case for a Galois extension of fields.

Both proofs compare coefficients in the L-basis u_σ:

• simplicity: a nonzero element a = ∑ a_σ u_σ of a two-sided ideal with at least two coefficients a_σ, a_ρ ≠ 0 gives the element a · x - ρ(x) · a = ∑ a_τ (τ(x) - ρ(x)) u_τ of the ideal, which for σ(x) ≠ ρ(x) is nonzero with a smaller support. An element of minimal support is therefore a single y · u_σ. Multiplying by u_{σ⁻¹} produces a nonzero element of the embedded coefficient ring, even when L is only a commutative ring without zero divisors. When L is a field, this element is a unit;
• centrality: a central element commutes with L, so all its coefficients off u_1 vanish because distinct automorphisms differ somewhere, and it commutes with every u_τ, so its remaining coefficient is fixed by Aut_K(L) and hence lies in K.

Main results

• TauCeti.CrossedProduct.exists_ne_zero_and_inc_mem: every nonzero two-sided ideal meets the embedded coefficient ring nontrivially when L has no zero divisors.
• TauCeti.CrossedProduct.instIsSimpleRing: the crossed product is a simple ring.
• TauCeti.CrossedProduct.instIsCentral: if the fixed points of Aut_K(L) on L come from K (for instance, if L/K is Galois), the crossed product is central over K.

References

• P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology (2006), §4.4.
• J.-P. Serre, Local Fields, GTM 67 (1979), Chapter X.

theorem TauCeti.CrossedProduct.exists_ne_zero_and_inc_mem {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [NoZeroDivisors L] [Algebra K L] (c : TwoCocycle K L) {I : TwoSidedIdeal (CrossedProduct c)} (hI : I ≠ ⊥) : ∃ (y : L), y ≠ 0 ∧ (inc c) y ∈ I

Every nonzero two-sided ideal of the crossed product contains a nonzero element of the embedded coefficient ring, provided the coefficient ring has no zero divisors.

instance TauCeti.CrossedProduct.instIsSimpleRing {K : Type u} [CommSemiring K] {L : Type v} [Field L] [Algebra K L] {c : TwoCocycle K L} : IsSimpleRing (CrossedProduct c)

The crossed product is a simple ring.

instance TauCeti.CrossedProduct.instIsCentral {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [NoZeroDivisors L] [Algebra K L] (c : TwoCocycle K L) [Algebra.IsInvariant K L (L ≃ₐ[K] L)] : Algebra.IsCentral K (CrossedProduct c)

The crossed product is central over K when every element of L fixed by Aut_K(L) comes from K; this holds for instance when L/K is a Galois extension of fields.