Crossed-product algebras of Galois 2-cocycles

Let K be a commutative semiring and L a commutative ring over K. A 2-cocycle c of Aut_K(L) with values in Lˣ is a function c(σ, τ) ∈ Lˣ of two automorphisms, stored curried as c.toFun σ τ, whose uncurried form Aut_K(L) × Aut_K(L) → Lˣ satisfies Mathlib's multiplicative cocycle identity groupCohomology.IsMulCocycle₂, which reads c(στ, ρ) · c(σ, τ) = σ(c(τ, ρ)) · c(σ, τρ) for the Galois action of Aut_K(L) on Lˣ. This is the inhomogeneous normalization of Gille–Szamuely §4.4 and Serre, Local Fields, Chapter X.

The crossed product (L, Aut_K(L), c) is the free L-module on symbols u_σ, one for each σ : L ≃ₐ[K] L, with the multiplication determined by L-linearity on the left and the two rules u_σ · x = σ(x) · u_σ and u_σ · u_τ = c(σ, τ) · u_{στ}. On basis multiples this is (x · u_σ) · (y · u_τ) = (x · σ(y) · c(σ, τ)) · u_{στ}, and associativity of this product is exactly the cocycle identity. The cocycle is not assumed normalized: the identity element is c(1, 1)⁻¹ · u_1, and L embeds by x ↦ (x · c(1, 1)⁻¹) · u_1.

An element is a wrapper around a finitely supported function Aut_K(L) →₀ L, its coordinates (CrossedProduct.basis c).repr in the L-basis u_σ, and the crossed product is a K-algebra. Over fields its Module.finrank is Module.finrank K L * Nat.card (Aut_K(L)); when L/K is finite Galois, this is the actual dimension [L : K]². It is not an L-algebra: L acts on the left by multiplication, but is not central unless the automorphism group is trivial.

Central simplicity of the crossed product of a finite Galois extension of fields is proved in TauCeti.Algebra.CrossedProduct.CentralSimple.

Main definitions

• TauCeti.TwoCocycle K L: the 2-cocycles of L ≃ₐ[K] L with values in Lˣ, a commutative group under pointwise multiplication (TauCeti.TwoCocycle.instCommGroup).
• TauCeti.TwoCocycle.comap f ι hf c: the inflation of c along a homomorphism f : Aut_K(M) → Aut_K(L) and an embedding ι : L →ₐ[K] M intertwining it.
• TauCeti.CrossedProduct c: the crossed-product ring of a cocycle c, with its K-algebra and left L-module structures.
• TauCeti.CrossedProduct.basis c: the L-basis u_σ of the crossed product.
• TauCeti.CrossedProduct.inc c: the embedding of L as a K-subalgebra.
• TauCeti.CrossedProduct.lift: the universal property, extending f : L →ₐ[K] R and elements u σ ∈ R satisfying the relations of the crossed product to a K-algebra homomorphism.

Main results

• TauCeti.CrossedProduct.smul_basis_mul_smul_basis: the multiplication table (x · u_σ) · (y · u_τ) = (x · σ(y) · c(σ, τ)) · u_{στ}.
• TauCeti.CrossedProduct.basis_mul_inc: u_σ · x = σ(x) · u_σ.
• TauCeti.CrossedProduct.basis_mul_basis: u_σ · u_τ = c(σ, τ) · u_{στ}.
• TauCeti.CrossedProduct.algHom_ext, TauCeti.CrossedProduct.lift_unique: a K-algebra homomorphism out of the crossed product is determined by its values on L and on the u_σ.
• TauCeti.CrossedProduct.finrank_eq_finrank_mul_card: over fields, the Module.finrank of the crossed product is Module.finrank K L * Nat.card (Aut_K(L)); and TauCeti.CrossedProduct.finrank_eq_finrank_sq: for a finite Galois extension its dimension is [L : 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.

structure TauCeti.TwoCocycle (K : Type u) [CommSemiring K] (L : Type v) [CommRing L] [Algebra K L] : Type v

A 2-cocycle of the automorphism group Aut_K(L) with values in the units of L: a function c(σ, τ) = c.toFun σ τ ∈ Lˣ whose uncurried form satisfies the multiplicative cocycle identity c(στ, ρ) · c(σ, τ) = σ(c(τ, ρ)) · c(σ, τρ) of groupCohomology.IsMulCocycle₂, for the Galois action of L ≃ₐ[K] L on Lˣ.

• toFun : (L ≃ₐ[K] L) → (L ≃ₐ[K] L) → Lˣ

  The underlying function (σ, τ) ↦ c(σ, τ), in curried form.

• isMulCocycle₂ : groupCohomology.IsMulCocycle₂ fun (p : (L ≃ₐ[K] L) × L ≃ₐ[K] L) => self.toFun p.1 p.2

  The cocycle identity, for the uncurried function (σ, τ) ↦ c(σ, τ).

theorem TauCeti.TwoCocycle.ext_iff {K : Type u} {inst✝ : CommSemiring K} {L : Type v} {inst✝¹ : CommRing L} {inst✝² : Algebra K L} {x y : TwoCocycle K L} : x = y ↔ x.toFun = y.toFun

theorem TauCeti.TwoCocycle.ext {K : Type u} {inst✝ : CommSemiring K} {L : Type v} {inst✝¹ : CommRing L} {inst✝² : Algebra K L} {x y : TwoCocycle K L} (toFun : x.toFun = y.toFun) : x = y

theorem TauCeti.TwoCocycle.map_toFun_mul_toFun {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) (σ τ ρ : L ≃ₐ[K] L) : σ ↑(c.toFun τ ρ) * ↑(c.toFun σ (τ * ρ)) = ↑(c.toFun σ τ) * ↑(c.toFun (σ * τ) ρ)

The cocycle identity σ(c(τ, ρ)) · c(σ, τρ) = c(σ, τ) · c(στ, ρ), read in L.

@[simp]

theorem TauCeti.TwoCocycle.toFun_one_left {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) (σ : L ≃ₐ[K] L) : c.toFun 1 σ = c.toFun 1 1

c(1, σ) = c(1, 1), Mathlib's groupCohomology.map_one_fst_of_isMulCocycle₂ for a 2-cocycle.

theorem TauCeti.TwoCocycle.toFun_one_right {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) (σ : L ≃ₐ[K] L) : ↑(c.toFun σ 1) = σ ↑(c.toFun 1 1)

c(σ, 1) = σ(c(1, 1)), Mathlib's groupCohomology.map_one_snd_of_isMulCocycle₂ read in L through the Galois action. Not a simp lemma: at σ = 1 its left-hand side c(1, 1) reappears inside its right-hand side, so simp would loop.

The pointwise group of 2-cocycles

@[instance_reducible]

instance TauCeti.TwoCocycle.instOne {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] : One (TwoCocycle K L)

The trivial 2-cocycle, constantly 1.

Equations

• TauCeti.TwoCocycle.instOne = { one := { toFun := fun (x x_1 : L ≃ₐ[K] L) => 1, isMulCocycle₂ := ⋯ } }

@[instance_reducible]

instance TauCeti.TwoCocycle.instMul {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] : Mul (TwoCocycle K L)

The pointwise product (c · d)(σ, τ) = c(σ, τ) · d(σ, τ) of two 2-cocycles.

Equations

• TauCeti.TwoCocycle.instMul = { mul := fun (c d : TauCeti.TwoCocycle K L) => { toFun := fun (σ τ : L ≃ₐ[K] L) => c.toFun σ τ * d.toFun σ τ, isMulCocycle₂ := ⋯ } }

@[instance_reducible]

instance TauCeti.TwoCocycle.instInv {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] : Inv (TwoCocycle K L)

The pointwise inverse c⁻¹(σ, τ) = c(σ, τ)⁻¹ of a 2-cocycle.

Equations

• TauCeti.TwoCocycle.instInv = { inv := fun (c : TauCeti.TwoCocycle K L) => { toFun := fun (σ τ : L ≃ₐ[K] L) => (c.toFun σ τ)⁻¹, isMulCocycle₂ := ⋯ } }

@[instance_reducible]

instance TauCeti.TwoCocycle.instDiv {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] : Div (TwoCocycle K L)

The pointwise quotient (c / d)(σ, τ) = c(σ, τ) / d(σ, τ) of two 2-cocycles.

Equations

• TauCeti.TwoCocycle.instDiv = { div := fun (c d : TauCeti.TwoCocycle K L) => { toFun := fun (σ τ : L ≃ₐ[K] L) => c.toFun σ τ / d.toFun σ τ, isMulCocycle₂ := ⋯ } }

@[instance_reducible]

instance TauCeti.TwoCocycle.instPowNat {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] : Pow (TwoCocycle K L) ℕ

The pointwise power cⁿ(σ, τ) = c(σ, τ)ⁿ of a 2-cocycle.

Equations

• TauCeti.TwoCocycle.instPowNat = { pow := fun (c : TauCeti.TwoCocycle K L) (n : ℕ) => { toFun := fun (σ τ : L ≃ₐ[K] L) => c.toFun σ τ ^ n, isMulCocycle₂ := ⋯ } }

@[instance_reducible]

instance TauCeti.TwoCocycle.instPowInt {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] : Pow (TwoCocycle K L) ℤ

The pointwise integer power cⁿ(σ, τ) = c(σ, τ)ⁿ of a 2-cocycle.

Equations

• TauCeti.TwoCocycle.instPowInt = { pow := fun (c : TauCeti.TwoCocycle K L) (n : ℤ) => { toFun := fun (σ τ : L ≃ₐ[K] L) => c.toFun σ τ ^ n, isMulCocycle₂ := ⋯ } }

@[simp]

theorem TauCeti.TwoCocycle.toFun_one {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (σ τ : L ≃ₐ[K] L) : toFun 1 σ τ = 1

The trivial 2-cocycle is constantly 1.

@[simp]

theorem TauCeti.TwoCocycle.toFun_mul {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c d : TwoCocycle K L) (σ τ : L ≃ₐ[K] L) : (c * d).toFun σ τ = c.toFun σ τ * d.toFun σ τ

Multiplication of 2-cocycles is pointwise multiplication.

@[simp]

theorem TauCeti.TwoCocycle.toFun_inv {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) (σ τ : L ≃ₐ[K] L) : c⁻¹.toFun σ τ = (c.toFun σ τ)⁻¹

Inversion of 2-cocycles is pointwise inversion.

@[simp]

theorem TauCeti.TwoCocycle.toFun_div {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c d : TwoCocycle K L) (σ τ : L ≃ₐ[K] L) : (c / d).toFun σ τ = c.toFun σ τ / d.toFun σ τ

Division of 2-cocycles is pointwise division.

@[simp]

theorem TauCeti.TwoCocycle.toFun_pow {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) (n : ℕ) (σ τ : L ≃ₐ[K] L) : (c ^ n).toFun σ τ = c.toFun σ τ ^ n

Powers of 2-cocycles are pointwise powers.

@[simp]

theorem TauCeti.TwoCocycle.toFun_zpow {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) (n : ℤ) (σ τ : L ≃ₐ[K] L) : (c ^ n).toFun σ τ = c.toFun σ τ ^ n

Integer powers of 2-cocycles are pointwise integer powers.

@[instance_reducible]

instance TauCeti.TwoCocycle.instCommGroup {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] : CommGroup (TwoCocycle K L)

The 2-cocycles form a commutative group under pointwise multiplication, the group of 2-cocycles whose quotient by coboundaries is H²(Aut_K(L), Lˣ).

Equations

• TauCeti.TwoCocycle.instCommGroup = Function.Injective.commGroup TauCeti.TwoCocycle.toFun ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def TauCeti.TwoCocycle.comap {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {M : Type w} [CommRing M] [Algebra K M] (f : (M ≃ₐ[K] M) →* L ≃ₐ[K] L) (ι : L →ₐ[K] M) (hf : ∀ (g : M ≃ₐ[K] M) (x : L), ι ((f g) x) = g (ι x)) (c : TwoCocycle K L) : TwoCocycle K M

The inflation of a 2-cocycle c of Aut_K(L) along a compatible pair: a homomorphism f : Aut_K(M) → Aut_K(L) and an embedding ι : L → M intertwining it, ι (f g x) = g (ι x). Its values are (g, g') ↦ ι (c (f g, f g')); the intertwining hypothesis is what makes this a cocycle.

Equations

• TauCeti.TwoCocycle.comap f ι hf c = { toFun := fun (g g' : M ≃ₐ[K] M) => (Units.map ↑ι) (c.toFun (f g) (f g')), isMulCocycle₂ := ⋯ }

@[simp]

theorem TauCeti.TwoCocycle.comap_toFun {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) {M : Type w} [CommRing M] [Algebra K M] (f : (M ≃ₐ[K] M) →* L ≃ₐ[K] L) (ι : L →ₐ[K] M) (hf : ∀ (g : M ≃ₐ[K] M) (x : L), ι ((f g) x) = g (ι x)) (g g' : M ≃ₐ[K] M) : (comap f ι hf c).toFun g g' = (Units.map ↑ι) (c.toFun (f g) (f g'))

The defining equation of the inflated cocycle, (c.comap f ι hf)(g, g') = ι (c (f g, f g')), as units.

@[simp]

theorem TauCeti.TwoCocycle.comap_one {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {M : Type w} [CommRing M] [Algebra K M] (f : (M ≃ₐ[K] M) →* L ≃ₐ[K] L) (ι : L →ₐ[K] M) (hf : ∀ (g : M ≃ₐ[K] M) (x : L), ι ((f g) x) = g (ι x)) : comap f ι hf 1 = 1

Inflation of the trivial 2-cocycle is trivial.

@[simp]

theorem TauCeti.TwoCocycle.comap_mul {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) {M : Type w} [CommRing M] [Algebra K M] (f : (M ≃ₐ[K] M) →* L ≃ₐ[K] L) (ι : L →ₐ[K] M) (hf : ∀ (g : M ≃ₐ[K] M) (x : L), ι ((f g) x) = g (ι x)) (d : TwoCocycle K L) : comap f ι hf (c * d) = comap f ι hf c * comap f ι hf d

Inflation is multiplicative.

@[simp]

theorem TauCeti.TwoCocycle.comap_inv {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) {M : Type w} [CommRing M] [Algebra K M] (f : (M ≃ₐ[K] M) →* L ≃ₐ[K] L) (ι : L →ₐ[K] M) (hf : ∀ (g : M ≃ₐ[K] M) (x : L), ι ((f g) x) = g (ι x)) : comap f ι hf c⁻¹ = (comap f ι hf c)⁻¹

Inflation commutes with inversion.

@[simp]

theorem TauCeti.TwoCocycle.comap_div {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) {M : Type w} [CommRing M] [Algebra K M] (f : (M ≃ₐ[K] M) →* L ≃ₐ[K] L) (ι : L →ₐ[K] M) (hf : ∀ (g : M ≃ₐ[K] M) (x : L), ι ((f g) x) = g (ι x)) (d : TwoCocycle K L) : comap f ι hf (c / d) = comap f ι hf c / comap f ι hf d

Inflation commutes with division.

@[simp]

theorem TauCeti.TwoCocycle.comap_pow {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) {M : Type w} [CommRing M] [Algebra K M] (f : (M ≃ₐ[K] M) →* L ≃ₐ[K] L) (ι : L →ₐ[K] M) (hf : ∀ (g : M ≃ₐ[K] M) (x : L), ι ((f g) x) = g (ι x)) (n : ℕ) : comap f ι hf (c ^ n) = comap f ι hf c ^ n

Inflation commutes with natural powers.

@[simp]

theorem TauCeti.TwoCocycle.comap_zpow {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) {M : Type w} [CommRing M] [Algebra K M] (f : (M ≃ₐ[K] M) →* L ≃ₐ[K] L) (ι : L →ₐ[K] M) (hf : ∀ (g : M ≃ₐ[K] M) (x : L), ι ((f g) x) = g (ι x)) (n : ℤ) : comap f ι hf (c ^ n) = comap f ι hf c ^ n

Inflation commutes with integer powers.

structure TauCeti.CrossedProduct {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) : Type v

The crossed-product algebra (L, Aut_K(L), c) of a 2-cocycle c: the free L-module on symbols u_σ, one for each σ : L ≃ₐ[K] L, with the multiplication (x · u_σ) · (y · u_τ) = (x · σ(y) · c(σ, τ)) · u_{στ}. An element is a wrapper around its coordinates Aut_K(L) →₀ L in the basis CrossedProduct.basis c; the cocycle is a parameter of the type so that the multiplication can be an instance.

• ofFinsupp :: (
• toFinsupp : (L ≃ₐ[K] L) →₀ L

  The coordinates σ ↦ a_σ of an element in the basis u_σ.

• )

theorem TauCeti.CrossedProduct.ext {K : Type u} {inst✝ : CommSemiring K} {L : Type v} {inst✝¹ : CommRing L} {inst✝² : Algebra K L} {c : TwoCocycle K L} {x y : CrossedProduct c} (toFinsupp : x.toFinsupp = y.toFinsupp) : x = y

theorem TauCeti.CrossedProduct.ext_iff {K : Type u} {inst✝ : CommSemiring K} {L : Type v} {inst✝¹ : CommRing L} {inst✝² : Algebra K L} {c : TwoCocycle K L} {x y : CrossedProduct c} : x = y ↔ x.toFinsupp = y.toFinsupp

@[instance_reducible]

noncomputable instance TauCeti.CrossedProduct.instAddCommGroup {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) : AddCommGroup (CrossedProduct c)

Equations

• TauCeti.CrossedProduct.instAddCommGroup c = { toFun := TauCeti.CrossedProduct.toFinsupp, invFun := TauCeti.CrossedProduct.ofFinsupp, left_inv := ⋯, right_inv := ⋯ }.addCommGroup

def TauCeti.CrossedProduct.equivFinsupp {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) : CrossedProduct c ≃+ ((L ≃ₐ[K] L) →₀ L)

The identification of the crossed product with its coordinates Aut_K(L) →₀ L as an additive group, forgetting the multiplication.

Equations

• TauCeti.CrossedProduct.equivFinsupp c = { toFun := TauCeti.CrossedProduct.toFinsupp, invFun := TauCeti.CrossedProduct.ofFinsupp, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[instance_reducible]

noncomputable instance TauCeti.CrossedProduct.instModule {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) : Module L (CrossedProduct c)

L acts on the crossed product by left multiplication; see CrossedProduct.smul_def.

Equations

• TauCeti.CrossedProduct.instModule c = AddEquiv.module L (TauCeti.CrossedProduct.equivFinsupp c)

@[instance_reducible]

noncomputable instance TauCeti.CrossedProduct.instModule_1 {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) : Module K (CrossedProduct c)

Equations

• TauCeti.CrossedProduct.instModule_1 c = AddEquiv.module K (TauCeti.CrossedProduct.equivFinsupp c)

instance TauCeti.CrossedProduct.instIsScalarTower {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) : IsScalarTower K L (CrossedProduct c)

noncomputable def TauCeti.CrossedProduct.basis {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) : Module.Basis (L ≃ₐ[K] L) L (CrossedProduct c)

The L-basis u_σ of the crossed product, indexed by L ≃ₐ[K] L.

Equations

• TauCeti.CrossedProduct.basis c = { repr := AddEquiv.linearEquiv L (TauCeti.CrossedProduct.equivFinsupp c) }

@[instance_reducible]

noncomputable instance TauCeti.CrossedProduct.instMul {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) : Mul (CrossedProduct c)

The multiplication of the crossed product, (∑ x_σ · u_σ) · (∑ y_τ · u_τ) = ∑ (x_σ · σ(y_τ) · c(σ, τ)) · u_{στ}.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance TauCeti.CrossedProduct.instOne {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) : One (CrossedProduct c)

The identity of the crossed product, c(1, 1)⁻¹ · u_1.

Equations

• TauCeti.CrossedProduct.instOne c = { one := (c.toFun 1 1)⁻¹ • (TauCeti.CrossedProduct.basis c) 1 }

theorem TauCeti.CrossedProduct.mul_def {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} (a b : CrossedProduct c) : a * b = ((basis c).repr a).sum fun (σ : L ≃ₐ[K] L) (x : L) => ((basis c).repr b).sum fun (τ : L ≃ₐ[K] L) (y : L) => (x * σ y * ↑(c.toFun σ τ)) • (basis c) (σ * τ)

The multiplication of the crossed product in coordinates.

theorem TauCeti.CrossedProduct.one_def {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) : 1 = ↑(c.toFun 1 1)⁻¹ • (basis c) 1

The identity of the crossed product is c(1, 1)⁻¹ · u_1.

@[simp]

theorem TauCeti.CrossedProduct.smul_basis_mul_smul_basis {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} (σ τ : L ≃ₐ[K] L) (x y : L) : x • (basis c) σ * y • (basis c) τ = (x * σ y * ↑(c.toFun σ τ)) • (basis c) (σ * τ)

The multiplication table of the crossed product: (x · u_σ) · (y · u_τ) = (x · σ(y) · c(σ, τ)) · u_{στ}.

theorem TauCeti.CrossedProduct.induction_on {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} {motive : CrossedProduct c → Prop} (a : CrossedProduct c) (zero : motive 0) (add : ∀ (a b : CrossedProduct c), motive a → motive b → motive (a + b)) (smul_basis : ∀ (σ : L ≃ₐ[K] L) (x : L), motive (x • (basis c) σ)) : motive a

Induction principle along the L-basis u_σ: a property of elements of the crossed product that holds for 0 and for every x · u_σ and is closed under addition holds everywhere.

@[instance_reducible]

noncomputable instance TauCeti.CrossedProduct.instNonUnitalNonAssocRing {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} : NonUnitalNonAssocRing (CrossedProduct c)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance TauCeti.CrossedProduct.instNonUnitalRing {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} : NonUnitalRing (CrossedProduct c)

Equations

• TauCeti.CrossedProduct.instNonUnitalRing = { toNonUnitalNonAssocRing := TauCeti.CrossedProduct.instNonUnitalNonAssocRing, mul_assoc := ⋯ }

@[instance_reducible]

noncomputable instance TauCeti.CrossedProduct.instNonAssocRing {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} : NonAssocRing (CrossedProduct c)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance TauCeti.CrossedProduct.instRing {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} : Ring (CrossedProduct c)

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.CrossedProduct.instIsScalarTower_1 {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} : IsScalarTower L (CrossedProduct c) (CrossedProduct c)

L acts on the crossed product by left multiplication: (x • a) * b = x • (a * b).

instance TauCeti.CrossedProduct.instSMulCommClass {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} : SMulCommClass K (CrossedProduct c) (CrossedProduct c)

Scalars from K commute with the multiplication of the crossed product, because the automorphisms σ are K-linear.

@[instance_reducible]

noncomputable instance TauCeti.CrossedProduct.instAlgebra {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} : Algebra K (CrossedProduct c)

The crossed product is a K-algebra.

Equations

• TauCeti.CrossedProduct.instAlgebra = Algebra.ofModule ⋯ ⋯

noncomputable def TauCeti.CrossedProduct.inc {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] (c : TwoCocycle K L) : L →ₐ[K] CrossedProduct c

The embedding x ↦ (x · c(1, 1)⁻¹) · u_1 of L into the crossed product, a homomorphism of K-algebras.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.CrossedProduct.inc_apply {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} (x : L) : (inc c) x = (x * ↑(c.toFun 1 1)⁻¹) • (basis c) 1

theorem TauCeti.CrossedProduct.smul_def {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} (x : L) (a : CrossedProduct c) : x • a = (inc c) x * a

Left multiplication by inc c x is the L-module structure.

theorem TauCeti.CrossedProduct.basis_one {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} : (basis c) 1 = (inc c) ↑(c.toFun 1 1)

u_1 = c(1, 1) · 1.

@[simp]

theorem TauCeti.CrossedProduct.basis_mul_inc {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} (σ : L ≃ₐ[K] L) (x : L) : (basis c) σ * (inc c) x = (inc c) (σ x) * (basis c) σ

The semilinearity rule u_σ · x = σ(x) · u_σ.

@[simp]

theorem TauCeti.CrossedProduct.basis_mul_basis {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} (σ τ : L ≃ₐ[K] L) : (basis c) σ * (basis c) τ = (inc c) ↑(c.toFun σ τ) * (basis c) (σ * τ)

The cocycle rule u_σ · u_τ = c(σ, τ) · u_{στ}.

@[simp]

theorem TauCeti.CrossedProduct.repr_mul_inc {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} (a : CrossedProduct c) (x : L) (σ : L ≃ₐ[K] L) : ((basis c).repr (a * (inc c) x)) σ = ((basis c).repr a) σ * σ x

Right multiplication by inc c x twists the σ-th coordinate by σ: (∑ a_σ · u_σ) · x = ∑ (a_σ · σ(x)) · u_σ.

noncomputable def TauCeti.CrossedProduct.lift {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} {R : Type u_1} [Semiring R] [Algebra K R] (f : L →ₐ[K] R) (u : (L ≃ₐ[K] L) → R) (hf : ∀ (σ : L ≃ₐ[K] L) (x : L), u σ * f x = f (σ x) * u σ) (hu : ∀ (σ τ : L ≃ₐ[K] L), u σ * u τ = f ↑(c.toFun σ τ) * u (σ * τ)) (hu₁ : u 1 = f ↑(c.toFun 1 1)) : CrossedProduct c →ₐ[K] R

The universal property of the crossed product: a K-algebra homomorphism f : L → R together with elements u σ ∈ R satisfying u σ · f(x) = f(σ x) · u σ, u σ · u τ = f(c(σ, τ)) · u (στ) and u 1 = f(c(1, 1)) extends to the K-algebra homomorphism x · u_σ ↦ f(x) · u σ out of CrossedProduct c. The last condition is basis_one; without it u = 0 would satisfy the first two.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.CrossedProduct.lift_smul_basis {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} {R : Type u_1} [Semiring R] [Algebra K R] (f : L →ₐ[K] R) (u : (L ≃ₐ[K] L) → R) (hf : ∀ (σ : L ≃ₐ[K] L) (x : L), u σ * f x = f (σ x) * u σ) (hu : ∀ (σ τ : L ≃ₐ[K] L), u σ * u τ = f ↑(c.toFun σ τ) * u (σ * τ)) (hu₁ : u 1 = f ↑(c.toFun 1 1)) (σ : L ≃ₐ[K] L) (x : L) : (lift f u hf hu hu₁) (x • (basis c) σ) = f x * u σ

CrossedProduct.lift sends x · u_σ to f(x) · u σ.

@[simp]

theorem TauCeti.CrossedProduct.lift_basis {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} {R : Type u_1} [Semiring R] [Algebra K R] (f : L →ₐ[K] R) (u : (L ≃ₐ[K] L) → R) (hf : ∀ (σ : L ≃ₐ[K] L) (x : L), u σ * f x = f (σ x) * u σ) (hu : ∀ (σ τ : L ≃ₐ[K] L), u σ * u τ = f ↑(c.toFun σ τ) * u (σ * τ)) (hu₁ : u 1 = f ↑(c.toFun 1 1)) (σ : L ≃ₐ[K] L) : (lift f u hf hu hu₁) ((basis c) σ) = u σ

CrossedProduct.lift sends the basis element u_σ to u σ.

@[simp]

theorem TauCeti.CrossedProduct.lift_inc {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} {R : Type u_1} [Semiring R] [Algebra K R] (f : L →ₐ[K] R) (u : (L ≃ₐ[K] L) → R) (hf : ∀ (σ : L ≃ₐ[K] L) (x : L), u σ * f x = f (σ x) * u σ) (hu : ∀ (σ τ : L ≃ₐ[K] L), u σ * u τ = f ↑(c.toFun σ τ) * u (σ * τ)) (hu₁ : u 1 = f ↑(c.toFun 1 1)) (x : L) : (lift f u hf hu hu₁) ((inc c) x) = f x

CrossedProduct.lift restricts to f on the copy inc c of L.

theorem TauCeti.CrossedProduct.algHom_ext {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} {R : Type u_1} [Semiring R] [Algebra K R] {F G : CrossedProduct c →ₐ[K] R} (hinc : ∀ (x : L), F ((inc c) x) = G ((inc c) x)) (hbasis : ∀ (σ : L ≃ₐ[K] L), F ((basis c) σ) = G ((basis c) σ)) : F = G

Uniqueness in the universal property: a K-algebra homomorphism out of CrossedProduct c is determined by its values on the copy inc c of L and on the basis elements u_σ.

theorem TauCeti.CrossedProduct.algHom_ext_iff {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} {R : Type u_1} [Semiring R] [Algebra K R] {F G : CrossedProduct c →ₐ[K] R} : F = G ↔ (∀ (x : L), F ((inc c) x) = G ((inc c) x)) ∧ ∀ (σ : L ≃ₐ[K] L), F ((basis c) σ) = G ((basis c) σ)

theorem TauCeti.CrossedProduct.lift_unique {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} {R : Type u_1} [Semiring R] [Algebra K R] (f : L →ₐ[K] R) (u : (L ≃ₐ[K] L) → R) (hf : ∀ (σ : L ≃ₐ[K] L) (x : L), u σ * f x = f (σ x) * u σ) (hu : ∀ (σ τ : L ≃ₐ[K] L), u σ * u τ = f ↑(c.toFun σ τ) * u (σ * τ)) (hu₁ : u 1 = f ↑(c.toFun 1 1)) (F : CrossedProduct c →ₐ[K] R) (hinc : ∀ (x : L), F ((inc c) x) = f x) (hbasis : ∀ (σ : L ≃ₐ[K] L), F ((basis c) σ) = u σ) : F = lift f u hf hu hu₁

CrossedProduct.lift is the unique K-algebra homomorphism restricting to f on inc c and sending each u_σ to u σ.

instance TauCeti.CrossedProduct.instNontrivial {K : Type u} [CommSemiring K] {L : Type v} [CommRing L] [Algebra K L] {c : TwoCocycle K L} [Nontrivial L] : Nontrivial (CrossedProduct c)

A crossed product over a nontrivial ring L is nontrivial.

theorem TauCeti.CrossedProduct.finrank_eq_finrank_mul_card {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (c : TwoCocycle K L) : Module.finrank K (CrossedProduct c) = Module.finrank K L * Nat.card Gal(L/K)

The crossed product satisfies the natural-number identity Module.finrank K (CrossedProduct c) = Module.finrank K L * Nat.card (Aut_K(L)). Without finite-dimensionality, these are truncated invariants rather than cardinal dimensions.

theorem TauCeti.CrossedProduct.finrank_eq_finrank_sq {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (c : TwoCocycle K L) [FiniteDimensional K L] [IsGalois K L] : Module.finrank K (CrossedProduct c) = Module.finrank K L ^ 2

The crossed product of a finite Galois extension has dimension [L : K]², so it has degree [L : K] as a central simple algebra.

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