noncomputable def map_mul_proof.S {K F : Type} [Field K] [Field F] [Algebra F K] (α β : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] : Set (TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β))

Equations

• map_mul_proof.S α β = Set.range fun (x : K × CrossProductAlgebra α × CrossProductAlgebra β) => match x with | (k, a, b) => (k • a) ⊗ₜ[F] b - a ⊗ₜ[F] (k • b)

@[simp]

theorem map_mul_proof.mem_S {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] (x : TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β)) : x ∈ S α β ↔ ∃ (k : K) (a : CrossProductAlgebra α) (b : CrossProductAlgebra β), x = (k • a) ⊗ₜ[F] b - a ⊗ₜ[F] (k • b)

@[reducible]

noncomputable def map_mul_proof.M {K F : Type} [Field K] [Field F] [Algebra F K] (α β : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] : Type

Equations

• map_mul_proof.M α β = (TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β) ⧸ Submodule.span F (map_mul_proof.S α β))

noncomputable def map_mul_proof.Aox_FB_smul_M_aux {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] (a' : CrossProductAlgebra α) (b' : CrossProductAlgebra β) : M α β →ₗ[F] M α β

Equations

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

noncomputable def map_mul_proof.Aox_FB_smul_M_aux_aux {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] (a : CrossProductAlgebra α) : CrossProductAlgebra β →ₗ[F] M α β →ₗ[F] M α β

Equations

• map_mul_proof.Aox_FB_smul_M_aux_aux a = { toFun := fun (b : CrossProductAlgebra β) => map_mul_proof.Aox_FB_smul_M_aux a b, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def map_mul_proof.Aox_FB_smul_M {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] : TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β) →ₗ[F] M α β →ₗ[F] M α β

Equations

• map_mul_proof.Aox_FB_smul_M = TensorProduct.lift { toFun := map_mul_proof.Aox_FB_smul_M_aux_aux, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem map_mul_proof.Aox_FB_smul_M_op_tmul_smul_mk_tmul {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] (a' a : CrossProductAlgebra α) (b' b : CrossProductAlgebra β) : (Aox_FB_smul_M (a' ⊗ₜ[F] b')) (Submodule.Quotient.mk (a ⊗ₜ[F] b)) = Submodule.Quotient.mk ((a * a') ⊗ₜ[F] (b * b'))

@[implicit_reducible]

noncomputable instance map_mul_proof.instSMulMulOppositeTensorProductCrossProductAlgebraM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] : SMul (TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β))ᵐᵒᵖ (M α β)

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] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] (a' a : CrossProductAlgebra α) (b' b : CrossProductAlgebra β) : MulOpposite.op (a' ⊗ₜ[F] b') • Submodule.Quotient.mk (a ⊗ₜ[F] b) = Submodule.Quotient.mk ((a * a') ⊗ₜ[F] (b * b'))

@[implicit_reducible]

noncomputable instance map_mul_proof.instMulActionMulOppositeTensorProductCrossProductAlgebraM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] : MulAction (TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β))ᵐᵒᵖ (M α β)

Equations

• map_mul_proof.instMulActionMulOppositeTensorProductCrossProductAlgebraM = { toSMul := map_mul_proof.instSMulMulOppositeTensorProductCrossProductAlgebraM, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

noncomputable instance map_mul_proof.instDistribMulActionMulOppositeTensorProductCrossProductAlgebraM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] : DistribMulAction (TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β))ᵐᵒᵖ (M α β)

Equations

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

@[implicit_reducible]

noncomputable instance map_mul_proof.instModuleMulOppositeTensorProductCrossProductAlgebraM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] : Module (TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β))ᵐᵒᵖ (M α β)

Equations

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

theorem map_mul_proof.F_smul_mul_compatible {K F : Type} [Field K] [Field F] [Algebra F K] {α : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] (f : F) (a a' : CrossProductAlgebra α) : f • a * a' = a * f • a'

noncomputable def map_mul_proof.C_smul_aux {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] (c : CrossProductAlgebra (α * β)) : M α β →ₗ[F] M α β

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] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] (k : K) (σ : Gal(K/F)) (a : CrossProductAlgebra α) (b : CrossProductAlgebra β) : (C_smul_aux (k • CrossProductAlgebra.basis σ)) (Submodule.Quotient.mk (a ⊗ₜ[F] b)) = Submodule.Quotient.mk ((k • CrossProductAlgebra.basis σ * a) ⊗ₜ[F] (CrossProductAlgebra.basis σ * b))

noncomputable def map_mul_proof.C_smul {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] : CrossProductAlgebra (α * β) →ₗ[F] M α β →ₗ[F] M α β

Equations

• map_mul_proof.C_smul = { toFun := map_mul_proof.C_smul_aux, map_add' := ⋯, map_smul' := ⋯ }

@[implicit_reducible]

noncomputable instance map_mul_proof.instSMulCrossProductAlgebraHMulForallProdAlgEquivUnitsM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] : SMul (CrossProductAlgebra (α * β)) (M α β)

Equations

• map_mul_proof.instSMulCrossProductAlgebraHMulForallProdAlgEquivUnitsM = { smul := fun (c : CrossProductAlgebra (α * β)) (x : map_mul_proof.M α β) => (map_mul_proof.C_smul c) x }

theorem map_mul_proof.C_smul_def {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] (c : CrossProductAlgebra (α * β)) (x : M α β) : c • x = (C_smul c) x

theorem map_mul_proof.C_smul_calc {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] (k : K) (σ : Gal(K/F)) (a : CrossProductAlgebra α) (b : CrossProductAlgebra β) : (k • CrossProductAlgebra.basis σ) • Submodule.Quotient.mk (a ⊗ₜ[F] b) = Submodule.Quotient.mk ((k • CrossProductAlgebra.basis σ * a) ⊗ₜ[F] (CrossProductAlgebra.basis σ * b))

theorem map_mul_proof.C_mul_smul' {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] (x y : CrossProductAlgebra (α * β)) (ab : M α β) : (x * y) • ab = x • y • ab

@[implicit_reducible]

noncomputable instance map_mul_proof.instMulActionCrossProductAlgebraHMulForallProdAlgEquivUnitsM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] : MulAction (CrossProductAlgebra (α * β)) (M α β)

Equations

• map_mul_proof.instMulActionCrossProductAlgebraHMulForallProdAlgEquivUnitsM = { toSMul := map_mul_proof.instSMulCrossProductAlgebraHMulForallProdAlgEquivUnitsM, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

noncomputable instance map_mul_proof.instDistribMulActionCrossProductAlgebraHMulForallProdAlgEquivUnitsM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] : DistribMulAction (CrossProductAlgebra (α * β)) (M α β)

Equations

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

@[implicit_reducible]

noncomputable instance map_mul_proof.instModuleCrossProductAlgebraHMulForallProdAlgEquivUnitsM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] : Module (CrossProductAlgebra (α * β)) (M α β)

Equations

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

@[implicit_reducible]

noncomputable instance map_mul_proof.instSMulWithZeroMulOppositeTensorProductCrossProductAlgebraM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] : SMulWithZero (TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β))ᵐᵒᵖ (M α β)

Equations

• map_mul_proof.instSMulWithZeroMulOppositeTensorProductCrossProductAlgebraM = { toSMulZeroClass := DistribMulAction.toDistribSMul.toSMulZeroClass, zero_smul := ⋯ }

instance map_mul_proof.instSMulCommClassMulOppositeTensorProductCrossProductAlgebraHMulForallProdAlgEquivUnitsM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] : SMulCommClass (TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β))ᵐᵒᵖ (CrossProductAlgebra (α * β)) (M α β)

instance map_mul_proof.instIsScalarTowerCrossProductAlgebraHMulForallProdAlgEquivUnitsM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] : IsScalarTower F (CrossProductAlgebra (α * β)) (M α β)

noncomputable def map_mul_proof.φ0 {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] : (TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β))ᵐᵒᵖ →ₐ[F] Module.End (CrossProductAlgebra (α * β)) (M α β)

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] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] : M α β →ₗ[F] TensorProduct K (CrossProductAlgebra α) (CrossProductAlgebra β)

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] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] : TensorProduct K (CrossProductAlgebra α) (CrossProductAlgebra β) →+ M α β

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] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] : TensorProduct K (CrossProductAlgebra α) (CrossProductAlgebra β) →ₗ[F] M α β

Equations

• map_mul_proof.Aox_KBToM = { toFun := ⇑map_mul_proof.Aox_KBToM_aux, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def map_mul_proof.Aox_KBEquivM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] : M α β ≃ₗ[F] TensorProduct K (CrossProductAlgebra α) (CrossProductAlgebra β)

Equations

• map_mul_proof.Aox_KBEquivM = LinearEquiv.ofLinear map_mul_proof.MtoAox_KB map_mul_proof.Aox_KBToM ⋯ ⋯

theorem map_mul_proof.M_F_dim {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Module.finrank F (M α β) = Module.finrank F K ^ 3

instance map_mul_proof.instFiniteDimensionalCrossProductAlgebraHMulForallProdAlgEquivUnitsOfIsGalois {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : FiniteDimensional F (CrossProductAlgebra (α * β))

instance map_mul_proof.instFiniteCrossProductAlgebraHMulForallProdAlgEquivUnitsMOfIsGalois {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Module.Finite (CrossProductAlgebra (α * β)) (M α β)

theorem map_mul_proof.exists_simple_module_directSum {K F : Type} [Field K] [Field F] [Algebra F K] (α β : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : ∃ (S : Type) (x : AddCommGroup S) (x_1 : Module (CrossProductAlgebra (α * β)) S) (_ : IsSimpleModule (CrossProductAlgebra (α * β)) S) (ι : Type) (x_3 : Fintype ι), Nonempty (CrossProductAlgebra (α * β) ≃ₗ[CrossProductAlgebra (α * β)] ι →₀ S)

noncomputable def map_mul_proof.SimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] (α β : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Type

Equations

• map_mul_proof.SimpleMod α β = ⋯.choose

@[implicit_reducible]

noncomputable instance map_mul_proof.instAddCommGroupSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : AddCommGroup (SimpleMod α β)

Equations

• map_mul_proof.instAddCommGroupSimpleMod = ⋯.choose

@[implicit_reducible]

noncomputable instance map_mul_proof.instModuleCrossProductAlgebraHMulForallProdAlgEquivUnitsSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Module (CrossProductAlgebra (α * β)) (SimpleMod α β)

Equations

• map_mul_proof.instModuleCrossProductAlgebraHMulForallProdAlgEquivUnitsSimpleMod = ⋯.choose

@[implicit_reducible]

noncomputable instance map_mul_proof.instModuleSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Module F (SimpleMod α β)

Equations

• map_mul_proof.instModuleSimpleMod = Module.compHom (map_mul_proof.SimpleMod α β) (algebraMap F (CrossProductAlgebra (α * β)))

instance map_mul_proof.instIsSimpleModuleCrossProductAlgebraHMulForallProdAlgEquivUnitsSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : IsSimpleModule (CrossProductAlgebra (α * β)) (SimpleMod α β)

noncomputable def map_mul_proof.IndexingSet {K F : Type} [Field K] [Field F] [Algebra F K] (α β : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Type

Equations

• map_mul_proof.IndexingSet α β = ⋯.choose

@[implicit_reducible]

noncomputable instance map_mul_proof.instFintypeIndexingSet {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Fintype (IndexingSet α β)

Equations

• map_mul_proof.instFintypeIndexingSet = ⋯.choose

noncomputable def map_mul_proof.isoιSM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : CrossProductAlgebra (α * β) ≃ₗ[CrossProductAlgebra (α * β)] IndexingSet α β →₀ SimpleMod α β

Equations

• map_mul_proof.isoιSM = ⋯.some

instance map_mul_proof.instNonemptyIndexingSet {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Nonempty (IndexingSet α β)

instance map_mul_proof.instNeZeroNatCardIndexingSet {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : NeZero (Fintype.card (IndexingSet α β))

noncomputable def map_mul_proof.isoιSMPow {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : CrossProductAlgebra (α * β) ≃ₗ[CrossProductAlgebra (α * β)] IndexingSet α β → SimpleMod α β

Equations

• map_mul_proof.isoιSMPow = map_mul_proof.isoιSM.trans (Finsupp.linearEquivFunOnFinite (CrossProductAlgebra (α * β)) (map_mul_proof.SimpleMod α β) (map_mul_proof.IndexingSet α β))

noncomputable def map_mul_proof.isoιSMPow' {K F : Type} [Field K] [Field F] [Algebra F K] (α β : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : CrossProductAlgebra (α * β) ≃ₗ[CrossProductAlgebra (α * β)] Fin (Fintype.card (IndexingSet α β)) → SimpleMod α β

Equations

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

instance map_mul_proof.instCompatibleSMulMFinsuppIndexingSetSimpleModCrossProductAlgebraHMulForallProdAlgEquivUnits {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : LinearMap.CompatibleSMul (M α β) (IndexingSet α β →₀ SimpleMod α β) F (CrossProductAlgebra (α * β))

instance map_mul_proof.instIsScalarTowerCrossProductAlgebraHMulForallProdAlgEquivUnitsSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : IsScalarTower F (CrossProductAlgebra (α * β)) (SimpleMod α β)

instance map_mul_proof.instFiniteCrossProductAlgebraHMulForallProdAlgEquivUnitsFinsuppIndexingSetSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Module.Finite (CrossProductAlgebra (α * β)) (IndexingSet α β →₀ SimpleMod α β)

instance map_mul_proof.instFiniteFinsuppIndexingSetSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Module.Finite F (IndexingSet α β →₀ SimpleMod α β)

instance map_mul_proof.instSMulCommClassCrossProductAlgebraHMulForallProdAlgEquivUnitsSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : SMulCommClass (CrossProductAlgebra (α * β)) F (SimpleMod α β)

noncomputable def map_mul_proof.isoDagger {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] (m : ℕ) [NeZero m] : Module.End (CrossProductAlgebra (α * β)) (Fin m → SimpleMod α β) ≃ₐ[F] Matrix (Fin m) (Fin m) (Module.End (CrossProductAlgebra (α * β)) (SimpleMod α β))

Equations

• map_mul_proof.isoDagger m = { toEquiv := (endPowEquivMatrix (CrossProductAlgebra (α * β)) (map_mul_proof.SimpleMod α β) m).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

noncomputable def map_mul_proof.mopEquivEnd' {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] : (CrossProductAlgebra (α * β))ᵐᵒᵖ ≃ₐ[F] Module.End (CrossProductAlgebra (α * β)) (CrossProductAlgebra (α * β))

Equations

• map_mul_proof.mopEquivEnd' = AlgEquiv.ofRingEquiv ⋯

noncomputable def map_mul_proof.C_iso_aux {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : (CrossProductAlgebra (α * β))ᵐᵒᵖ ≃ₐ[F] Module.End (CrossProductAlgebra (α * β)) (Fin (Fintype.card (IndexingSet α β)) → SimpleMod α β)

Equations

• map_mul_proof.C_iso_aux = map_mul_proof.mopEquivEnd'.trans (LinearEquiv.conjAlgEquiv F (map_mul_proof.isoιSMPow' α β))

noncomputable def map_mul_proof.C_iso_aux' {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : (CrossProductAlgebra (α * β))ᵐᵒᵖ ≃ₐ[F] Matrix (Fin (Fintype.card (IndexingSet α β))) (Fin (Fintype.card (IndexingSet α β))) (Module.End (CrossProductAlgebra (α * β)) (SimpleMod α β))

Equations

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

theorem map_mul_proof.dim_endCSM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Module.finrank F K ^ 2 = Fintype.card (IndexingSet α β) ^ 2 * Module.finrank F (Module.End (CrossProductAlgebra (α * β)) (SimpleMod α β))

noncomputable def map_mul_proof.C_iso_aux'' {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : CrossProductAlgebra (α * β) ≃ₐ[F] (Matrix (Fin (Fintype.card (IndexingSet α β))) (Fin (Fintype.card (IndexingSet α β))) (Module.End (CrossProductAlgebra (α * β)) (SimpleMod α β)))ᵐᵒᵖ

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] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : CrossProductAlgebra (α * β) ≃ₐ[F] Matrix (Fin (Fintype.card (IndexingSet α β))) (Fin (Fintype.card (IndexingSet α β))) (Module.End (CrossProductAlgebra (α * β)) (SimpleMod α β))ᵐᵒᵖ

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] (α β : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : ∃ (ιM : Type) (x : Fintype ιM), Nonempty (M α β ≃ₗ[CrossProductAlgebra (α * β)] ιM →₀ SimpleMod α β)

noncomputable def map_mul_proof.IndexingSetM {K F : Type} [Field K] [Field F] [Algebra F K] (α β : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Type

Equations

• map_mul_proof.IndexingSetM α β = ⋯.choose

@[implicit_reducible]

noncomputable instance map_mul_proof.instFintypeIndexingSetM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Fintype (IndexingSetM α β)

Equations

• map_mul_proof.instFintypeIndexingSetM = ⋯.choose

noncomputable def map_mul_proof.M_iso_directSum {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : M α β ≃ₗ[CrossProductAlgebra (α * β)] IndexingSetM α β →₀ SimpleMod α β

Equations

• map_mul_proof.M_iso_directSum = ⋯.some

instance map_mul_proof.instFiniteCrossProductAlgebraHMulForallProdAlgEquivUnitsSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Module.Finite (CrossProductAlgebra (α * β)) (SimpleMod α β)

instance map_mul_proof.instFiniteSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Module.Finite F (SimpleMod α β)

theorem map_mul_proof.SM_F_dim {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Fintype.card (IndexingSet α β) * Module.finrank F (SimpleMod α β) = Module.finrank F K ^ 2

instance map_mul_proof.instFiniteCrossProductAlgebraHMulForallProdAlgEquivUnitsForallFinNatCardIndexingSetFinrankSimpleMod {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Module.Finite (CrossProductAlgebra (α * β)) (Fin (Fintype.card (IndexingSet α β) * Module.finrank F K) → SimpleMod α β)

theorem map_mul_proof.M_iso_powAux {K F : Type} [Field K] [Field F] [Algebra F K] (α β : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Nonempty (M α β ≃ₗ[CrossProductAlgebra (α * β)] Fin (Module.finrank F K * Fintype.card (IndexingSet α β)) → SimpleMod α β)

noncomputable def map_mul_proof.M_iso_pow {K F : Type} [Field K] [Field F] [Algebra F K] (α β : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : M α β ≃ₗ[CrossProductAlgebra (α * β)] Fin (Module.finrank F K * Fintype.card (IndexingSet α β)) → SimpleMod α β

Equations

• map_mul_proof.M_iso_pow α β = ⋯.some

noncomputable def map_mul_proof.M_iso_pow' {K F : Type} [Field K] [Field F] [Algebra F K] (α β : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : M α β ≃ₗ[F] Fin (Module.finrank F K * Fintype.card (IndexingSet α β)) → SimpleMod α β

Equations

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

noncomputable def map_mul_proof.endCMIso {K F : Type} [Field K] [Field F] [Algebra F K] (α β : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Module.End (CrossProductAlgebra (α * β)) (M α β) ≃ₐ[F] Module.End (CrossProductAlgebra (α * β)) (Fin (Module.finrank F K * Fintype.card (IndexingSet α β)) → SimpleMod α β)

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] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : NeZero (Module.finrank F K * Fintype.card (IndexingSet α β))

noncomputable def map_mul_proof.endCMIso' {K F : Type} [Field K] [Field F] [Algebra F K] (α β : Gal(K/F) × Gal(K/F) → Kˣ) [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Module.End (CrossProductAlgebra (α * β)) (M α β) ≃ₐ[F] Matrix (Fin (Module.finrank F K * Fintype.card (IndexingSet α β))) (Fin (Module.finrank F K * Fintype.card (IndexingSet α β))) (Module.End (CrossProductAlgebra (α * β)) (SimpleMod α β))

Equations

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

theorem map_mul_proof.dim_endCM {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : Module.finrank F (Module.End (CrossProductAlgebra (α * β)) (M α β)) = Module.finrank F K ^ 4

noncomputable def map_mul_proof.φ1 {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : (TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β))ᵐᵒᵖ ≃ₐ[F] Module.End (CrossProductAlgebra (α * β)) (M α β)

Equations

• map_mul_proof.φ1 = AlgEquiv.ofBijective map_mul_proof.φ0 ⋯

noncomputable def map_mul_proof.φ2 {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β) ≃ₐ[F] (Module.End (CrossProductAlgebra (α * β)) (M α β))ᵐᵒᵖ

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] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β) ≃ₐ[F] (Matrix (Fin (Module.finrank F K * Fintype.card (IndexingSet α β))) (Fin (Module.finrank F K * Fintype.card (IndexingSet α β))) (Module.End (CrossProductAlgebra (α * β)) (SimpleMod α β)))ᵐᵒᵖ

Equations

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

noncomputable def map_mul_proof.φ4 {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β) ≃ₐ[F] Matrix (Fin (Module.finrank F K * Fintype.card (IndexingSet α β))) (Fin (Module.finrank F K * Fintype.card (IndexingSet α β))) (Module.End (CrossProductAlgebra (α * β)) (SimpleMod α β))ᵐᵒᵖ

Equations

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

theorem map_mul_proof.isBrauerEquivalent {K F : Type} [Field K] [Field F] [Algebra F K] {α β : Gal(K/F) × Gal(K/F) → Kˣ} [Fact (groupCohomology.IsMulCocycle₂ α)] [Fact (groupCohomology.IsMulCocycle₂ β)] [FiniteDimensional F K] [IsGalois F K] : IsBrauerEquivalent { toAlgCat := AlgCat.of F (TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β)), isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ } { toAlgCat := AlgCat.of F (CrossProductAlgebra (α * β)), isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ }

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

Equations

• RelativeBrGroup.isoSnd K F = (AddEquiv.mk' (Additive.ofMul.symm.trans RelativeBrGroup.equivSnd).symm ⋯).symm