LeanPool.BrauerGroupNew.DoubleCentralizer

Imported Lean Pool material for LeanPool.BrauerGroupNew.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} (𝒜' : Module.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} (𝒜 : Module.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} (𝒜 : Module.Basis ι F A) (𝒜' : Module.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

Identifies the centralizer of left multiplication with endomorphisms over the center.

Equations

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

instance instSMulCommClassSubtypeMemSubalgebraCenter_leanPool {F B : Type u} [Field F] [Ring B] [Algebra F B] : SMulCommClass (↥(Subalgebra.center F B)) B B

@[implicit_reducible]

noncomputable instance centerField {F B : Type u} [Field F] [Ring B] [Algebra F B] [IsSimpleRing B] : Field ↥(Subalgebra.center F B)

Equations

• centerField = ⋯.toField

@[implicit_reducible]

instance centerAlgebra {F B : Type u} [Field F] [Ring B] [Algebra F B] : Algebra (↥(Subalgebra.center F B)) B

Equations

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

instance instFiniteDimensionalSubtypeMemSubalgebraCenter_leanPool {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)

The subalgebra of endomorphisms given by left multiplication.

Equations

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

@[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)

The subalgebra of endomorphisms given by right multiplication.

Equations

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

noncomputable def Module.End.rightMulEquiv {F B : Type u} [Field F] [Ring B] [Algebra F B] : ↥(rightMul F B) ≃ₐ[F] Bᵐᵒᵖ

Right multiplication endomorphisms are equivalent to the opposite algebra.

Equations

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

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ˣ) : Subalgebra F A

The conjugate of a subalgebra by a unit.

Equations

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

@[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)

The algebra homomorphism from a subalgebra to its conjugate.

Equations

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

@[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

The algebra homomorphism from a conjugate subalgebra back to the original subalgebra.

Equations

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

@[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)

Conjugation by a unit gives an algebra equivalence onto the conjugate subalgebra.

Equations

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

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 centralizerIsSimple.aux.instIsCentralMatrixFinFinrankSubtypeMemSubalgebra_leanPool {F A : Type u} [Field F] [Ring A] [Algebra F A] (B : Subalgebra F A) : Algebra.IsCentral F (Matrix (Fin (Module.finrank F ↥B)) (Fin (Module.finrank F ↥B)) F)

instance centralizerIsSimple.aux.instIsCentralEndSubtypeMemSubalgebra_leanPool {F A : Type u} [Field F] [Ring A] [Algebra F A] [FiniteDimensional F A] (B : Subalgebra F A) : Algebra.IsCentral F (Module.End F ↥B)

instance centralizerIsSimple.aux.instIsSimpleRingEndSubtypeMemSubalgebra_leanPool {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 centralizerIsSimple.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

The left tensor inclusion as an algebra equivalence onto its range.

Equations

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

noncomputable def centralizerIsSimple.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

The right tensor inclusion as an algebra equivalence onto its range.

Equations

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

instance centralizerIsSimple.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 centralizerIsSimple.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} (ℬ : Module.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 centralizerIsSimple.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 centralizerIsSimple {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} (ℬ : Module.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) [IsSimpleRing ↥B] [Algebra.IsCentral F ↥B] : A ≃ₐ[F] TensorProduct F ↥B ↥(Subalgebra.centralizer F ↑B)

The double-centralizer tensor-product decomposition.

Equations

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