theorem bijective_of_dim_eq_of_isCentralSimple (K : Type u) [Field K] (A B : Type u) [Ring A] [Ring B] [Algebra K A] [Algebra K B] [csa_source : IsSimpleRing A] [fin_source : FiniteDimensional K A] [fin_target : FiniteDimensional K B] (f : A →ₐ[K] B) (h : Module.finrank K A = Module.finrank K B) : Function.Bijective ⇑f

theorem bijective_of_surj_of_isCentralSimple (K : Type u) [Field K] (A B : Type u) [Ring A] [Ring B] [Algebra K A] [Algebra K B] [csa_source : IsSimpleRing A] (f : A →ₐ[K] B) [Nontrivial B] (h : Function.Surjective ⇑f) : Function.Bijective ⇑f

instance CSA_op_is_CSA (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] [hA : Algebra.IsCentral K A] : Algebra.IsCentral K Aᵐᵒᵖ

instance tensor_self_op.st (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] : IsScalarTower K K (Module.End K A)

noncomputable def tensor_self_op.toEnd (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] : TensorProduct K A Aᵐᵒᵖ →ₐ[K] Module.End K A

Equations

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

instance tensor_self_op.instFiniteDimensionalMulOpposite_brauerGroup (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] [FiniteDimensional K A] : FiniteDimensional K Aᵐᵒᵖ

instance tensor_self_op.fin_end (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] [FiniteDimensional K A] : FiniteDimensional K (Module.End K A)

theorem tensor_self_op.dim_eq (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] [FiniteDimensional K A] : Module.finrank K (TensorProduct K A Aᵐᵒᵖ) = Module.finrank K (Module.End K A)

noncomputable def tensor_self_op.equivEnd (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [hA : IsSimpleRing A] [FiniteDimensional K A] : TensorProduct K A Aᵐᵒᵖ ≃ₐ[K] Module.End K A

Equations

• tensor_self_op.equivEnd K A = AlgEquiv.ofBijective (tensor_self_op.toEnd K A) ⋯

noncomputable def tensor_self_op (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [hA : IsSimpleRing A] [FiniteDimensional K A] : TensorProduct K A Aᵐᵒᵖ ≃ₐ[K] Matrix (Fin (Module.finrank K A)) (Fin (Module.finrank K A)) K

Equations

• tensor_self_op K A = (tensor_self_op.equivEnd K A).trans (algEquivMatrix (Module.finBasis K A))

noncomputable def tensor_op_self (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] [Algebra.IsCentral K A] [hA : IsSimpleRing A] [FiniteDimensional K A] : TensorProduct K Aᵐᵒᵖ A ≃ₐ[K] Matrix (Fin (Module.finrank K A)) (Fin (Module.finrank K A)) K

Equations

• tensor_op_self K A = (Algebra.TensorProduct.comm K Aᵐᵒᵖ A).trans (tensor_self_op K A)

structure CSA (K : Type u) [Field K] : Type (max u (v + 1))

• carrier : Type v
• ring : Ring self.carrier
• algebra : Algebra K self.carrier
• isCentral : Algebra.IsCentral K self.carrier
• isSimple : IsSimpleRing self.carrier
• fin_dim : FiniteDimensional K self.carrier

noncomputable instance instCoeSortCSAType (K : Type u) [Field K] : CoeSort (CSA K) (Type v)

Equations

• instCoeSortCSAType K = { coe := fun (A : CSA K) => A.carrier }

noncomputable instance instRingCarrier (K : Type u) [Field K] (A : CSA K) : Ring A.carrier

Equations

• instRingCarrier K A = A.ring

noncomputable instance instAlgebraCarrier (K : Type u) [Field K] (A : CSA K) : Algebra K A.carrier

Equations

• instAlgebraCarrier K A = A.algebra

instance instIsCentralCarrier (K : Type u) [Field K] (A : CSA K) : Algebra.IsCentral K A.carrier

instance instIsSimpleRingCarrier (K : Type u) [Field K] (A : CSA K) : IsSimpleRing A.carrier

instance instFiniteDimensionalCarrier (K : Type u) [Field K] (A : CSA K) : FiniteDimensional K A.carrier

structure BrauerEquivalence {K : Type u} [Field K] (A : CSA K) (B : CSA K) : Type (max u_1 u_2)

• n : ℕ
• m : ℕ
• hn : NeZero self.n
• hm : NeZero self.m
• iso : Matrix (Fin self.n) (Fin self.n) A.carrier ≃ₐ[K] Matrix (Fin self.m) (Fin self.m) B.carrier

instance instNeZeroNatN {K : Type u} [Field K] (A : CSA K) (B : CSA K) (h : BrauerEquivalence A B) : NeZero h.n

instance instNeZeroNatM {K : Type u} [Field K] (A : CSA K) (B : CSA K) (h : BrauerEquivalence A B) : NeZero h.m

@[reducible, inline]

noncomputable abbrev IsBrauerEquivalent {K : Type u} [Field K] (A : CSA K) (B : CSA K) : Prop

Equations

• IsBrauerEquivalent A B = Nonempty (BrauerEquivalence A B)

noncomputable def IsBrauerEquivalent.refl {K : Type u} [Field K] (A : CSA K) : IsBrauerEquivalent A A

Equations

• ⋯ = ⋯

noncomputable def IsBrauerEquivalent.symm {K : Type u} [Field K] {A : CSA K} {B : CSA K} (h : IsBrauerEquivalent A B) : IsBrauerEquivalent B A

Equations

• ⋯ = ⋯

noncomputable def IsBrauerEquivalent.matrix_eqv' {K : Type u} [Field K] (n m : ℕ) (A : Type u_1) [Ring A] [Algebra K A] : Matrix (Fin n × Fin m) (Fin n × Fin m) A ≃ₐ[K] Matrix (Fin (n * m)) (Fin (n * m)) A

Equations

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

noncomputable def IsBrauerEquivalent.trans {K : Type u} [Field K] {A : CSA K} {B : CSA K} {C : CSA K} (hAB : IsBrauerEquivalent A B) (hBC : IsBrauerEquivalent B C) : IsBrauerEquivalent A C

Equations

• ⋯ = ⋯

theorem IsBrauerEquivalent.iso_to_eqv {K : Type u} [Field K] (A : CSA K) (B : CSA K) (h : A.carrier ≃ₐ[K] B.carrier) : IsBrauerEquivalent A B

theorem IsBrauerEquivalent.Braur_is_eqv {K : Type u} [Field K] : Equivalence IsBrauerEquivalent

noncomputable def BrauerGroup.CSA_Setoid {K : Type u} [Field K] : Setoid (CSA K)

Equations

• BrauerGroup.CSA_Setoid = { r := IsBrauerEquivalent, iseqv := ⋯ }

noncomputable def BrauerGroup.mul {K : Type u} [Field K] (A B : CSA K) : CSA K

Equations

• BrauerGroup.mul A B = CSA.mk (TensorProduct K A.carrier B.carrier)

noncomputable def BrauerGroup.is_fin_dim_of_mop {K : Type u} [Field K] (A : Type u_1) [Ring A] [Algebra K A] [FiniteDimensional K A] : FiniteDimensional K Aᵐᵒᵖ

Equations

• ⋯ = ⋯

noncomputable def BrauerGroup.one_in {K : Type u} [Field K] (n : ℕ) [hn : NeZero n] : CSA K

Equations

• BrauerGroup.one_in n = CSA.mk (Matrix (Fin n) (Fin n) K)

noncomputable def BrauerGroup.one_in' {K : Type u} [Field K] : CSA K

Equations

• BrauerGroup.one_in' = CSA.mk K

noncomputable def BrauerGroup.one_mul_in {K : Type u} [Field K] (n : ℕ) [hn : NeZero n] (A : CSA K) : CSA K

Equations

• BrauerGroup.one_mul_in n A = CSA.mk (TensorProduct K A.carrier (Matrix (Fin n) (Fin n) K))

noncomputable def BrauerGroup.mul_one_in {K : Type u} [Field K] (n : ℕ) [hn : NeZero n] (A : CSA K) : CSA K

Equations

• BrauerGroup.mul_one_in n A = CSA.mk (TensorProduct K (Matrix (Fin n) (Fin n) K) A.carrier)

noncomputable def BrauerGroup.eqv_in {K : Type u} [Field K] (A : CSA K) (A' : Type u_1) [Ring A'] [Algebra K A'] (e : A.carrier ≃ₐ[K] A') : CSA K

Equations

• BrauerGroup.eqv_in A A' e = CSA.mk A'

noncomputable def BrauerGroup.matrix_A {K : Type u} [Field K] (n : ℕ) [hn : NeZero n] (A : CSA K) : CSA K

Equations

• BrauerGroup.matrix_A n A = BrauerGroup.eqv_in (BrauerGroup.one_mul_in n A) (Matrix (Fin n) (Fin n) A.carrier) (id (matrixEquivTensor K A.carrier (Fin n)).symm)

noncomputable def BrauerGroup.dim_1 {K : Type u} [Field K] (R : Type u_1) [Ring R] [Algebra K R] : Algebra K (Matrix (Fin 1) (Fin 1) R)

Equations

• BrauerGroup.dim_1 R = Algebra.mk { toFun := fun (k : K) => Matrix.diagonal fun (x : Fin 1) => (Algebra.ofId K R) k, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

noncomputable def BrauerGroup.dim_one_iso {K : Type u} [Field K] (R : Type u_1) [Ring R] [Algebra K R] : Matrix (Fin 1) (Fin 1) R ≃ₐ[K] R

Equations

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

noncomputable def BrauerGroup.matrix_comp {K : Type u} [Field K] (n m : ℕ) (A : Type u_1) [Ring A] [Algebra K A] : Matrix (Fin n) (Fin n) (Matrix (Fin m) (Fin m) A) ≃ₐ[K] Matrix (Fin m) (Fin m) (Matrix (Fin n) (Fin n) A)

Equations

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

theorem BrauerGroup.eqv_mat {K : Type u} [Field K] (A : CSA K) (n : ℕ) [hn : NeZero n] : IsBrauerEquivalent A (matrix_A n A)

noncomputable def BrauerGroup.matrixEquivForward {K : Type u} [Field K] (m : Type u_1) (n : Type u_2) [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] : TensorProduct K (Matrix m m K) (Matrix n n K) →ₐ[K] Matrix (m × n) (m × n) K

Equations

• BrauerGroup.matrixEquivForward m n = Algebra.TensorProduct.algHomOfLinearMapTensorProduct (TensorProduct.lift Matrix.kroneckerBilinear) ⋯ ⋯

theorem BrauerGroup.matrixEquivForward_tmul {K : Type u} [Field K] (m : Type u_1) (n : Type u_2) [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (M : Matrix m m K) (N : Matrix n n K) : (matrixEquivForward m n) (M ⊗ₜ[K] N) = Matrix.kroneckerMap (fun (x1 x2 : K) => x1 * x2) M N

theorem BrauerGroup.matrixEquivForward_surjective {K : Type u} [Field K] (n : Type u_1) (m : Type u_2) [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] : Function.Surjective ⇑(matrixEquivForward m n)

noncomputable def BrauerGroup.matrix_eqv {K : Type u} [Field K] (m n : ℕ) : TensorProduct K (Matrix (Fin m) (Fin m) K) (Matrix (Fin n) (Fin n) K) ≃ₐ[K] Matrix (Fin m × Fin n) (Fin m × Fin n) K

Equations

• BrauerGroup.matrix_eqv m n = AlgEquiv.ofBijective (BrauerGroup.matrixEquivForward (Fin m) (Fin n)) ⋯

theorem BrauerGroup.one_mul {K : Type u} [Field K] (n : ℕ) [hn : NeZero n] (A : CSA K) : IsBrauerEquivalent A (one_mul_in n A)

theorem BrauerGroup.mul_one {K : Type u} [Field K] (n : ℕ) [hn : NeZero n] (A : CSA K) : IsBrauerEquivalent A (mul_one_in n A)

theorem BrauerGroup.mul_assoc {K : Type u} [Field K] (A B C : CSA K) : IsBrauerEquivalent (mul (mul A B) C) (mul A (mul B C))

noncomputable def BrauerGroup.huarongdao {K : Type u} [Field K] (A : Type u_1) (B : Type u_2) (C : Type u_3) (D : Type u_4) [Ring A] [Ring B] [Ring C] [Ring D] [Algebra K A] [Algebra K B] [Algebra K C] [Algebra K D] : TensorProduct K (TensorProduct K A B) (TensorProduct K C D) ≃ₐ[K] TensorProduct K (TensorProduct K A C) (TensorProduct K B D)

Equations

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

noncomputable def BrauerGroup.kroneckerMatrixTensor' {K : Type u} [Field K] (A : Type u_1) (B : Type u_2) [Ring A] [Ring B] [Algebra K A] [Algebra K B] (n m : ℕ) : TensorProduct K (Matrix (Fin n) (Fin n) A) (Matrix (Fin m) (Fin m) B) ≃ₐ[K] Matrix (Fin (n * m)) (Fin (n * m)) (TensorProduct K A B)

Equations

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

theorem BrauerGroup.eqv_tensor_eqv {K : Type u} [Field K] (A B C D : CSA K) (hAB : IsBrauerEquivalent A B) (hCD : IsBrauerEquivalent C D) : IsBrauerEquivalent (mul A C) (mul B D)

@[reducible, inline]

noncomputable abbrev BrauerGroup.BrGroup {K : Type u} [Field K] : Type (max u (u_1 + 1))

Equations

• BrauerGroup.BrGroup = Quotient BrauerGroup.CSA_Setoid

noncomputable instance BrauerGroup.Mul {K : Type u} [Field K] : _root_.Mul BrGroup

Equations

• BrauerGroup.Mul = { mul := Quotient.lift₂ (fun (A B : CSA K) => ⟦BrauerGroup.mul A B⟧) ⋯ }

noncomputable instance BrauerGroup.One {K : Type u} [Field K] : _root_.One BrGroup

Equations

• BrauerGroup.One = { one := ⟦BrauerGroup.one_in'⟧ }

theorem BrauerGroup.mul_assoc' {K : Type u} [Field K] (A B C : BrGroup) : A * B * C = A * (B * C)

theorem BrauerGroup.mul_inv {K : Type u} [Field K] (A : CSA K) : IsBrauerEquivalent (mul A (inv A)) one_in'

theorem BrauerGroup.inv_mul {K : Type u} [Field K] (A : CSA K) : IsBrauerEquivalent (mul (inv A) A) one_in'

noncomputable def BrauerGroup.matrixEquivMatrixMop_algebra (K : Type u_1) (R : Type u_2) [CommSemiring K] [Semiring R] [Algebra K R] (n : ℕ) : Matrix (Fin n) (Fin n) Rᵐᵒᵖ ≃ₐ[K] (Matrix (Fin n) (Fin n) R)ᵐᵒᵖ

Mn(Rᵒᵖ) ≃ₐ[K] Mₙ(R)ᵒᵖ

Equations

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

theorem BrauerGroup.inv_eqv {K : Type u} [Field K] (A B : CSA K) (hAB : IsBrauerEquivalent A B) : IsBrauerEquivalent (inv A) (inv B)

noncomputable instance BrauerGroup.Inv {K : Type u} [Field K] : _root_.Inv BrGroup

Equations

• BrauerGroup.Inv = { inv := Quotient.lift (fun (A : CSA K) => ⟦BrauerGroup.inv A⟧) ⋯ }

theorem BrauerGroup.mul_left_inv' {K : Type u} [Field K] (A : BrGroup) : A⁻¹ * A = 1

theorem BrauerGroup.one_mul' {K : Type u} [Field K] (A : BrGroup) : 1 * A = A

theorem BrauerGroup.mul_one' {K : Type u} [Field K] (A : BrGroup) : A * 1 = A

noncomputable instance BrauerGroup.Bruaer_Group {K : Type u} [Field K] : Group BrGroup

Equations

• BrauerGroup.Bruaer_Group = Group.mk ⋯

theorem BrauerGroup.Alg_closed_equiv_one {K : Type u} [Field K] [IsAlgClosed K] (A : CSA K) : IsBrauerEquivalent A one_in'

theorem BrauerGroup.Alg_closed_eq_one {K : Type u} [Field K] [IsAlgClosed K] (A : BrGroup) : A = 1

noncomputable instance BrauerGroup.instUniqueBrGroupOfIsAlgClosed {K : Type u} [Field K] [IsAlgClosed K] : Unique BrGroup

Equations

• BrauerGroup.instUniqueBrGroupOfIsAlgClosed = { default := 1, uniq := ⋯ }

theorem BrauerGroup.Alg_closed_Brauer_trivial {K : Type u} [Field K] [IsAlgClosed K] : ⊤ = ⊥

noncomputable def BrauerGroupHom.someEquivs.e1 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] (A : Type u) [Ring A] [Algebra K A] (m : ℕ) : Matrix (Fin m) (Fin m) (TensorProduct K E A) ≃ₐ[E] TensorProduct E (TensorProduct K E A) (Matrix (Fin m) (Fin m) E)

Equations

• BrauerGroupHom.someEquivs.e1 A m = matrixEquivTensor E (TensorProduct K E A) (Fin m)

noncomputable def BrauerGroupHom.someEquivs.e2 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] (A : Type u) [Ring A] [Algebra K A] (m : ℕ) : TensorProduct E (TensorProduct K E A) (Matrix (Fin m) (Fin m) E) ≃ₐ[E] TensorProduct E (TensorProduct K E A) (TensorProduct K E (Matrix (Fin m) (Fin m) K))

Equations

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

noncomputable def BrauerGroupHom.someEquivs.e3Aux0 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] (A : Type u) [Ring A] [Algebra K A] (m : ℕ) : TensorProduct K E A →ₐ[E] TensorProduct K E (TensorProduct K A (Matrix (Fin m) (Fin m) K))

Equations

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

noncomputable def BrauerGroupHom.someEquivs.e3Aux10 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] (A : Type u) [Ring A] [Algebra K A] (m : ℕ) : TensorProduct K (TensorProduct K E (Matrix (Fin m) (Fin m) K)) A ≃ₐ[K] TensorProduct K E (TensorProduct K A (Matrix (Fin m) (Fin m) K))

Equations

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

noncomputable def BrauerGroupHom.someEquivs.e3Aux1 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] (A : Type u) [Ring A] [Algebra K A] (m : ℕ) : TensorProduct K E (Matrix (Fin m) (Fin m) K) →ₐ[E] TensorProduct K E (TensorProduct K A (Matrix (Fin m) (Fin m) K))

Equations

• BrauerGroupHom.someEquivs.e3Aux1 A m = (let __src := ↑(BrauerGroupHom.someEquivs.e3Aux10 A m); { toRingHom := __src.toRingHom, commutes' := ⋯ }).comp Algebra.TensorProduct.includeLeft

theorem BrauerGroupHom.someEquivs.e3Aux3 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] (A : Type u) [Ring A] [Algebra K A] (m : ℕ) (hm : m = 0) : Subsingleton (TensorProduct E (TensorProduct K E A) (TensorProduct K E (Matrix (Fin m) (Fin m) K)))

noncomputable def BrauerGroupHom.someEquivs.e3Aux4 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] (A : Type u) [Ring A] [Algebra K A] (m : ℕ) : TensorProduct E (TensorProduct K E A) (TensorProduct K E (Matrix (Fin m) (Fin m) K)) →ₐ[E] TensorProduct K E (TensorProduct K A (Matrix (Fin m) (Fin m) K))

Equations

• BrauerGroupHom.someEquivs.e3Aux4 A m = Algebra.TensorProduct.lift (BrauerGroupHom.someEquivs.e3Aux0 A m) (BrauerGroupHom.someEquivs.e3Aux1 A m) ⋯

theorem BrauerGroupHom.someEquivs.e3Aux5 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] (A : Type u) [Ring A] [Algebra K A] (m : ℕ) : Function.Surjective ⇑(e3Aux4 A m)

noncomputable def BrauerGroupHom.someEquivs.e3 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] (A : Type u) [Ring A] [Algebra K A] (m : ℕ) [Algebra.IsCentral K A] [csa_A : IsSimpleRing A] : TensorProduct E (TensorProduct K E A) (TensorProduct K E (Matrix (Fin m) (Fin m) K)) ≃ₐ[E] TensorProduct K E (TensorProduct K A (Matrix (Fin m) (Fin m) K))

Equations

• BrauerGroupHom.someEquivs.e3 A m = AlgEquiv.ofBijective (BrauerGroupHom.someEquivs.e3Aux4 A m) ⋯

noncomputable def BrauerGroupHom.someEquivs.e4 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] (A : Type u) [Ring A] [Algebra K A] (m : ℕ) : TensorProduct K E (TensorProduct K A (Matrix (Fin m) (Fin m) K)) ≃ₐ[E] TensorProduct K E (Matrix (Fin m) (Fin m) A)

Equations

• BrauerGroupHom.someEquivs.e4 A m = Algebra.TensorProduct.congr AlgEquiv.refl (matrixEquivTensor K A (Fin m)).symm

noncomputable def BrauerGroupHom.someEquivs.e5 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] (A B : Type u) [Ring A] [Algebra K A] [Ring B] [Algebra K B] (e : A ≃ₐ[K] B) : TensorProduct K E A ≃ₐ[E] TensorProduct K E B

Equations

• BrauerGroupHom.someEquivs.e5 A B e = Algebra.TensorProduct.congr AlgEquiv.refl e

noncomputable def BrauerGroupHom.someEquivs.e6Aux0 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] (A B : Type u) [Ring A] [Algebra K A] [Ring B] [Algebra K B] : TensorProduct E (TensorProduct K E A) (TensorProduct K E B) →ₐ[E] TensorProduct K E (TensorProduct K A B)

Equations

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

noncomputable def BrauerGroupHom.someEquivs.e6 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] (A B : Type u) [Ring A] [Algebra K A] [Ring B] [Algebra K B] [Algebra.IsCentral K A] [csa_A : IsSimpleRing A] [Algebra.IsCentral K B] [csa_B : IsSimpleRing B] : TensorProduct E (TensorProduct K E A) (TensorProduct K E B) ≃ₐ[E] TensorProduct K E (TensorProduct K A B)

Equations

• BrauerGroupHom.someEquivs.e6 A B = AlgEquiv.ofBijective (BrauerGroupHom.someEquivs.e6Aux0 A B) ⋯

noncomputable def BrauerGroupHom.someEquivs.e7 {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] : E ≃ₐ[E] TensorProduct K E K

Equations

• BrauerGroupHom.someEquivs.e7 = (Algebra.TensorProduct.rid K E E).symm

@[reducible, inline]

noncomputable abbrev BrauerGroupHom.BaseChange {K : Type u} [Field K] {E : Type u} [Field E] [Algebra K E] : BrauerGroup.BrGroup →* BrauerGroup.BrGroup

Equations

• BrauerGroupHom.BaseChange = { toFun := Quotient.map' (fun (A : CSA K) => CSA.mk (TensorProduct K E A.carrier)) ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[reducible, inline]

noncomputable abbrev BrauerGroupHom.BaseChange_Q_to_C : BrauerGroup.BrGroup →* BrauerGroup.BrGroup

Equations

• BrauerGroupHom.BaseChange_Q_to_C = BrauerGroupHom.BaseChange

theorem BrauerGroupHom.BaseChange_Q_to_C_eq_one : BaseChange_Q_to_C = 1

noncomputable instance BrauerGroupHom.IsAbelBrauer {K : Type u} [Field K] : CommGroup BrauerGroup.BrGroup

Equations

• BrauerGroupHom.IsAbelBrauer = CommGroup.mk ⋯

noncomputable def BrauerGroupHom.baseChange_idem.Aux (F K E : Type u) [Field F] [Field K] [Field E] [Algebra F K] [Algebra F E] [Algebra K E] [IsScalarTower F K E] (A : CSA F) : TensorProduct K E (TensorProduct F K A.carrier) ≃ₗ[E] TensorProduct F E A.carrier

Equations

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

noncomputable def BrauerGroupHom.baseChange_idem.Aux' (F K E : Type u) [Field F] [Field K] [Field E] [Algebra F K] [Algebra F E] [Algebra K E] [IsScalarTower F K E] (A : CSA F) : TensorProduct K E (TensorProduct F K A.carrier) ≃ₐ[E] TensorProduct F E A.carrier

Equations

• BrauerGroupHom.baseChange_idem.Aux' F K E A = AlgEquiv.ofLinearEquiv (BrauerGroupHom.baseChange_idem.Aux F K E A) ⋯ ⋯

theorem BrauerGroupHom.baseChange_idem (F K E : Type u) [Field F] [Field K] [Field E] [Algebra F K] [Algebra F E] [Algebra K E] [IsScalarTower F K E] : BaseChange = BaseChange.comp BaseChange

noncomputable def BrauerGroupHom.Br : CategoryTheory.Functor FieldCat CommGrp

Equations

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