Documentation

BrauerGroup.DoubleCentralizer

theorem centralizer_inclusionLeft {F A A' : Type u} [Field F] [Ring A] [Algebra F A] [Ring A'] [Algebra F A'] (B : Subalgebra F A) {ι' : Type u_2} (𝒜' : Basis ι' F A') :

Subalgebra.centralizer F ↑(Algebra.TensorProduct.includeLeft.comp B.val).range = (Algebra.TensorProduct.map (Subalgebra.centralizer F ↑B).val (AlgHom.id F A')).range

theorem centralizer_inclusionRight {F A A' : Type u} [Field F] [Ring A] [Algebra F A] [Ring A'] [Algebra F A'] (B' : Subalgebra F A') {ι : Type u_1} (𝒜 : Basis ι F A) :

Subalgebra.centralizer F ↑(Algebra.TensorProduct.includeRight.comp B'.val).range = (Algebra.TensorProduct.map (AlgHom.id F A) (Subalgebra.centralizer F ↑B').val).range

theorem centralizer_tensor_le_inf_centralizer {F A A' : Type u} [Field F] [Ring A] [Algebra F A] [Ring A'] [Algebra F A'] (B : Subalgebra F A) (B' : Subalgebra F A') :

Subalgebra.centralizer F ↑(Algebra.TensorProduct.map B.val B'.val).range ≤ Subalgebra.centralizer F ↑(Algebra.TensorProduct.includeLeft.comp B.val).range ⊓ Subalgebra.centralizer F ↑(Algebra.TensorProduct.includeRight.comp B'.val).range

theorem centralizer_tensor_centralizer {F A A' : Type u} [Field F] [Ring A] [Algebra F A] [Ring A'] [Algebra F A'] (B : Subalgebra F A) (B' : Subalgebra F A') {ι : Type u_1} {ι' : Type u_2} (𝒜 : Basis ι F A) (𝒜' : Basis ι' F A') :

Subalgebra.centralizer F ↑(Algebra.TensorProduct.map B.val B'.val).range = (Algebra.TensorProduct.map (Subalgebra.centralizer F ↑B).val (Subalgebra.centralizer F ↑B').val).range

theorem centralizer_mulLeft_le_of_isCentralSimple (F B : Type u) [Field F] [Ring B] [Algebra F B] [Algebra.IsCentral F B] [IsSimpleRing B] [FiniteDimensional F B] :

↑(Subalgebra.centralizer F (Set.range (LinearMap.mulLeft F))) ≤ Set.range (LinearMap.mulRight F)

def centralizerMulLeftCopy (F B : Type u) [Field F] [Ring B] [Algebra F B] :

↥(Subalgebra.centralizer F (Set.range (LinearMap.mulLeft F))) →ₗ[F] B →ₗ[↥(Subalgebra.center F B)] B

Equations

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

Instances For

instance instSMulCommClassSubtypeMemSubalgebraCenter_brauerGroup {F B : Type u} [Field F] [Ring B] [Algebra F B] :

SMulCommClass (↥(Subalgebra.center F B)) B B

noncomputable instance center_field {F B : Type u} [Field F] [Ring B] [Algebra F B] [IsSimpleRing B] :

Field ↥(Subalgebra.center F B)

Equations

center_field = ⋯.toField

instance center_algebra {F B : Type u} [Field F] [Ring B] [Algebra F B] :

Algebra (↥(Subalgebra.center F B)) B

Equations

center_algebra = Algebra.mk { toFun := fun (a : ↥(Subalgebra.center F B)) => ↑a, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

instance instFiniteDimensionalSubtypeMemSubalgebraCenter_brauerGroup {F B : Type u} [Field F] [Ring B] [Algebra F B] [IsSimpleRing B] [FiniteDimensional F B] :

FiniteDimensional (↥(Subalgebra.center F B)) B

def Module.End.leftMul (F B : Type u) [Field F] [Ring B] [Algebra F B] :

Subalgebra F (End F B)

Equations

Module.End.leftMul F B = { carrier := Set.range (LinearMap.mulLeft F), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

Instances For

@[simp]

theorem Module.End.coe_leftMul (F B : Type u) [Field F] [Ring B] [Algebra F B] :

↑(leftMul F B) = Set.range (LinearMap.mulLeft F)

def Module.End.rightMul (F B : Type u) [Field F] [Ring B] [Algebra F B] :

Subalgebra F (End F B)

Equations

Module.End.rightMul F B = { carrier := Set.range (LinearMap.mulRight F), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

Instances For

noncomputable def Module.End.rightMulEquiv {F B : Type u} [Field F] [Ring B] [Algebra F B] :

↥(rightMul F B) ≃ₐ[F] Bᵐᵒᵖ

Equations

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

Instances For

theorem centralizer_mulLeft {F B : Type u} [Field F] [Ring B] [Algebra F B] [IsSimpleRing B] [FiniteDimensional F B] :

Subalgebra.centralizer F ↑(Module.End.leftMul F B) = Module.End.rightMul F B

def Subalgebra.conj {F A : Type u} [Field F] [Ring A] [Algebra F A] (B : Subalgebra F A) (x : Aˣ) :

Equations

B.conj x = { carrier := {y : A | ∃ b ∈ B, y = ↑x * b * ↑x⁻¹}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

Instances For

@[simp]

theorem Subalgebra.coe_conj {F A : Type u} [Field F] [Ring A] [Algebra F A] (B : Subalgebra F A) (x : Aˣ) :

↑(B.conj x) = {y : A | ∃ b ∈ B, y = ↑x * b * ↑x⁻¹}

theorem Subalgebra.mem_conj {F A : Type u} [Field F] [Ring A] [Algebra F A] {B : Subalgebra F A} {x : Aˣ} {y : A} :

y ∈ B.conj x ↔ ∃ b ∈ B, y = ↑x * b * ↑x⁻¹

def Subalgebra.toConj {F A : Type u} [Field F] [Ring A] [Algebra F A] (B : Subalgebra F A) (x : Aˣ) :

↥B →ₐ[F] ↥(B.conj x)

Equations

B.toConj x = { toFun := fun (b : ↥B) => ⟨↑x * ↑b * ↑x⁻¹, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

@[simp]

theorem Subalgebra.toConj_apply_coe {F A : Type u} [Field F] [Ring A] [Algebra F A] (B : Subalgebra F A) (x : Aˣ) (b : ↥B) :

↑((B.toConj x) b) = ↑x * ↑b * ↑x⁻¹

def Subalgebra.fromConj {F A : Type u} [Field F] [Ring A] [Algebra F A] (B : Subalgebra F A) (x : Aˣ) :

↥(B.conj x) →ₐ[F] ↥B

Equations

B.fromConj x = { toFun := fun (b : ↥(B.conj x)) => ⟨↑x⁻¹ * ↑b * ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

@[simp]

theorem Subalgebra.fromConj_apply_coe {F A : Type u} [Field F] [Ring A] [Algebra F A] (B : Subalgebra F A) (x : Aˣ) (b : ↥(B.conj x)) :

↑((B.fromConj x) b) = ↑x⁻¹ * ↑b * ↑x

def Subalgebra.conjEquiv {F A : Type u} [Field F] [Ring A] [Algebra F A] (B : Subalgebra F A) (x : Aˣ) :

↥B ≃ₐ[F] ↥(B.conj x)

Equations

B.conjEquiv x = AlgEquiv.ofAlgHom (B.toConj x) (B.fromConj x) ⋯ ⋯

Instances For

theorem Subalgebra.finrank_conj {F A : Type u} [Field F] [Ring A] [Algebra F A] (B : Subalgebra F A) (x : Aˣ) :

Module.finrank F ↥(B.conj x) = Module.finrank F ↥B

theorem Subalgebra.conj_simple_iff {F A : Type u} [Field F] [Ring A] [Algebra F A] {B : Subalgebra F A} {x : Aˣ} :

IsSimpleOrder (TwoSidedIdeal ↥(B.conj x)) ↔ IsSimpleOrder (TwoSidedIdeal ↥B)

theorem Subalgebra.conj_centralizer {F A : Type u} [Field F] [Ring A] [Algebra F A] (B : Subalgebra F A) {x : Aˣ} :

centralizer F ↑(B.conj x) = (centralizer F ↑B).conj x

theorem Subalgebra.conj_centralizer' {F A : Type u} [Field F] [Ring A] [Algebra F A] (B : Subalgebra F A) {x : Aˣ} :

centralizer F (B.conj x).carrier = (centralizer F ↑B).conj x

instance centralizer_isSimple.aux.instIsCentralMatrixFinFinrankSubtypeMemSubalgebra_brauerGroup {F A : Type u} [Field F] [Ring A] [Algebra F A] [FiniteDimensional F A] [IsSimpleRing A] (B : Subalgebra F A) :

Algebra.IsCentral F (Matrix (Fin (Module.finrank F ↥B)) (Fin (Module.finrank F ↥B)) F)

instance centralizer_isSimple.aux.instIsCentralEndSubtypeMemSubalgebra_brauerGroup {F A : Type u} [Field F] [Ring A] [Algebra F A] [FiniteDimensional F A] [IsSimpleRing A] (B : Subalgebra F A) :

Algebra.IsCentral F (Module.End F ↥B)

instance centralizer_isSimple.aux.instIsSimpleRingEndSubtypeMemSubalgebra_brauerGroup {F A : Type u} [Field F] [Ring A] [Algebra F A] [FiniteDimensional F A] [IsSimpleRing A] (B : Subalgebra F A) :

IsSimpleRing (Module.End F ↥B)

noncomputable def centralizer_isSimple.aux.auxLeft {F A : Type u} [Field F] [Ring A] [Algebra F A] (B : Subalgebra F A) (C : Type u) [Ring C] [Algebra F C] :

TensorProduct F (↥B) C ≃ₐ[F] ↥(Algebra.TensorProduct.map B.val (AlgHom.id F C)).range

Equations

centralizer_isSimple.aux.auxLeft B C = AlgEquiv.ofLinearEquiv (LinearEquiv.ofInjective (TensorProduct.AlgebraTensorModule.map B.val.toLinearMap (AlgHom.id F C).toLinearMap) ⋯) ⋯ ⋯

Instances For

noncomputable def centralizer_isSimple.aux.auxRight {F A : Type u} [Field F] [Ring A] [Algebra F A] (B : Subalgebra F A) (C : Type u) [Ring C] [Algebra F C] :

TensorProduct F C ↥B ≃ₐ[F] ↥(Algebra.TensorProduct.map (AlgHom.id F C) B.val).range

Equations

centralizer_isSimple.aux.auxRight B C = AlgEquiv.ofLinearEquiv (LinearEquiv.ofInjective (TensorProduct.AlgebraTensorModule.map (AlgHom.id F C).toLinearMap B.val.toLinearMap) ⋯) ⋯ ⋯

Instances For

instance centralizer_isSimple.aux.instIsSimpleRingTensorProductSubtypeEndMemSubalgebraRightMul {F A : Type u} [Field F] [Ring A] [Algebra F A] [Algebra.IsCentral F A] [IsSimpleRing A] (B : Subalgebra F A) [IsSimpleRing ↥B] :

IsSimpleRing (TensorProduct F A ↥(Module.End.rightMul F ↥B))

theorem centralizer_isSimple.aux.step1 {F A : Type u} [Field F] [Ring A] [Algebra F A] [FiniteDimensional F A] [Algebra.IsCentral F A] [IsSimpleRing A] (B : Subalgebra F A) [IsSimpleRing ↥B] {ι : Type u_1} (ℬ : Basis ι F (Module.End F ↥B)) :

∃ (x : (TensorProduct F A (Module.End F ↥B))ˣ), Nonempty (TensorProduct F (↥(Subalgebra.centralizer F ↑B)) (Module.End F ↥B) ≃ₐ[F] ↥((Algebra.TensorProduct.map (AlgHom.id F A) (Module.End.rightMul F ↥B).val).range.conj x))

theorem centralizer_isSimple.aux.finrank_mop {F : Type u} [Field F] (B : Type u_1) [Ring B] [Algebra F B] :

Module.finrank F Bᵐᵒᵖ = Module.finrank F B

theorem centralizer_isSimple {F A : Type u} [Field F] [Ring A] [Algebra F A] [FiniteDimensional F A] [Algebra.IsCentral F A] [IsSimpleRing A] (B : Subalgebra F A) [IsSimpleRing ↥B] {ι : Type u_1} (ℬ : Basis ι F (Module.End F ↥B)) :

IsSimpleRing ↥(Subalgebra.centralizer F ↑B)

theorem dim_centralizer (F : Type u) {A : Type u} [Field F] [Ring A] [Algebra F A] [FiniteDimensional F A] [Algebra.IsCentral F A] [IsSimpleRing A] (B : Subalgebra F A) [IsSimpleRing ↥B] :

Module.finrank F ↥(Subalgebra.centralizer F ↑B) * Module.finrank F ↥B = Module.finrank F A

theorem double_centralizer {F A : Type u} [Field F] [Ring A] [Algebra F A] [FiniteDimensional F A] [Algebra.IsCentral F A] [IsSimpleRing A] (B : Subalgebra F A) [IsSimpleRing ↥B] :

Subalgebra.centralizer F ↑(Subalgebra.centralizer F ↑B) = B

noncomputable def writeAsTensorProduct {F A : Type u} [Field F] [Ring A] [Algebra F A] [FiniteDimensional F A] [Algebra.IsCentral F A] [IsSimpleRing A] (B : Subalgebra F A) [Algebra.IsCentral F ↥B] [IsSimpleRing ↥B] :

A ≃ₐ[F] TensorProduct F ↥B ↥(Subalgebra.centralizer F ↑B)

Equations

writeAsTensorProduct B = (AlgEquiv.ofBijective (Algebra.TensorProduct.lift B.val (Subalgebra.centralizer F ↑B).val ⋯) ⋯).symm

Instances For