Cross product algebra

This file constructs the cross product algebra associated to a 2-cocycle of a field extension K / F and shows that it is a central simple F-algebra of dimension dim(K / F) ^ 2.

References

• [Advanced Algebra]

structure CrossProductAlgebra {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] (f : Gal(K/F) × Gal(K/F) → Kˣ) : Type u_4

The cross product algebra attached to a multiplicative two-cocycle on Gal(K, F).

• val : Gal(K/F) →₀ K

  The finitely supported coefficient function on the Galois group.

theorem CrossProductAlgebra.ext {F : Type u_3} {K : Type u_4} {inst✝ : Field F} {inst✝¹ : Field K} {inst✝² : Algebra F K} {f : Gal(K/F) × Gal(K/F) → Kˣ} {x y : CrossProductAlgebra f} (val : x.val = y.val) : x = y

theorem CrossProductAlgebra.ext_iff {F : Type u_3} {K : Type u_4} {inst✝ : Field F} {inst✝¹ : Field K} {inst✝² : Algebra F K} {f : Gal(K/F) × Gal(K/F) → Kˣ} {x y : CrossProductAlgebra f} : x = y ↔ x.val = y.val

theorem CrossProductAlgebra.val_injective {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : Function.Injective val

theorem CrossProductAlgebra.val_surjective {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : Function.Surjective val

theorem CrossProductAlgebra.val_bijective {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : Function.Bijective val

@[simp]

theorem CrossProductAlgebra.val_inj {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} {x y : CrossProductAlgebra f} : x.val = y.val ↔ x = y

theorem CrossProductAlgebra.forall {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} {P : CrossProductAlgebra f → Prop} : (∀ (x : CrossProductAlgebra f), P x) ↔ ∀ (x : Gal(K/F) →₀ K), P { val := x }

instance CrossProductAlgebra.instNontrivial {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : Nontrivial (CrossProductAlgebra f)

@[implicit_reducible]

noncomputable instance CrossProductAlgebra.instZero {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : Zero (CrossProductAlgebra f)

Equations

• CrossProductAlgebra.instZero = { zero := { val := 0 } }

@[implicit_reducible]

noncomputable instance CrossProductAlgebra.instAdd {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : Add (CrossProductAlgebra f)

Equations

• CrossProductAlgebra.instAdd = { add := fun (x y : CrossProductAlgebra f) => { val := x.val + y.val } }

@[implicit_reducible]

noncomputable instance CrossProductAlgebra.instNeg {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : Neg (CrossProductAlgebra f)

Equations

• CrossProductAlgebra.instNeg = { neg := fun (x : CrossProductAlgebra f) => { val := -x.val } }

@[implicit_reducible]

noncomputable instance CrossProductAlgebra.instSub {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : Sub (CrossProductAlgebra f)

Equations

• CrossProductAlgebra.instSub = { sub := fun (x y : CrossProductAlgebra f) => { val := x.val - y.val } }

@[implicit_reducible]

noncomputable instance CrossProductAlgebra.instSMulOfModule {R : Type u_1} {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Semiring R] [Module R K] : SMul R (CrossProductAlgebra f)

Equations

• CrossProductAlgebra.instSMulOfModule = { smul := fun (r : R) (x : CrossProductAlgebra f) => { val := r • x.val } }

@[simp]

theorem CrossProductAlgebra.val_zero {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : val 0 = 0

@[simp]

theorem CrossProductAlgebra.val_add {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} (x y : CrossProductAlgebra f) : (x + y).val = x.val + y.val

@[simp]

theorem CrossProductAlgebra.val_smul {R : Type u_1} {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Semiring R] [Module R K] (r : R) (x : CrossProductAlgebra f) : (r • x).val = r • x.val

@[simp]

theorem CrossProductAlgebra.val_neg {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} (x : CrossProductAlgebra f) : (-x).val = -x.val

@[simp]

theorem CrossProductAlgebra.val_sub {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} (x y : CrossProductAlgebra f) : (x - y).val = x.val - y.val

@[simp]

theorem CrossProductAlgebra.mk_zero {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : { val := 0 } = 0

@[simp]

theorem CrossProductAlgebra.mk_add_mk {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} (x y : Gal(K/F) →₀ K) : { val := x } + { val := y } = { val := x + y }

@[simp]

theorem CrossProductAlgebra.smul_mk {R : Type u_1} {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Semiring R] [Module R K] (r : R) (x : Gal(K/F) →₀ K) : r • { val := x } = { val := r • x }

@[simp]

theorem CrossProductAlgebra.neg_mk {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} (x : Gal(K/F) →₀ K) : -{ val := x } = { val := -x }

@[simp]

theorem CrossProductAlgebra.mk_sub_mk {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} (x y : Gal(K/F) →₀ K) : { val := x } - { val := y } = { val := x - y }

@[implicit_reducible]

noncomputable instance CrossProductAlgebra.addCommGroup {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : AddCommGroup (CrossProductAlgebra f)

Equations

• CrossProductAlgebra.addCommGroup = Function.Injective.addCommGroup CrossProductAlgebra.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def CrossProductAlgebra.valAddEquiv {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : CrossProductAlgebra f ≃+ (Gal(K/F) →₀ K)

The additive equivalence with finitely supported functions on the Galois group.

Equations

• CrossProductAlgebra.valAddEquiv = { toFun := CrossProductAlgebra.val, invFun := CrossProductAlgebra.mk, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem CrossProductAlgebra.valAddEquiv_apply {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} (self : CrossProductAlgebra f) : valAddEquiv self = self.val

@[simp]

theorem CrossProductAlgebra.valAddEquiv_symm_apply_val {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} (val : Gal(K/F) →₀ K) : (valAddEquiv.symm val).val = val

@[simp]

theorem CrossProductAlgebra.val_finsuppSum {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} {α : Type u_5} {M : Type u_6} [AddCommMonoid M] (g : α →₀ M) (h : α → M → CrossProductAlgebra f) : (g.sum h).val = g.sum fun (a : α) (m : M) => (h a m).val

@[implicit_reducible]

noncomputable instance CrossProductAlgebra.instModule {R : Type u_1} {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Semiring R] [Module R K] : Module R (CrossProductAlgebra f)

Equations

• CrossProductAlgebra.instModule = Function.Injective.module R CrossProductAlgebra.valAddEquiv.toAddMonoidHom ⋯ ⋯

instance CrossProductAlgebra.instIsScalarTower {R : Type u_1} {S : Type u_2} {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Semiring R] [Semiring S] [Module R K] [Module S K] [Module R S] [IsScalarTower R S K] : IsScalarTower R S (CrossProductAlgebra f)

noncomputable def CrossProductAlgebra.valLinearEquiv {R : Type u_1} {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Semiring R] [Module R K] : CrossProductAlgebra f ≃ₗ[R] Gal(K/F) →₀ K

The linear equivalence with finitely supported functions on the Galois group.

Equations

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

@[simp]

theorem CrossProductAlgebra.valLinearEquiv_apply {R : Type u_1} {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Semiring R] [Module R K] (a✝ : CrossProductAlgebra f) : valLinearEquiv a✝ = valAddEquiv.toFun a✝

@[simp]

theorem CrossProductAlgebra.valLinearEquiv_symm_apply {R : Type u_1} {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Semiring R] [Module R K] (a✝ : Gal(K/F) →₀ K) : valLinearEquiv.symm a✝ = valAddEquiv.invFun a✝

noncomputable def CrossProductAlgebra.basis {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : Module.Basis Gal(K/F) K (CrossProductAlgebra f)

The standard basis of the cross product algebra over K.

Equations

• CrossProductAlgebra.basis = { repr := CrossProductAlgebra.valLinearEquiv }

@[simp]

theorem CrossProductAlgebra.basis_repr {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : basis.repr = valLinearEquiv

theorem CrossProductAlgebra.basis_val {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} (σ : Gal(K/F)) : (basis σ).val = Finsupp.single σ 1

theorem CrossProductAlgebra.mk_single_one {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} (σ : Gal(K/F)) : { val := Finsupp.single σ 1 } = basis σ

noncomputable def CrossProductAlgebra.mulLinearMap {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] (f : Gal(K/F) × Gal(K/F) → Kˣ) : (Gal(K/F) →₀ K) →ₗ[F] (Gal(K/F) →₀ K) →ₗ[F] Gal(K/F) →₀ K

The bilinear multiplication map on the underlying finitely supported functions.

Equations

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

@[simp]

theorem CrossProductAlgebra.mulLinearMap_single_single {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] (f : Gal(K/F) × Gal(K/F) → Kˣ) (c d : K) (σ τ : Gal(K/F)) : ((mulLinearMap f) (Finsupp.single σ c)) (Finsupp.single τ d) = Finsupp.single (σ * τ) (c * σ d * ↑(f (σ, τ)))

@[simp]

theorem CrossProductAlgebra.mulLinearMap_single_left_apply {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] (f : Gal(K/F) × Gal(K/F) → Kˣ) (c : K) (σ : Gal(K/F)) (x : Gal(K/F) →₀ K) (τ : Gal(K/F)) : (((mulLinearMap f) (Finsupp.single σ c)) x) τ = c * σ (x (σ⁻¹ * τ)) * ↑(f (σ, σ⁻¹ * τ))

@[simp]

theorem CrossProductAlgebra.mulLinearMap_single_right_apply {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] (f : Gal(K/F) × Gal(K/F) → Kˣ) (c : K) (σ : Gal(K/F)) (x : Gal(K/F) →₀ K) (τ : Gal(K/F)) : (((mulLinearMap f) x) (Finsupp.single σ c)) τ = x (τ * σ⁻¹) * τ (σ⁻¹ c) * ↑(f (τ * σ⁻¹, σ))

@[implicit_reducible]

noncomputable instance CrossProductAlgebra.instOne {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : One (CrossProductAlgebra f)

Equations

• CrossProductAlgebra.instOne = { one := { val := Finsupp.single 1 (↑(f (1, 1)))⁻¹ } }

@[implicit_reducible]

noncomputable instance CrossProductAlgebra.instMul {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : Mul (CrossProductAlgebra f)

Equations

• CrossProductAlgebra.instMul = { mul := fun (x y : CrossProductAlgebra f) => { val := ((CrossProductAlgebra.mulLinearMap f) x.val) y.val } }

theorem CrossProductAlgebra.one_def {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : 1 = { val := Finsupp.single 1 (↑(f (1, 1)))⁻¹ }

@[simp]

theorem CrossProductAlgebra.val_one {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} : val 1 = Finsupp.single 1 (↑(f (1, 1)))⁻¹

@[simp]

theorem CrossProductAlgebra.val_mul {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} (x y : CrossProductAlgebra f) : (x * y).val = ((mulLinearMap f) x.val) y.val

@[simp]

theorem CrossProductAlgebra.mk_mul_mk {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} (x y : Gal(K/F) →₀ K) : { val := x } * { val := y } = { val := ((mulLinearMap f) x) y }

@[implicit_reducible]

noncomputable instance CrossProductAlgebra.monoid {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] : Monoid (CrossProductAlgebra f)

Equations

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

@[implicit_reducible]

noncomputable instance CrossProductAlgebra.instRing {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] : Ring (CrossProductAlgebra f)

Equations

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

@[implicit_reducible]

noncomputable instance CrossProductAlgebra.algebra {R : Type u_1} {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] [CommSemiring R] [Algebra R F] [Module R K] [IsScalarTower R F K] : Algebra R (CrossProductAlgebra f)

Equations

• CrossProductAlgebra.algebra = Algebra.ofModule ⋯ ⋯

theorem CrossProductAlgebra.algebraMap_val {R : Type u_1} {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] [CommSemiring R] [Algebra R F] [Algebra R K] [IsScalarTower R F K] (r : R) : ((algebraMap R (CrossProductAlgebra f)) r).val = Finsupp.single 1 ((algebraMap R K) r * ↑(f (1, 1))⁻¹)

theorem CrossProductAlgebra.basis_smul_comm {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} (σ : Gal(K/F)) (k1 k2 : K) (x : CrossProductAlgebra f) : k1 • basis σ * k2 • x = σ k2 • k1 • basis σ * x

noncomputable def CrossProductAlgebra.incl {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] (f : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ f)] : K →ₐ[F] CrossProductAlgebra f

The inclusion from K into CrossProductAlgebra f.

Note that this does not make CrossProductAlgebra f into a K-algebra, because that would require incl k * x = x * incl k.

Equations

• CrossProductAlgebra.incl f = { toFun := fun (k : K) => k • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem CrossProductAlgebra.incl_apply {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] (f : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ f)] (k : K) : (incl f) k = k • 1

theorem CrossProductAlgebra.smul_eq_incl_mul {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] (k : K) (x : CrossProductAlgebra f) : k • x = (incl f) k * x

instance CrossProductAlgebra.instIsScalarTower_1 {R : Type u_1} {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] [CommSemiring R] [Algebra R K] : IsScalarTower R (CrossProductAlgebra f) (CrossProductAlgebra f)

noncomputable def CrossProductAlgebra.of {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] (f : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ f)] (σ : Gal(K/F)) : (CrossProductAlgebra f)ˣ

The canonical unit associated to an element of the Galois group.

Equations

• CrossProductAlgebra.of f σ = { val := { val := Finsupp.single σ 1 }, inv := { val := Finsupp.single σ⁻¹ (↑(f (σ⁻¹, σ))⁻¹ * ↑(f (1, 1))⁻¹) }, val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem CrossProductAlgebra.val_inv_of_val {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] (f : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ f)] (σ : Gal(K/F)) : (↑(of f σ)⁻¹).val = Finsupp.single σ⁻¹ (↑(f (σ⁻¹, σ))⁻¹ * ↑(f (1, 1))⁻¹)

@[simp]

theorem CrossProductAlgebra.val_of_val {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] (f : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ f)] (σ : Gal(K/F)) : (↑(of f σ)).val = Finsupp.single σ 1

theorem CrossProductAlgebra.basis_eq_of {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] (σ : Gal(K/F)) : basis σ = ↑(of f σ)

@[simp]

theorem CrossProductAlgebra.of_one {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] (f : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ f)] : ↑(of f 1) = (incl f) ↑(f (1, 1))

@[simp]

theorem CrossProductAlgebra.of_mul_of {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] (f : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ f)] (σ τ : Gal(K/F)) : ↑(of f σ) * ↑(of f τ) = (incl f) ↑(f (σ, τ)) * ↑(of f (σ * τ))

@[simp]

theorem CrossProductAlgebra.basis_mul_basis {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] (σ τ : Gal(K/F)) : basis σ * basis τ = (incl f) ↑(f (σ, τ)) * basis (σ * τ)

theorem CrossProductAlgebra.of_mul_incl {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] (σ : Gal(K/F)) (c : K) : ↑(of f σ) * (incl f) c = (incl f) (σ c) * ↑(of f σ)

theorem CrossProductAlgebra.sum_of {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] (x : CrossProductAlgebra f) : (x.val.sum fun (σ : Gal(K/F)) (c : K) => c • ↑(of f σ)) = x

theorem CrossProductAlgebra.of_conj {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] (σ : Gal(K/F)) (k : K) : ↑(of f σ) * (incl f) k * ↑(of f σ)⁻¹ = (incl f) (σ k)

Finite dimensionality

@[simp]

theorem CrossProductAlgebra.dim_eq_sq {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] [Module.Finite F K] [IsGalois F K] : Module.finrank F (CrossProductAlgebra f) = Module.finrank F K ^ 2

instance CrossProductAlgebra.instFinite {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] [Module.Finite F K] [IsGalois F K] : Module.Finite F (CrossProductAlgebra f)

Centrality

instance CrossProductAlgebra.instIsCentral {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] [Module.Finite F K] [IsGalois F K] : Algebra.IsCentral F (CrossProductAlgebra f)

Simplicity

instance CrossProductAlgebra.instIsSimpleRing {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] {f : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ f)] : IsSimpleRing (CrossProductAlgebra f)

The cross product algebra as a central simple algebra

noncomputable def CrossProductAlgebra.asCSA {F : Type u_3} {K : Type u_4} [Field F] [Field K] [Algebra F K] (f : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ f)] [Module.Finite F K] [IsGalois F K] : CSA F

The cross product algebra as a central simple algebra.

Equations

• CrossProductAlgebra.asCSA f = { toAlgCat := AlgCat.of F (CrossProductAlgebra f), isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ }