LeanPool.BrauerGroupNew.BrauerGroup

Imported Lean Pool material for LeanPool.BrauerGroupNew.BrauerGroup.

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 tensorSelfOp.st (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] : IsScalarTower K K (Module.End K A)

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

The action map from A ⊗ Aᵐᵒᵖ to endomorphisms of A.

Equations

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

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

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

The central simple algebra isomorphism A ⊗ Aᵐᵒᵖ ≃ End_K(A).

Equations

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

noncomputable def tensorSelfOp (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

Identifies A ⊗ Aᵐᵒᵖ with a full matrix algebra over the base field.

Equations

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

noncomputable def tensorOpSelf (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

Identifies Aᵐᵒᵖ ⊗ A with a full matrix algebra over the base field.

Equations

• tensorOpSelf K A = (Algebra.TensorProduct.comm K Aᵐᵒᵖ A).trans (tensorSelfOp K A)

noncomputable def IsBrauerEquivalent.matrixEqv' {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

Reindexes matrices over Fin n × Fin m as matrices over Fin (n * m).

Equations

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

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

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

@[implicit_reducible]

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

The setoid on central simple algebras generated by Brauer equivalence.

Equations

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

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

Tensor-product multiplication on representatives of the Brauer group.

Equations

• BrauerGroup.mul A B = { toAlgCat := AlgCat.of K (TensorProduct K ↑A.toAlgCat ↑B.toAlgCat), isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ }

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

Finite-dimensionality is preserved by passing to the opposite algebra.

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

The opposite algebra representative used for inversion in the Brauer group.

Equations

• BrauerGroup.inv A = { toAlgCat := AlgCat.of K (↑A.toAlgCat)ᵐᵒᵖ, isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ }

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

The matrix algebra representative of the identity Brauer class.

Equations

• BrauerGroup.oneIn n = { toAlgCat := AlgCat.of K (Matrix (Fin n) (Fin n) K), isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ }

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

The base field representative of the identity Brauer class.

Equations

• BrauerGroup.oneIn' = { toAlgCat := AlgCat.of K K, isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ }

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

Right tensoring by an identity matrix algebra representative.

Equations

• BrauerGroup.oneMulIn n A = { toAlgCat := AlgCat.of K (TensorProduct K (↑A.toAlgCat) (Matrix (Fin n) (Fin n) K)), isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ }

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

Left tensoring by an identity matrix algebra representative.

Equations

• BrauerGroup.mulOneIn n A = { toAlgCat := AlgCat.of K (TensorProduct K (Matrix (Fin n) (Fin n) K) ↑A.toAlgCat), isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ }

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

Transports a central simple algebra structure across an algebra equivalence.

Equations

• BrauerGroup.eqvIn A A' e = { toAlgCat := AlgCat.of K A', isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ }

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

The representative obtained by replacing A ⊗ Mₙ(K) with Mₙ(A).

Equations

• BrauerGroup.matrixA n A = BrauerGroup.eqvIn (BrauerGroup.oneMulIn n A) (Matrix (Fin n) (Fin n) ↑A.toAlgCat) (id (matrixEquivTensor (Fin n) K ↑A.toAlgCat).symm)

@[implicit_reducible]

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)

The standard scalar action on 1 × 1 matrices.

Equations

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

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

The algebra equivalence between 1 × 1 matrices and the coefficient algebra.

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 (matrixA 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

The Kronecker product algebra homomorphism on square matrices.

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.matrixEqv {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

The tensor product of matrix algebras is a matrix algebra on the product index type.

Equations

• BrauerGroup.matrixEqv 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 (oneMulIn n A)

theorem BrauerGroup.mul_one {K : Type u} [Field K] (n : ℕ) [hn : NeZero n] (A : CSA K) : IsBrauerEquivalent A (mulOneIn 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.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)

Kronecker-style equivalence for tensor products of matrix algebras over two algebras.

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)

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

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

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

noncomputable def BrauerGroup.matrixEquivMatrixMopAlgebra (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)

@[implicit_reducible]

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

Equations

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

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

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

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

@[implicit_reducible]

noncomputable instance BrauerGroup.BruaerGroup {K : Type u} [Field K] : Group (BrauerGroup K)

Equations

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

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

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

@[implicit_reducible]

noncomputable instance BrauerGroup.instUniqueOfIsAlgClosedLeanPool {K : Type u} [Field K] [IsAlgClosed K] : Unique (BrauerGroup K)

Equations

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

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

noncomputable def BrauerGroupHom.someEquivs.baseChangeTensorLinear {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)

The linear equivalence underlying compatibility of scalar extension with tensor products.

Equations

• BrauerGroupHom.someEquivs.baseChangeTensorLinear A B = (TensorProduct.AlgebraTensorModule.cancelBaseChange K E E (TensorProduct K E A) B).trans ↑(Algebra.TensorProduct.assoc K K E E A B)

theorem BrauerGroupHom.someEquivs.baseChangeTensorLinear_tmul {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 e' : E) (a : A) (b : B) : (baseChangeTensorLinear A B) (e ⊗ₜ[K] a ⊗ₜ[E] (e' ⊗ₜ[K] b)) = (e * e') ⊗ₜ[K] (a ⊗ₜ[K] b)

Evaluates the scalar-extension tensor compatibility equivalence on pure tensors.

noncomputable def BrauerGroupHom.someEquivs.baseChangeTensorEquiv {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)

Scalar extension is compatible with tensor products of algebras.

Equations

• BrauerGroupHom.someEquivs.baseChangeTensorEquiv A B = AlgEquiv.ofLinearEquiv (BrauerGroupHom.someEquivs.baseChangeTensorLinear A B) ⋯ ⋯

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

If the matrix index is empty, the scalar-extension tensor source is subsingleton.

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

The algebra homomorphism underlying e3.

Equations

• BrauerGroupHom.someEquivs.e3Aux4 A m = ↑(BrauerGroupHom.someEquivs.baseChangeTensorEquiv A (Matrix (Fin m) (Fin m) K))

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)

The algebra homomorphism underlying e3 is surjective.

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)

Rewrites matrices over a scalar extension as a tensor product with matrices over the extension.

Equations

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

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

Replaces matrices over the extension field by scalar extension of matrices over K.

Equations

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

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 : ℕ) : 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))

Reassociates a tensor product after base change along K → E.

Equations

• BrauerGroupHom.someEquivs.e3 A m = BrauerGroupHom.someEquivs.baseChangeTensorEquiv A (Matrix (Fin m) (Fin m) K)

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)

Applies the matrix-tensor equivalence inside a scalar extension.

Equations

• BrauerGroupHom.someEquivs.e4 A m = Algebra.TensorProduct.congr AlgEquiv.refl (matrixEquivTensor (Fin m) K A).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

Extends an algebra equivalence by scalars from K to E.

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)

The algebra homomorphism underlying scalar-extension compatibility with tensor products.

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] : TensorProduct E (TensorProduct K E A) (TensorProduct K E B) ≃ₐ[E] TensorProduct K E (TensorProduct K A B)

Scalar extension is compatible with tensor products of algebras.

Equations

• BrauerGroupHom.someEquivs.e6 A B = BrauerGroupHom.someEquivs.baseChangeTensorEquiv 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

The base field scalar extension E ⊗[K] K is equivalent to E.

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 K →* BrauerGroup E

The Brauer group homomorphism induced by scalar extension from K to E.

Equations

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

@[reducible, inline]

noncomputable abbrev BrauerGroupHom.BaseChangeQToC : BrauerGroup ℚ →* BrauerGroup ℂ

The scalar extension homomorphism from the rational Brauer group to the complex Brauer group.

Equations

• BrauerGroupHom.BaseChangeQToC = BrauerGroupHom.BaseChange

theorem BrauerGroupHom.BaseChangeQToC_eq_one : BaseChangeQToC = 1

@[implicit_reducible]

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

Equations

• BrauerGroupHom.IsAbelBrauer = { toGroup := BrauerGroup.BruaerGroup, mul_comm := ⋯ }

noncomputable def BrauerGroupHom.baseChangeIdem.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.toAlgCat) ≃ₗ[E] TensorProduct F E ↑A.toAlgCat

The linear equivalence comparing two-step and one-step scalar extension.

Equations

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

@[simp]

theorem BrauerGroupHom.baseChangeIdem.Aux_apply (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) (x : TensorProduct K E (TensorProduct F K ↑A.toAlgCat)) : (Aux F K E A) x = (TensorProduct.AlgebraTensorModule.congr (TensorProduct.AlgebraTensorModule.rid K E E) (LinearEquiv.refl F ↑A.toAlgCat)) ((TensorProduct.AlgebraTensorModule.assoc F K E E K ↑A.toAlgCat).symm x)

@[simp]

theorem BrauerGroupHom.baseChangeIdem.Aux_symm_apply (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) (a✝ : TensorProduct F E ↑A.toAlgCat) : (Aux F K E A).symm a✝ = (TensorProduct.AlgebraTensorModule.assoc F K E E K ↑A.toAlgCat) ((TensorProduct.AlgebraTensorModule.congr (TensorProduct.AlgebraTensorModule.rid K E E) (LinearEquiv.refl F ↑A.toAlgCat)).symm a✝)

noncomputable def BrauerGroupHom.baseChangeIdem.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.toAlgCat) ≃ₐ[E] TensorProduct F E ↑A.toAlgCat

The algebra equivalence comparing two-step and one-step scalar extension.

Equations

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

theorem BrauerGroupHom.baseChangeIdem (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 CommGrpCat

The Brauer group functor from fields to commutative groups.

Equations

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