[Merged by Bors] - feat(Mathlib/Algebra/BrauerGroup/Defs): define Brauer Equivalence and Brauer Group

[Whysoserioushah]

co-authored by: @jjaassoonn

---

[github-actions]

PR summary ba507b2bfb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.BrauerGroup.Defs (new file)	1352

---

Declarations diff

+ Brauer.CSA_Setoid:
+ BrauerGroup
+ CSA
+ IsBrauerEquivalent
+ instance : CoeSort (CSA.{u, v} K) (Type v) := ⟨(·.carrier)⟩
+ is_eqv
+ refl
+ symm
+ trans

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[alreadydone]

For this we do need to use the notion of Morita equivalence over a base field/commutative ring, which is now in #20632: see https://mathoverflow.net/questions/344673/are-azumaya-algebras-of-trivial-brauer-class-isomorphic-to-mathcalend-mathc#comment1183423_344684

[Whysoserioushah]

the official PR is actually #20640, I have a WIP branch on mathlib called azumaya_wip that's gonna be about proving azumaya algebras on fields aare indeed central simple algebras but a lot prerequists are yet to implement,
optimistically speaking that part of content is about 2-3 PRs away?

[Whysoserioushah]

equivalency of Azumaya and CSA sorry-freed! Next step is to prove Morita iff BrauerEquivalent over field!

[jcommelin]

I'm inclined to wait with this PR for a little time while mathlib learns more about Azumaya algebras. Because I imagine that most of this file will have to be rewritten anyways once you have Morita equivalence for Azumaya algebras available.

[Whysoserioushah]

No I think my current plan is (because I have lots of materials on CSA and BrauerGroup awaiting PR) to PR only about fields and I'm proving over fields this is equivalent to azumaya algebra and morita equivalence if that's okay

[jcommelin]

Ok, let's go for it.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style