LeanPool.BrauerGroupNew.IsoSecond

Imported Lean Pool material for LeanPool.BrauerGroupNew.IsoSecond.

noncomputable def mapMulProof.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 β))

The balancing relations used to form the tensor-product quotient module.

Equations

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

@[simp]

theorem mapMulProof.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 mapMulProof.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

The balanced tensor-product module used in the multiplicativity proof.

Equations

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

noncomputable def mapMulProof.AoxFBSmulMAux {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 α β

Right multiplication by fixed tensor factors descends to the balanced quotient.

Equations

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

noncomputable def mapMulProof.AoxFBSmulMAuxAux {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 α β

The auxiliary right action map as a linear map in the second tensor factor.

Equations

• mapMulProof.AoxFBSmulMAuxAux a = { toFun := fun (b : CrossProductAlgebra β) => mapMulProof.AoxFBSmulMAux a b, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def mapMulProof.AoxFBSmulM {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 α β

The right action of A ⊗[F] B on the balanced quotient module.

Equations

• mapMulProof.AoxFBSmulM = TensorProduct.lift { toFun := mapMulProof.AoxFBSmulMAuxAux, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem mapMulProof.AoxFBSmulM_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 β) : (AoxFBSmulM (a' ⊗ₜ[F] b')) (Submodule.Quotient.mk (a ⊗ₜ[F] b)) = Submodule.Quotient.mk ((a * a') ⊗ₜ[F] (b * b'))

@[implicit_reducible]

noncomputable instance mapMulProof.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 mapMulProof.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 mapMulProof.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

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

@[implicit_reducible]

noncomputable instance mapMulProof.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 mapMulProof.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 mapMulProof.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 mapMulProof.CSmulAux {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 α β

The auxiliary left action of the product cross-product algebra on the balanced quotient.

Equations

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

theorem mapMulProof.CSmulAux_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 β) : (CSmulAux (k • CrossProductAlgebra.basis σ)) (Submodule.Quotient.mk (a ⊗ₜ[F] b)) = Submodule.Quotient.mk ((k • CrossProductAlgebra.basis σ * a) ⊗ₜ[F] (CrossProductAlgebra.basis σ * b))

noncomputable def mapMulProof.CSmul {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 α β

The left action of the product cross-product algebra on the balanced quotient.

Equations

• mapMulProof.CSmul = { toFun := mapMulProof.CSmulAux, map_add' := ⋯, map_smul' := ⋯ }

@[implicit_reducible]

noncomputable instance mapMulProof.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

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

theorem mapMulProof.CSmul_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 = (CSmul c) x

theorem mapMulProof.CSmul_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 mapMulProof.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 mapMulProof.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

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

@[implicit_reducible]

noncomputable instance mapMulProof.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 mapMulProof.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 mapMulProof.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

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

instance mapMulProof.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 α β)

theorem mapMulProof.Aox_FB_smul_comm_CSmul {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 : (TensorProduct F (CrossProductAlgebra α) (CrossProductAlgebra β))ᵐᵒᵖ) (c : CrossProductAlgebra (α * β)) (m : M α β) : x • c • m = c • x • m

The tensor-product action commutes with the cross-product action on M.

instance mapMulProof.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 mapMulProof.φ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 α β)

The representation of the opposite tensor product algebra by endomorphisms of M.

Equations

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

noncomputable def mapMulProof.MtoAoxKB {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 β)

The map from the balanced quotient to the tensor product over K.

Equations

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

noncomputable def mapMulProof.AoxKBToMAux {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 α β

The additive map from the tensor product over K back to the balanced quotient.

Equations

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

noncomputable def mapMulProof.AoxKBToM {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 α β

The linear map from the tensor product over K back to the balanced quotient.

Equations

• mapMulProof.AoxKBToM = { toFun := (↑mapMulProof.AoxKBToMAux).toFun, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def mapMulProof.AoxKBEquivM {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 β)

The balanced quotient is linearly equivalent to the tensor product over K.

Equations

• mapMulProof.AoxKBEquivM = LinearEquiv.ofLinear mapMulProof.MtoAoxKB mapMulProof.AoxKBToM ⋯ ⋯

theorem mapMulProof.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 mapMulProof.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 mapMulProof.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 mapMulProof.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 mapMulProof.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

A chosen simple module appearing in the Wedderburn decomposition of C.

Equations

• mapMulProof.SimpleMod α β = ⋯.choose

@[implicit_reducible]

noncomputable instance mapMulProof.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

• mapMulProof.instAddCommGroupSimpleMod = ⋯.choose

@[implicit_reducible]

noncomputable instance mapMulProof.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

• mapMulProof.instModuleCrossProductAlgebraHMulForallProdAlgEquivUnitsSimpleMod = ⋯.choose

@[implicit_reducible]

noncomputable instance mapMulProof.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

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

instance mapMulProof.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 mapMulProof.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

The finite index set for the simple-module decomposition of C.

Equations

• mapMulProof.IndexingSet α β = ⋯.choose

@[implicit_reducible]

noncomputable instance mapMulProof.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

• mapMulProof.instFintypeIndexingSet = ⋯.choose

noncomputable def mapMulProof.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 α β

The decomposition of C as a finite direct sum of copies of the simple module.

Equations

• mapMulProof.isoιSM = ⋯.some

instance mapMulProof.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 mapMulProof.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 mapMulProof.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 α β

The direct-sum decomposition rewritten as functions on the finite index set.

Equations

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

noncomputable def mapMulProof.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 α β

The direct-sum decomposition reindexed by Fin (Fintype.card ι).

Equations

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

instance mapMulProof.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 mapMulProof.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 mapMulProof.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 mapMulProof.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 mapMulProof.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 mapMulProof.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 : ℕ) : Module.End (CrossProductAlgebra (α * β)) (Fin m → SimpleMod α β) ≃ₐ[F] Matrix (Fin m) (Fin m) (Module.End (CrossProductAlgebra (α * β)) (SimpleMod α β))

Endomorphisms of a finite power are matrix algebras over endomorphisms of the summand.

Equations

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

noncomputable def mapMulProof.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 (α * β))

The opposite algebra of C as endomorphisms of the regular C-module.

Equations

• mapMulProof.mopEquivEnd' = AlgEquiv.ofRingEquiv ⋯

noncomputable def mapMulProof.CIsoAux {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 α β)

Transport the regular-module endomorphism algebra across the simple-module decomposition.

Equations

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

noncomputable def mapMulProof.CIsoAux' {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 α β))

The matrix form of the opposite algebra of C.

Equations

• mapMulProof.CIsoAux' = mapMulProof.CIsoAux.trans (mapMulProof.isoDagger (Fintype.card (mapMulProof.IndexingSet α β)))

theorem mapMulProof.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 mapMulProof.CIsoAux'' {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 α β)))ᵐᵒᵖ

Move the matrix algebra description from the opposite algebra back to C.

Equations

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

noncomputable def mapMulProof.CIso {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 α β))ᵐᵒᵖ

The final matrix-algebra model for the product cross-product algebra.

Equations

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

theorem mapMulProof.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 mapMulProof.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

The finite index set for the simple-module decomposition of M.

Equations

• mapMulProof.IndexingSetM α β = ⋯.choose

@[implicit_reducible]

noncomputable instance mapMulProof.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

• mapMulProof.instFintypeIndexingSetM = ⋯.choose

noncomputable def mapMulProof.MIsoDirectSum {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 α β

The decomposition of M as a finite direct sum of copies of the simple module.

Equations

• mapMulProof.MIsoDirectSum = ⋯.some

instance mapMulProof.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 mapMulProof.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 mapMulProof.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 mapMulProof.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 mapMulProof.MIsoPowAux {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 mapMulProof.MIsoPow {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 α β

A linear equivalence from M to a finite power of the chosen simple module.

Equations

• mapMulProof.MIsoPow α β = ⋯.some

noncomputable def mapMulProof.MIsoPow' {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 α β

The same finite-power equivalence over the base field.

Equations

• mapMulProof.MIsoPow' α β = LinearEquiv.restrictScalars F (mapMulProof.MIsoPow α β)

noncomputable def mapMulProof.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 α β)

Conjugation by MIsoPow identifies endomorphism algebras over C.

Equations

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

instance mapMulProof.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 mapMulProof.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 α β))

The endomorphism algebra of M as a matrix algebra over endomorphisms of SM.

Equations

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

theorem mapMulProof.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 mapMulProof.φ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 α β)

The opposite tensor product algebra as endomorphisms of the balanced quotient.

Equations

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

noncomputable def mapMulProof.φ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 α β))ᵐᵒᵖ

The tensor product algebra as the opposite of the endomorphism algebra of M.

Equations

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

noncomputable def mapMulProof.φ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 α β)))ᵐᵒᵖ

The tensor product algebra as an opposite matrix algebra over End_C(SM).

Equations

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

noncomputable def mapMulProof.φ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 α β))ᵐᵒᵖ

The tensor product algebra as a matrix algebra over the opposite endomorphism algebra.

Equations

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

theorem mapMulProof.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))

The additive form of the isomorphism between the relative Brauer group and second cohomology.

Equations

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