noncomputable def map_one_proof.φ0 (K F : Type) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : GoodRep.CrossProduct ⋯ →ₗ[K] Module.End F K

Equations

• map_one_proof.φ0 K F = ((GoodRep.CrossProduct.x_AsBasis ⋯).constr F) fun (σ : K ≃ₐ[F] K) => σ.toLinearMap

noncomputable def map_one_proof.φ1 (K F : Type) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : GoodRep.CrossProduct ⋯ →ₗ[F] Module.End F K

Equations

• map_one_proof.φ1 K F = ↑F (map_one_proof.φ0 K F)

noncomputable def map_one_proof.φ2 (K F : Type) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : GoodRep.CrossProduct ⋯ →ₐ[F] Module.End F K

Equations

• map_one_proof.φ2 K F = AlgHom.ofLinearMap (map_one_proof.φ1 K F) ⋯ ⋯

noncomputable def map_one_proof.φ3 (K F : Type) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] [DecidableEq (K ≃ₐ[F] K)] : GoodRep.CrossProduct ⋯ ≃ₐ[F] Module.End F K

Equations

• map_one_proof.φ3 K F = AlgEquiv.ofBijective (map_one_proof.φ2 K F) ⋯

noncomputable def map_one_proof.φ4 (K F : Type) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] [DecidableEq (K ≃ₐ[F] K)] : GoodRep.CrossProduct ⋯ ≃ₐ[F] Matrix (Fin (Module.finrank F K)) (Fin (Module.finrank F K)) F

Equations

• map_one_proof.φ4 K F = (map_one_proof.φ3 K F).trans (LinearMap.toMatrixAlgEquiv (Module.finBasis F K))

theorem map_one_proof.map_one' (K F : Type) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] [DecidableEq (K ≃ₐ[F] K)] : RelativeBrGroup.fromTwoCocycles 0 = 1

theorem map_one_proof.fromSnd_zero (K F : Type) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] [DecidableEq (K ≃ₐ[F] K)] : RelativeBrGroup.fromSnd F K 0 = 1

theorem map_mul_proof.hαβ {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) : groupCohomology.IsMulTwoCocycle (α * β)

@[reducible, inline]

noncomputable abbrev map_mul_proof.S {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : Set (TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ))

Equations

• map_mul_proof.S hα hβ = Set.range fun (cba : K × GoodRep.CrossProduct hα × GoodRep.CrossProduct hβ) => (cba.1 • cba.2.1) ⊗ₜ[F] cba.2.2 - cba.2.1 ⊗ₜ[F] (cba.1 • cba.2.2)

@[simp]

theorem map_mul_proof.mem_S {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] (x : TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ)) : x ∈ S hα hβ ↔ ∃ (k : K) (a : GoodRep.CrossProduct hα) (b : GoodRep.CrossProduct hβ), x = (k • a) ⊗ₜ[F] b - a ⊗ₜ[F] (k • b)

@[reducible, inline]

noncomputable abbrev map_mul_proof.M {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : Type

Equations

• map_mul_proof.M hα hβ = (TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ) ⧸ Submodule.span F (map_mul_proof.S hα hβ))

instance map_mul_proof.instIsScalarTowerCrossProduct {K F : Type} [Field K] [Field F] [Algebra F K] {α : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : IsScalarTower K (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hα)

noncomputable def map_mul_proof.Aox_FB_smul_M_aux {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] (a' : GoodRep.CrossProduct hα) (b' : GoodRep.CrossProduct hβ) : M hα hβ →ₗ[F] M hα hβ

Equations

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

noncomputable def map_mul_proof.Aox_FB_smul_M {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ) →ₗ[F] M hα hβ →ₗ[F] M hα hβ

Equations

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

@[simp]

theorem map_mul_proof.Aox_FB_smul_M_op_tmul_smul_mk_tmul {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] (a' a : GoodRep.CrossProduct hα) (b' b : GoodRep.CrossProduct hβ) : ((Aox_FB_smul_M hα hβ) (a' ⊗ₜ[F] b')) (Submodule.Quotient.mk (a ⊗ₜ[F] b)) = Submodule.Quotient.mk ((a * a') ⊗ₜ[F] (b * b'))

noncomputable instance map_mul_proof.instSMulMulOppositeTensorProductCrossProductM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : SMul (TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ))ᵐᵒᵖ (M hα hβ)

Equations

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

@[simp]

theorem map_mul_proof.Aox_FB_op_tmul_smul_mk_tmul {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] (a' a : GoodRep.CrossProduct hα) (b' b : GoodRep.CrossProduct hβ) : MulOpposite.op (a' ⊗ₜ[F] b') • Submodule.Quotient.mk (a ⊗ₜ[F] b) = Submodule.Quotient.mk ((a * a') ⊗ₜ[F] (b * b'))

noncomputable instance map_mul_proof.instMulActionMulOppositeTensorProductCrossProductM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : MulAction (TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ))ᵐᵒᵖ (M hα hβ)

Equations

• map_mul_proof.instMulActionMulOppositeTensorProductCrossProductM hα hβ = MulAction.mk ⋯ ⋯

noncomputable instance map_mul_proof.instDistribMulActionMulOppositeTensorProductCrossProductM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : DistribMulAction (TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ))ᵐᵒᵖ (M hα hβ)

Equations

• map_mul_proof.instDistribMulActionMulOppositeTensorProductCrossProductM hα hβ = DistribMulAction.mk ⋯ ⋯

noncomputable instance map_mul_proof.instModuleMulOppositeTensorProductCrossProductM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : Module (TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ))ᵐᵒᵖ (M hα hβ)

Equations

• map_mul_proof.instModuleMulOppositeTensorProductCrossProductM hα hβ = Module.mk ⋯ ⋯

noncomputable def map_mul_proof.F_smul_mul_compatible {K F : Type} [Field K] [Field F] [Algebra F K] {α : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] (f : F) (a a' : GoodRep.CrossProduct hα) : f • a * a' = a * f • a'

Equations

• ⋯ = ⋯

noncomputable def map_mul_proof.C_smul_aux {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] (c : GoodRep.CrossProduct ⋯) : M hα hβ →ₗ[F] M hα hβ

Equations

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

theorem map_mul_proof.C_smul_aux_calc {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] (k : K) (σ : K ≃ₐ[F] K) (a : GoodRep.CrossProduct hα) (b : GoodRep.CrossProduct hβ) : (C_smul_aux hα hβ (k • (GoodRep.CrossProduct.x_AsBasis ⋯) σ)) (Submodule.Quotient.mk (a ⊗ₜ[F] b)) = Submodule.Quotient.mk ((k • (GoodRep.CrossProduct.x_AsBasis hα) σ * a) ⊗ₜ[F] ((GoodRep.CrossProduct.x_AsBasis hβ) σ * b))

noncomputable def map_mul_proof.C_smul {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : GoodRep.CrossProduct ⋯ →ₗ[F] M hα hβ →ₗ[F] M hα hβ

Equations

• map_mul_proof.C_smul hα hβ = { toFun := fun (c : GoodRep.CrossProduct ⋯) => map_mul_proof.C_smul_aux hα hβ c, map_add' := ⋯, map_smul' := ⋯ }

noncomputable instance map_mul_proof.instSMulCrossProductM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : SMul (GoodRep.CrossProduct ⋯) (M hα hβ)

Equations

• map_mul_proof.instSMulCrossProductM hα hβ = { smul := fun (c : GoodRep.CrossProduct ⋯) (x : map_mul_proof.M hα hβ) => ((map_mul_proof.C_smul hα hβ) c) x }

theorem map_mul_proof.C_smul_calc {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] (k : K) (σ : K ≃ₐ[F] K) (a : GoodRep.CrossProduct hα) (b : GoodRep.CrossProduct hβ) : (k • (GoodRep.CrossProduct.x_AsBasis ⋯) σ) • Submodule.Quotient.mk (a ⊗ₜ[F] b) = Submodule.Quotient.mk ((k • (GoodRep.CrossProduct.x_AsBasis hα) σ * a) ⊗ₜ[F] ((GoodRep.CrossProduct.x_AsBasis hβ) σ * b))

noncomputable instance map_mul_proof.instMulActionCrossProductM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : MulAction (GoodRep.CrossProduct ⋯) (M hα hβ)

Equations

• map_mul_proof.instMulActionCrossProductM hα hβ = MulAction.mk ⋯ ⋯

noncomputable instance map_mul_proof.instDistribMulActionCrossProductM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : DistribMulAction (GoodRep.CrossProduct ⋯) (M hα hβ)

Equations

• map_mul_proof.instDistribMulActionCrossProductM hα hβ = DistribMulAction.mk ⋯ ⋯

noncomputable instance map_mul_proof.instModuleCrossProductM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : Module (GoodRep.CrossProduct ⋯) (M hα hβ)

Equations

• map_mul_proof.instModuleCrossProductM hα hβ = Module.mk ⋯ ⋯

instance map_mul_proof.instSMulCommClassMulOppositeTensorProductCrossProductM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : SMulCommClass (TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ))ᵐᵒᵖ (GoodRep.CrossProduct ⋯) (M hα hβ)

instance map_mul_proof.instIsScalarTowerCrossProductM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : IsScalarTower F (GoodRep.CrossProduct ⋯) (M hα hβ)

noncomputable instance map_mul_proof.instModuleM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : Module F (M hα hβ)

Equations

• map_mul_proof.instModuleM hα hβ = inferInstance

noncomputable def map_mul_proof.φ0 {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : (TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ))ᵐᵒᵖ →ₐ[F] Module.End (GoodRep.CrossProduct ⋯) (M hα hβ)

Equations

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

noncomputable def map_mul_proof.MtoAox_KB {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : M hα hβ →ₗ[F] TensorProduct K (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ)

Equations

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

noncomputable def map_mul_proof.Aox_KBToM_aux {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : TensorProduct K (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ) →+ M hα hβ

Equations

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

noncomputable def map_mul_proof.Aox_KBToM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : TensorProduct K (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ) →ₗ[F] M hα hβ

Equations

• map_mul_proof.Aox_KBToM hα hβ = { toFun := (↑(map_mul_proof.Aox_KBToM_aux hα hβ)).toFun, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def map_mul_proof.Aox_KBEquivM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : M hα hβ ≃ₗ[F] TensorProduct K (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ)

Equations

• map_mul_proof.Aox_KBEquivM hα hβ = LinearEquiv.ofLinear (map_mul_proof.MtoAox_KB hα hβ) (map_mul_proof.Aox_KBToM hα hβ) ⋯ ⋯

theorem map_mul_proof.M_F_dim {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module.finrank F (M hα hβ) = Module.finrank F K ^ 3

instance map_mul_proof.instFiniteDimensionalCrossProductOfIsGalois {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : FiniteDimensional F (GoodRep.CrossProduct ⋯)

instance map_mul_proof.instFiniteCrossProductMOfIsGalois {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module.Finite (GoodRep.CrossProduct ⋯) (M hα hβ)

theorem map_mul_proof.exists_simple_module_directSum {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : ∃ (S : Type) (x : AddCommGroup S) (x_1 : Module (GoodRep.CrossProduct ⋯) S) (_ : IsSimpleModule (GoodRep.CrossProduct ⋯) S) (ι : Type) (x_3 : Fintype ι), Nonempty (GoodRep.CrossProduct ⋯ ≃ₗ[GoodRep.CrossProduct ⋯] ι →₀ S)

noncomputable def map_mul_proof.simpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Type

Equations

• map_mul_proof.simpleMod hα hβ = ⋯.choose

noncomputable instance map_mul_proof.instAddCommGroupSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : AddCommGroup (simpleMod hα hβ)

Equations

• map_mul_proof.instAddCommGroupSimpleMod hα hβ = ⋯.choose

noncomputable instance map_mul_proof.instModuleCrossProductSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module (GoodRep.CrossProduct ⋯) (simpleMod hα hβ)

Equations

• map_mul_proof.instModuleCrossProductSimpleMod hα hβ = ⋯.choose

noncomputable instance map_mul_proof.instModuleSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module F (simpleMod hα hβ)

Equations

• map_mul_proof.instModuleSimpleMod hα hβ = Module.compHom (map_mul_proof.simpleMod hα hβ) (algebraMap F (GoodRep.CrossProduct ⋯))

instance map_mul_proof.instIsSimpleModuleCrossProductSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : IsSimpleModule (GoodRep.CrossProduct ⋯) (simpleMod hα hβ)

noncomputable def map_mul_proof.indexingSet {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Type

Equations

• map_mul_proof.indexingSet hα hβ = ⋯.choose

noncomputable instance map_mul_proof.instFintypeIndexingSet {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Fintype (indexingSet hα hβ)

Equations

• map_mul_proof.instFintypeIndexingSet hα hβ = ⋯.choose

noncomputable def map_mul_proof.isoιSM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : GoodRep.CrossProduct ⋯ ≃ₗ[GoodRep.CrossProduct ⋯] indexingSet hα hβ →₀ simpleMod hα hβ

Equations

• map_mul_proof.isoιSM hα hβ = ⋯.some

instance map_mul_proof.instNonemptyIndexingSet {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Nonempty (indexingSet hα hβ)

instance map_mul_proof.instNeZeroNatCardIndexingSet {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : NeZero (Fintype.card (indexingSet hα hβ))

noncomputable def map_mul_proof.isoιSMPow {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : GoodRep.CrossProduct ⋯ ≃ₗ[GoodRep.CrossProduct ⋯] indexingSet hα hβ → simpleMod hα hβ

Equations

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

noncomputable def map_mul_proof.isoιSMPow' {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : GoodRep.CrossProduct ⋯ ≃ₗ[GoodRep.CrossProduct ⋯] Fin (Fintype.card (indexingSet hα hβ)) → simpleMod hα hβ

Equations

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

instance map_mul_proof.instCompatibleSMulMFinsuppIndexingSetSimpleModCrossProduct {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : LinearMap.CompatibleSMul (M hα hβ) (indexingSet hα hβ →₀ simpleMod hα hβ) F (GoodRep.CrossProduct ⋯)

instance map_mul_proof.instIsScalarTowerCrossProductSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : IsScalarTower F (GoodRep.CrossProduct ⋯) (simpleMod hα hβ)

instance map_mul_proof.instFiniteCrossProductFinsuppIndexingSetSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module.Finite (GoodRep.CrossProduct ⋯) (indexingSet hα hβ →₀ simpleMod hα hβ)

instance map_mul_proof.instFiniteFinsuppIndexingSetSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module.Finite F (indexingSet hα hβ →₀ simpleMod hα hβ)

instance map_mul_proof.instSMulCommClassCrossProductSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : SMulCommClass (GoodRep.CrossProduct ⋯) F (simpleMod hα hβ)

noncomputable instance map_mul_proof.instDivisionRingEndCrossProductSimpleModOfDecidableEq {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] [DecidableEq (Module.End (GoodRep.CrossProduct ⋯) (simpleMod hα hβ))] : DivisionRing (Module.End (GoodRep.CrossProduct ⋯) (simpleMod hα hβ))

Equations

• map_mul_proof.instDivisionRingEndCrossProductSimpleModOfDecidableEq hα hβ = Module.End.divisionRing

noncomputable instance map_mul_proof.instAlgebraEndCrossProductSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Algebra F (Module.End (GoodRep.CrossProduct ⋯) (simpleMod hα hβ))

Equations

• map_mul_proof.instAlgebraEndCrossProductSimpleMod hα hβ = Module.End.instAlgebra F (GoodRep.CrossProduct ⋯) (map_mul_proof.simpleMod hα hβ)

noncomputable def map_mul_proof.isoDagger {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] (m : ℕ) [NeZero m] : Module.End (GoodRep.CrossProduct ⋯) (Fin m → simpleMod hα hβ) ≃ₐ[F] Matrix (Fin m) (Fin m) (Module.End (GoodRep.CrossProduct ⋯) (simpleMod hα hβ))

Equations

• map_mul_proof.isoDagger hα hβ m = { toEquiv := (endPowEquivMatrix (GoodRep.CrossProduct ⋯) (map_mul_proof.simpleMod hα hβ) m).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

noncomputable def map_mul_proof.mopEquivEnd' {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] : (GoodRep.CrossProduct ⋯)ᵐᵒᵖ ≃ₐ[F] Module.End (GoodRep.CrossProduct ⋯) (GoodRep.CrossProduct ⋯)

Equations

• map_mul_proof.mopEquivEnd' hα hβ = AlgEquiv.ofRingEquiv ⋯

noncomputable def map_mul_proof.C_iso_aux {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : (GoodRep.CrossProduct ⋯)ᵐᵒᵖ ≃ₐ[F] Module.End (GoodRep.CrossProduct ⋯) (Fin (Fintype.card (indexingSet hα hβ)) → simpleMod hα hβ)

Equations

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

noncomputable def map_mul_proof.C_iso_aux' {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : (GoodRep.CrossProduct ⋯)ᵐᵒᵖ ≃ₐ[F] Matrix (Fin (Fintype.card (indexingSet hα hβ))) (Fin (Fintype.card (indexingSet hα hβ))) (Module.End (GoodRep.CrossProduct ⋯) (simpleMod hα hβ))

Equations

• map_mul_proof.C_iso_aux' hα hβ = (map_mul_proof.C_iso_aux hα hβ).trans (map_mul_proof.isoDagger hα hβ (Fintype.card (map_mul_proof.indexingSet hα hβ)))

theorem map_mul_proof.dim_endCSM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module.finrank F K ^ 2 = Fintype.card (indexingSet hα hβ) ^ 2 * Module.finrank F (Module.End (GoodRep.CrossProduct ⋯) (simpleMod hα hβ))

noncomputable def map_mul_proof.C_iso_aux'' {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : GoodRep.CrossProduct ⋯ ≃ₐ[F] (Matrix (Fin (Fintype.card (indexingSet hα hβ))) (Fin (Fintype.card (indexingSet hα hβ))) (Module.End (GoodRep.CrossProduct ⋯) (simpleMod hα hβ)))ᵐᵒᵖ

Equations

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

noncomputable def map_mul_proof.C_iso {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : GoodRep.CrossProduct ⋯ ≃ₐ[F] Matrix (Fin (Fintype.card (indexingSet hα hβ))) (Fin (Fintype.card (indexingSet hα hβ))) (Module.End (GoodRep.CrossProduct ⋯) (simpleMod hα hβ))ᵐᵒᵖ

Equations

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

theorem map_mul_proof.M_directSum {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : ∃ (ιM : Type) (x : Fintype ιM), Nonempty (M hα hβ ≃ₗ[GoodRep.CrossProduct ⋯] ιM →₀ simpleMod hα hβ)

noncomputable def map_mul_proof.indexingSetM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Type

Equations

• map_mul_proof.indexingSetM hα hβ = ⋯.choose

noncomputable instance map_mul_proof.instFintypeIndexingSetM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Fintype (indexingSetM hα hβ)

Equations

• map_mul_proof.instFintypeIndexingSetM hα hβ = ⋯.choose

noncomputable def map_mul_proof.M_iso_directSum {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : M hα hβ ≃ₗ[GoodRep.CrossProduct ⋯] indexingSetM hα hβ →₀ simpleMod hα hβ

Equations

• map_mul_proof.M_iso_directSum hα hβ = ⋯.some

instance map_mul_proof.instFiniteCrossProductSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module.Finite (GoodRep.CrossProduct ⋯) (simpleMod hα hβ)

instance map_mul_proof.instFiniteSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module.Finite F (simpleMod hα hβ)

theorem map_mul_proof.SM_F_dim {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Fintype.card (indexingSet hα hβ) * Module.finrank F (simpleMod hα hβ) = Module.finrank F K ^ 2

instance map_mul_proof.instFiniteCrossProductFinsuppFinHMulNatCardIndexingSetFinrankSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module.Finite (GoodRep.CrossProduct ⋯) (Fin (Fintype.card (indexingSet hα hβ) * Module.finrank F K) →₀ simpleMod hα hβ)

instance map_mul_proof.instFiniteCrossProductForallFinHMulNatCardIndexingSetFinrankSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module.Finite (GoodRep.CrossProduct ⋯) (Fin (Fintype.card (indexingSet hα hβ) * Module.finrank F K) → simpleMod hα hβ)

theorem map_mul_proof.M_iso_powAux {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Nonempty (M hα hβ ≃ₗ[GoodRep.CrossProduct ⋯] Fin (Module.finrank F K * Fintype.card (indexingSet hα hβ)) → simpleMod hα hβ)

noncomputable def map_mul_proof.M_iso_pow {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : M hα hβ ≃ₗ[GoodRep.CrossProduct ⋯] Fin (Module.finrank F K * Fintype.card (indexingSet hα hβ)) → simpleMod hα hβ

Equations

• map_mul_proof.M_iso_pow hα hβ = ⋯.some

noncomputable def map_mul_proof.M_iso_pow' {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : M hα hβ ≃ₗ[F] Fin (Module.finrank F K * Fintype.card (indexingSet hα hβ)) → simpleMod hα hβ

Equations

• map_mul_proof.M_iso_pow' hα hβ = LinearEquiv.restrictScalars F (map_mul_proof.M_iso_pow hα hβ)

noncomputable def map_mul_proof.endCMIso {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module.End (GoodRep.CrossProduct ⋯) (M hα hβ) ≃ₐ[F] Module.End (GoodRep.CrossProduct ⋯) (Fin (Module.finrank F K * Fintype.card (indexingSet hα hβ)) → simpleMod hα hβ)

Equations

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

instance map_mul_proof.instNeZeroNatHMulFinrankCardIndexingSet {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : NeZero (Module.finrank F K * Fintype.card (indexingSet hα hβ))

noncomputable def map_mul_proof.endCMIso' {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module.End (GoodRep.CrossProduct ⋯) (M hα hβ) ≃ₐ[F] Matrix (Fin (Module.finrank F K * Fintype.card (indexingSet hα hβ))) (Fin (Module.finrank F K * Fintype.card (indexingSet hα hβ))) (Module.End (GoodRep.CrossProduct ⋯) (simpleMod hα hβ))

Equations

• map_mul_proof.endCMIso' hα hβ = (map_mul_proof.endCMIso hα hβ).trans (map_mul_proof.isoDagger hα hβ (Module.finrank F K * Fintype.card (map_mul_proof.indexingSet hα hβ)))

theorem map_mul_proof.dim_endCM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : Module.finrank F (Module.End (GoodRep.CrossProduct ⋯) (M hα hβ)) = Module.finrank F K ^ 4

noncomputable def map_mul_proof.φ1 {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : (TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ))ᵐᵒᵖ ≃ₐ[F] Module.End (GoodRep.CrossProduct ⋯) (M hα hβ)

Equations

• map_mul_proof.φ1 hα hβ = AlgEquiv.ofBijective (map_mul_proof.φ0 hα hβ) ⋯

noncomputable def map_mul_proof.φ2 {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ) ≃ₐ[F] (Module.End (GoodRep.CrossProduct ⋯) (M hα hβ))ᵐᵒᵖ

Equations

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

noncomputable def map_mul_proof.φ3 {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ) ≃ₐ[F] (Matrix (Fin (Module.finrank F K * Fintype.card (indexingSet hα hβ))) (Fin (Module.finrank F K * Fintype.card (indexingSet hα hβ))) (Module.End (GoodRep.CrossProduct ⋯) (simpleMod hα hβ)))ᵐᵒᵖ

Equations

• map_mul_proof.φ3 hα hβ = (map_mul_proof.φ2 hα hβ).trans (AlgEquiv.op (map_mul_proof.endCMIso' hα hβ))

noncomputable def map_mul_proof.φ4 {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ) ≃ₐ[F] Matrix (Fin (Module.finrank F K * Fintype.card (indexingSet hα hβ))) (Fin (Module.finrank F K * Fintype.card (indexingSet hα hβ))) (Module.End (GoodRep.CrossProduct ⋯) (simpleMod hα hβ))ᵐᵒᵖ

Equations

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

noncomputable instance map_mul_proof.instDivisionRingMulOppositeEndCrossProductSimpleModOfDecidableEq {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] [DecidableEq (Module.End (GoodRep.CrossProduct ⋯) (simpleMod hα hβ))] : DivisionRing (Module.End (GoodRep.CrossProduct ⋯) (simpleMod hα hβ))ᵐᵒᵖ

Equations

• map_mul_proof.instDivisionRingMulOppositeEndCrossProductSimpleModOfDecidableEq hα hβ = inferInstance

theorem map_mul_proof.isBrauerEquivalent {K F : Type} [Field K] [Field F] [Algebra F K] {α β : ((K ≃ₐ[F] K) × K ≃ₐ[F] K) → Kˣ} (hα : groupCohomology.IsMulTwoCocycle α) (hβ : groupCohomology.IsMulTwoCocycle β) [FiniteDimensional F K] [DecidableEq (K ≃ₐ[F] K)] [IsGalois F K] : IsBrauerEquivalent (CSA.mk (TensorProduct F (GoodRep.CrossProduct hα) (GoodRep.CrossProduct hβ))) (CSA.mk (GoodRep.CrossProduct ⋯))

noncomputable def RelativeBrGroup.fromSndAddMonoidHom (K F : Type) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] [DecidableEq (K ≃ₐ[F] K)] : groupCohomology.H2 (galAct F K) →+ Additive ↥(RelativeBrGroup K F)

Equations

• RelativeBrGroup.fromSndAddMonoidHom K F = { toFun := ⇑Additive.ofMul ∘ RelativeBrGroup.fromSnd F K, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RelativeBrGroup.fromSndAddMonoidHom_apply (K F : Type) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] [DecidableEq (K ≃ₐ[F] K)] (a✝ : groupCohomology.H2 (galAct F K)) : (fromSndAddMonoidHom K F) a✝ = (⇑Additive.ofMul ∘ fromSnd F K) a✝

noncomputable def RelativeBrGroup.toSndAddMonoidHom (K F : Type) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] [DecidableEq (K ≃ₐ[F] K)] : Additive ↥(RelativeBrGroup K F) →+ groupCohomology.H2 (galAct F K)

Equations

• RelativeBrGroup.toSndAddMonoidHom K F = { toFun := RelativeBrGroup.toSnd ∘ ⇑Additive.toMul, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def RelativeBrGroup.isoSnd (K F : Type) [Field K] [Field F] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] [DecidableEq (K ≃ₐ[F] K)] : Additive ↥(RelativeBrGroup K F) ≃+ groupCohomology.H2 (galAct F K)

Equations

• RelativeBrGroup.isoSnd K F = { toFun := (↑(RelativeBrGroup.toSndAddMonoidHom K F)).toFun, invFun := RelativeBrGroup.equivSnd.invFun, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }