Skip to content

Import brauergroup_new formalization #88

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Vilin97 merged 38 commits into from
Jun 1, 2026
Merged

Import brauergroup_new formalization #88

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
38 commits
Select commit Hold shift + click to select a range
bf80767
Vendor Brauer group core
Vilin97 May 17, 2026
ce6d0f0
Merge branch 'main' into import/brauergroup_new
Vilin97 May 18, 2026
971b78b
Add Brauer group source citation
Vilin97 May 18, 2026
a56d88f
Regenerate project card
Vilin97 May 18, 2026
14c2b52
Add Brauer group core
Vilin97 May 19, 2026
020f677
Narrow Brauer group source scope
Vilin97 May 19, 2026
e8ef5ac
Merge origin/main into import/brauergroup_new
Vilin97 May 19, 2026
68df6f3
Restore BrauerGroup finite-field theorem
Vilin97 May 20, 2026
d849a45
Merge remote-tracking branch 'origin/main' into import/brauergroup_new
Vilin97 May 21, 2026
e471ca7
Add BrauerGroup upstream repository metadata
Vilin97 May 24, 2026
615ae54
Restore BrauerGroup upstream helper files
Vilin97 May 24, 2026
1c3f64b
Restore BrauerGroup Morita equivalence
Vilin97 May 24, 2026
649db4d
Restore BrauerGroup splitting prerequisites
Vilin97 May 24, 2026
50a106f
Restore BrauerGroup helper compatibility modules
Vilin97 May 24, 2026
a82b595
Port BrauerGroup ZeroSevenFourE
Vilin97 May 24, 2026
e937e58
Port BrauerGroup Skolem-Noether
Vilin97 May 24, 2026
b4642f2
Port BrauerGroup double centralizer
Vilin97 May 24, 2026
8910b16
Port BrauerGroup maximal subfields
Vilin97 May 24, 2026
23158bc
Port relative Brauer group
Vilin97 May 24, 2026
06f9aab
Port BrauerGroup subfield splitting
Vilin97 May 24, 2026
daac4e1
Port BrauerGroup cross product algebra
Vilin97 May 24, 2026
032d6f2
Port BrauerGroup Morita change of rings
Vilin97 May 24, 2026
8f3190a
Port BrauerGroup Azumaya basics
Vilin97 May 24, 2026
9aa75f4
Port BrauerGroup Azumaya multiplication
Vilin97 May 24, 2026
01933f8
Fix BrauerGroup Azumaya warning-free build
Vilin97 May 24, 2026
cc173b4
Port BrauerGroup Morita tensor product
Vilin97 May 24, 2026
08d7bfe
Port BrauerGroup ShortComplex homology example
Vilin97 May 24, 2026
1ce8ea6
Port BrauerGroup second cohomology equivalence
Vilin97 May 25, 2026
bb8843d
Port BrauerGroup additive cohomology isomorphism
Vilin97 May 25, 2026
275547d
Port BrauerGroup Frobenius theorem
Vilin97 May 25, 2026
a415b60
Port BrauerGroup separable subfields
Vilin97 May 25, 2026
02c6f33
Port BrauerGroup real and absolute results
Vilin97 May 25, 2026
4dc2d5b
Restore BrauerGroup compatibility declarations
Vilin97 May 25, 2026
9d7c140
Restore BrauerGroup congruence compatibility import
Vilin97 May 25, 2026
5e9435c
Restore BrauerGroup tensor compatibility helper
Vilin97 May 25, 2026
1b75fcf
Use Mathlib span compatibility theorem
Vilin97 May 25, 2026
8445168
Clean BrauerGroup separable subfield warnings
Vilin97 May 25, 2026
b2b05d5
Merge remote-tracking branch 'origin/main' into tmp-brauergroup_new
Vilin97 Jun 1, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
78 changes: 78 additions & 0 deletions LeanPool.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,84 @@ import LeanPool.ArtinWedderburn.NonUnitalToUnital
import LeanPool.ArtinWedderburn.PrimeRing
import LeanPool.ArtinWedderburn.SetProd
import LeanPool.Basic
import LeanPool.BrauerGroupNew
import LeanPool.BrauerGroupNew.AbsoluteIsoH2
import LeanPool.BrauerGroupNew.AlgClosedUnion
import LeanPool.BrauerGroupNew.Azumaya.Basic
import LeanPool.BrauerGroupNew.Azumaya.Mul
import LeanPool.BrauerGroupNew.BrauerGroup
import LeanPool.BrauerGroupNew.BrauerOverR
import LeanPool.BrauerGroupNew.CentralSimple
import LeanPool.BrauerGroupNew.Centralizer
import LeanPool.BrauerGroupNew.CrossProductAlgebra
import LeanPool.BrauerGroupNew.DoubleCentralizer
import LeanPool.BrauerGroupNew.Examples.ShortComplex.LeftHomologyMapData
import LeanPool.BrauerGroupNew.ExtendScalar
import LeanPool.BrauerGroupNew.FieldCat
import LeanPool.BrauerGroupNew.FiniteField
import LeanPool.BrauerGroupNew.FrobeniusTheorem
import LeanPool.BrauerGroupNew.IsoSecond
import LeanPool.BrauerGroupNew.LemmasAboutSimpleRing
import LeanPool.BrauerGroupNew.Mathlib
import LeanPool.BrauerGroupNew.Mathlib.Algebra
import LeanPool.BrauerGroupNew.Mathlib.Algebra.Algebra
import LeanPool.BrauerGroupNew.Mathlib.Algebra.Algebra.Equiv
import LeanPool.BrauerGroupNew.Mathlib.Algebra.Algebra.Subalgebra
import LeanPool.BrauerGroupNew.Mathlib.Algebra.Algebra.Subalgebra.Basic
import LeanPool.BrauerGroupNew.Mathlib.Algebra.Algebra.Subalgebra.Directed
import LeanPool.BrauerGroupNew.Mathlib.Algebra.Algebra.Subalgebra.Lattice
import LeanPool.BrauerGroupNew.Mathlib.Data
import LeanPool.BrauerGroupNew.Mathlib.Data.DFinsupp
import LeanPool.BrauerGroupNew.Mathlib.Data.DFinsupp.Submonoid
import LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra
import LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.LinearIndependent
import LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.LinearIndependent.Defs
import LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Matrix
import LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Matrix.Charpoly
import LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
import LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup
import LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
import LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Span
import LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Span.Basic
import LeanPool.BrauerGroupNew.Mathlib.RepresentationTheory
import LeanPool.BrauerGroupNew.Mathlib.RepresentationTheory.Homological
import LeanPool.BrauerGroupNew.Mathlib.RepresentationTheory.Homological.GroupCohomology
import LeanPool.BrauerGroupNew.Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
import LeanPool.BrauerGroupNew.Mathlib.RingTheory
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.Congruence
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.Congruence.Basic
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.Congruence.Defs
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.MatrixAlgebra
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubring
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubring.Defs
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubsemiring
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubsemiring.Basic
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubsemiring.Defs
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.TensorProduct
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.TensorProduct.Basic
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Basic
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Kernel
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Lattice
import LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Operations
import LeanPool.BrauerGroupNew.MatrixCenterEquiv
import LeanPool.BrauerGroupNew.MatrixEquivTensor
import LeanPool.BrauerGroupNew.Morita.ChangeOfRings
import LeanPool.BrauerGroupNew.Morita.TensorProduct
import LeanPool.BrauerGroupNew.MoritaEquivalence
import LeanPool.BrauerGroupNew.RelativeBrauer
import LeanPool.BrauerGroupNew.SkolemNoether
import LeanPool.BrauerGroupNew.SplittingOfCSA
import LeanPool.BrauerGroupNew.Subfield
import LeanPool.BrauerGroupNew.Subfield.Defs
import LeanPool.BrauerGroupNew.Subfield.FiniteDimensional
import LeanPool.BrauerGroupNew.Subfield.Separable
import LeanPool.BrauerGroupNew.Subfield.Splitting
import LeanPool.BrauerGroupNew.Subfield.Subfield
import LeanPool.BrauerGroupNew.ToSecond
import LeanPool.BrauerGroupNew.TwoSidedIdeal
import LeanPool.BrauerGroupNew.Wedderburn
import LeanPool.BrauerGroupNew.ZeroSevenFourE
import LeanPool.BruhatTits
import LeanPool.BruhatTits.Cartan
import LeanPool.BruhatTits.Cartan.Existence
Expand Down
48 changes: 48 additions & 0 deletions LeanPool/BrauerGroupNew.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
/-
Copyright (c) 2026 Yunzhou Xie and contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yunzhou Xie, Yichen Feng, Jujian Zhang, Yael Dillies
-/

import LeanPool.BrauerGroupNew.CentralSimple
import LeanPool.BrauerGroupNew.Centralizer
import LeanPool.BrauerGroupNew.CrossProductAlgebra
import LeanPool.BrauerGroupNew.ExtendScalar
import LeanPool.BrauerGroupNew.Azumaya.Basic
import LeanPool.BrauerGroupNew.Azumaya.Mul
import LeanPool.BrauerGroupNew.Examples.ShortComplex.LeftHomologyMapData
import LeanPool.BrauerGroupNew.FieldCat
import LeanPool.BrauerGroupNew.AlgClosedUnion
import LeanPool.BrauerGroupNew.FiniteField
import LeanPool.BrauerGroupNew.BrauerGroup
import LeanPool.BrauerGroupNew.LemmasAboutSimpleRing
import LeanPool.BrauerGroupNew.MatrixCenterEquiv
import LeanPool.BrauerGroupNew.MatrixEquivTensor
import LeanPool.BrauerGroupNew.Morita.ChangeOfRings
import LeanPool.BrauerGroupNew.Morita.TensorProduct
import LeanPool.BrauerGroupNew.MoritaEquivalence
import LeanPool.BrauerGroupNew.SplittingOfCSA
import LeanPool.BrauerGroupNew.TwoSidedIdeal
import LeanPool.BrauerGroupNew.Wedderburn
import LeanPool.BrauerGroupNew.ZeroSevenFourE
import LeanPool.BrauerGroupNew.RelativeBrauer
import LeanPool.BrauerGroupNew.SkolemNoether
import LeanPool.BrauerGroupNew.ToSecond
import LeanPool.BrauerGroupNew.IsoSecond
import LeanPool.BrauerGroupNew.AbsoluteIsoH2
import LeanPool.BrauerGroupNew.DoubleCentralizer
import LeanPool.BrauerGroupNew.FrobeniusTheorem
import LeanPool.BrauerGroupNew.BrauerOverR
import LeanPool.BrauerGroupNew.Mathlib
import LeanPool.BrauerGroupNew.Subfield

/-!
# Brauer Group Core

Source: url:https://doi.org/10.1017/9781107359419
Authors: Yunzhou Xie, Yichen Feng, Jujian Zhang, Yael Dillies
Status: verified
Main declarations: `BrauerGroup.Bruaer_Group`, `BrauerGroupHom.Br`, `Wedderburn_Artin`
Tags: algebra, ring-theory, central-simple-algebras, brauer-groups
MSC: 16K20, 16K50, 16S35
-/
10 changes: 10 additions & 0 deletions LeanPool/BrauerGroupNew/AbsoluteIsoH2.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
/-
Copyright (c) 2026 Yunzhou Xie and contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yunzhou Xie, Yichen Feng, Jujian Zhang, Yael Dillies
-/

import LeanPool.BrauerGroupNew.IsoSecond
import Mathlib.FieldTheory.IsSepClosed

variable (F F_star : Type) [Field F] [Field F_star] [Algebra F F_star] [IsSepClosure F F_star]
Loading
Loading