LeanPool.BrauerGroupNew.Azumaya.Basic

Imported Lean Pool material for LeanPool.BrauerGroupNew.Azumaya.Basic.

theorem TensorProduct.flip_mk_injective {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [NoZeroSMulDivisors R N] [Module.Flat R M] (a : N) (ha : a ≠ 0) : Function.Injective ⇑((mk R M N).flip a)

theorem IsCentral.left_of_tensor (K : Type u) [Field K] (B : Type u_1) (C : Type u_2) [Ring B] [Ring C] [Nontrivial B] [Nontrivial C] [Algebra K C] [Algebra K B] [FiniteDimensional K B] [hbc : Algebra.IsCentral K (TensorProduct K B C)] : Algebra.IsCentral K B

theorem Algebra.IsCentral_ofAlgEquiv (K : Type u) [Field K] (A : Type u_1) (B : Type u_2) [Ring A] [Ring B] [Algebra K A] [Algebra K B] (e : A ≃ₐ[K] B) (hA : IsCentral K A) : IsCentral K B

theorem IsSimpleRing.ofAlgEquiv (K : Type u) [Field K] (A : Type u_1) (B : Type u_2) [Ring A] [Ring B] [Algebra K A] [Algebra K B] (e : A ≃ₐ[K] B) (hA : IsSimpleRing A) : IsSimpleRing B

theorem IsAzumaya_iff_CentralSimple (K : Type u) [Field K] (A : Type u) [Ring A] [Algebra K A] [Nontrivial A] : IsAzumaya K A ↔ FiniteDimensional K A ∧ Algebra.IsCentral K A ∧ IsSimpleRing A

def finswap {n m : ℕ} : Fin (n * m) ≃ Fin (m * n)

The canonical equivalence Fin (n * m) ≃ Fin (m * n) induced by commutativity.

Equations

• finswap = { toFun := fun (i : Fin (n * m)) => ⟨↑i, ⋯⟩, invFun := fun (i : Fin (m * n)) => ⟨↑i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem IsMorita_iff_IsBrauer' (R : Type u) [CommRing R] (A B : Type v) [Ring A] [Ring B] [IsSimpleRing A] [IsSimpleRing B] [IsArtinianRing A] [IsArtinianRing B] [Algebra R A] [Algebra R B] : IsMoritaEquivalent R A B ↔ ∃ (n : ℕ) (m : ℕ), n ≠ 0 ∧ m ≠ 0 ∧ Nonempty (Matrix (Fin n) (Fin n) A ≃ₐ[R] Matrix (Fin m) (Fin m) B)

theorem IsMorita_iff_IsBrauer (K : Type u) [Field K] (A B : CSA K) : IsMoritaEquivalent K ↑A.toAlgCat ↑B.toAlgCat ↔ IsBrauerEquivalent A B

instance instFaithfulSMulMatrixFinOfNeZeroNat_leanPool (R : Type u) [CommRing R] (n : ℕ) [NeZero n] : FaithfulSMul R (Matrix (Fin n) (Fin n) R)

@[reducible, inline]

abbrev matrixAlgEquivMatrixMop (R : Type u) [CommRing R] (n : ℕ) : Matrix (Fin n) (Fin n) R ≃ₐ[R] (Matrix (Fin n) (Fin n) R)ᵐᵒᵖ

The matrix algebra is equivalent to its opposite algebra over the base ring.

Equations

• matrixAlgEquivMatrixMop R n = (AlgEquiv.toOpposite R R).mapMatrix.trans (AlgEquiv.ofRingEquiv ⋯)

@[reducible, inline]

noncomputable abbrev mopAlgEquivEnd (R : Type u) [CommRing R] : Rᵐᵒᵖ ≃ₐ[R] Module.End R R

The opposite algebra of R identifies with the endomorphism algebra of R as a module.

Equations

• mopAlgEquivEnd R = AlgEquiv.ofRingEquiv ⋯

@[reducible, inline]

noncomputable abbrev tensorEquivEnd (R : Type u) [CommRing R] : TensorProduct R R Rᵐᵒᵖ ≃ₐ[R] Module.End R R

The tensor product R ⊗[R] Rᵐᵒᵖ identifies with Module.End R R.

Equations

• tensorEquivEnd R = (Algebra.TensorProduct.lid R Rᵐᵒᵖ).trans (mopAlgEquivEnd R)

theorem equal_mulLeftRight (R : Type u) [CommRing R] : ↑(tensorEquivEnd R) = AlgHom.mulLeftRight R R

theorem bij_Rtensor (R : Type u) [CommRing R] : Function.Bijective ⇑(AlgHom.mulLeftRight R R)

instance instFaithfulSMul_leanPool (R : Type u) [CommRing R] : FaithfulSMul R R

theorem IsAzumaya_R (R : Type u) [CommRing R] : IsAzumaya R R

@[reducible, inline]

abbrev Mat.inv (R : Type u) [CommRing R] (n : ℕ) : Module.End R (Matrix (Fin n) (Fin n) R) →ₗ[R] TensorProduct R (Matrix (Fin n) (Fin n) R) (Matrix (Fin n) (Fin n) R)ᵐᵒᵖ

An explicit inverse to AlgHom.mulLeftRight for matrix algebras.

Equations

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

theorem single.eq (R : Type u) [CommRing R] (n : ℕ) (i j : Fin n) : Matrix.single i j 1 = Matrix.of fun (i' j' : Fin n) => if i = i' ∧ j = j' then 1 else 0

theorem Mat.inv_toFun1' (R : Type u) [CommRing R] (n : ℕ) : inv R n ∘ₗ (AlgHom.mulLeftRight R (Matrix (Fin n) (Fin n) R)).toLinearMap = LinearMap.id

theorem Mat.inv_toFun2' (R : Type u) [CommRing R] (n : ℕ) : (AlgHom.mulLeftRight R (Matrix (Fin n) (Fin n) R)).toLinearMap ∘ₗ inv R n = LinearMap.id

theorem Mat.bij (R : Type u) [CommRing R] (n : ℕ) : Function.Bijective ⇑(AlgHom.mulLeftRight R (Matrix (Fin n) (Fin n) R))

instance instFaithfulSMulMatrixFinOfNeZeroNat_leanPool_1 (R : Type u) [CommRing R] (n : ℕ) [NeZero n] : FaithfulSMul R (Matrix (Fin n) (Fin n) R)