Merge branch 'main' of https://github.com/Whysoserioushah/BrauerGroup…

…_new
Whysoserioushah · Aug 23, 2024 · e43326d · e43326d
2 parents 77f07a1 + 06b4be9
commit e43326d
Show file tree

Hide file tree

Showing 15 changed files with 27 additions and 25 deletions.
diff --git a/BrauerGroup/074E.lean b/BrauerGroup/074E.lean
@@ -1,8 +1,6 @@
 import BrauerGroup.Wedderburn
-import BrauerGroup.BrauerGroup
 
 import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
-import Mathlib.Algebra.Category.ModuleCat.Adjunctions
 import Mathlib.FieldTheory.Finiteness
 import Mathlib.Algebra.Algebra.Basic
 import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
@@ -353,8 +351,7 @@ lemma linearEquiv_iff_finrank_eq_over_simple_ring
     haveI : Module.Finite k (ι →₀ S) := Module.Finite.equiv ISO
     haveI : Module.Finite k (ι' →₀ S) := Module.Finite.equiv ISO'
     haveI : Module.Finite k S := by
-      suffices : IsNoetherian k S
-      · infer_instance
+      suffices IsNoetherian k S from inferInstance
       rw [IsNoetherian.iff_rank_lt_aleph0]
       apply_fun ((↑) : ℕ → Cardinal) at eq
       rw [finrank_eq_rank, finrank_eq_rank, rank_finsupp] at eq
@@ -377,8 +374,7 @@ lemma linearEquiv_iff_finrank_eq_over_simple_ring
       simp only [Cardinal.lift_id] at ineq
       have ineq2 := @Cardinal.le_mul_left (Cardinal.mk ι) (Module.rank k S)
         (by
-          suffices : 0 < Module.rank k S
-          · exact Ne.symm (ne_of_lt this)
+          suffices 0 < Module.rank k S by exact Ne.symm (ne_of_lt this)
           apply rank_pos)
       rw [mul_comm] at ineq2
       exact lt_of_le_of_lt ineq2 ineq
@@ -393,8 +389,8 @@ lemma linearEquiv_iff_finrank_eq_over_simple_ring
       simp only [Cardinal.lift_id] at ineq
       have ineq2 := @Cardinal.le_mul_left (Cardinal.mk ι') (Module.rank k S)
         (by
-          suffices : 0 < Module.rank k S
-          · exact Ne.symm (ne_of_lt this)
+          suffices 0 < Module.rank k S from
+            Ne.symm (ne_of_lt this)
           apply rank_pos)
       rw [mul_comm] at ineq2
       exact lt_of_le_of_lt ineq2 ineq

diff --git a/BrauerGroup/AlgClosedUnion.lean b/BrauerGroup/AlgClosedUnion.lean
@@ -1,4 +1,3 @@
-import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
 import Mathlib.LinearAlgebra.FiniteDimensional
 import Mathlib.RingTheory.Finiteness
 import Mathlib.RingTheory.Flat.Basic

diff --git a/BrauerGroup/BrauerGroup.lean b/BrauerGroup/BrauerGroup.lean
@@ -1,6 +1,9 @@
 import BrauerGroup.CentralSimple
 import BrauerGroup.Composition
 import Mathlib.LinearAlgebra.Matrix.ToLin
+import Mathlib.Analysis.Complex.Polynomial
+import Mathlib.LinearAlgebra.FreeModule.PID
+import Mathlib.LinearAlgebra.Matrix.FiniteDimensional
 
 
 suppress_compilation

diff --git a/BrauerGroup/Con.lean b/BrauerGroup/Con.lean
@@ -1,4 +1,8 @@
-import Mathlib.Tactic
+import Mathlib.Algebra.CharP.Defs
+import Mathlib.Algebra.Module.Opposites
+import Mathlib.LinearAlgebra.Alternating.Basic
+import Mathlib.RingTheory.Congruence.Basic
+import Mathlib.RingTheory.Ideal.Basic
 
 variable {M : Type*} [AddCommMonoid M] (r : AddCon M) {ι : Type*} (s : Finset ι)
 variable {R : Type*} [Ring R] (t : RingCon R)

diff --git a/BrauerGroup/Lemmas.lean b/BrauerGroup/Lemmas.lean
@@ -1,5 +1,5 @@
 import Mathlib.RingTheory.TensorProduct.Basic
-import BrauerGroup.BrauerGroup
+import BrauerGroup.CentralSimple
 
 universe u
 

diff --git a/BrauerGroup/MoritaEquivalence.lean b/BrauerGroup/MoritaEquivalence.lean
@@ -1,5 +1,4 @@
 import Mathlib.Algebra.Category.ModuleCat.Abelian
-import Mathlib.LinearAlgebra.Matrix.FiniteDimensional
 import Mathlib.CategoryTheory.Elementwise
 import Mathlib.Algebra.Module.LinearMap.End
 import Mathlib.RingTheory.SimpleModule

diff --git a/BrauerGroup/PiTensorProduct.lean b/BrauerGroup/PiTensorProduct.lean
@@ -1,5 +1,7 @@
 import Mathlib.LinearAlgebra.PiTensorProduct
-import BrauerGroup.Dual
+import Mathlib.GroupTheory.MonoidLocalization
+import Mathlib.LinearAlgebra.Finsupp
+import Mathlib.Algebra.Algebra.Basic
 
 suppress_compilation
 

diff --git a/BrauerGroup/Profinite/Basic.lean b/BrauerGroup/Profinite/Basic.lean
@@ -1,6 +1,6 @@
-import Mathlib.Topology.Category.Profinite.AsLimit
 import Mathlib.Topology.ContinuousFunction.Basic
-import Mathlib.Algebra.Category.Grp.FilteredColimits
+import Mathlib.Algebra.Category.Grp.Basic
+import Mathlib.Topology.Category.Profinite.Basic
 
 /-!
 

diff --git a/BrauerGroup/QuadraticExtension.lean b/BrauerGroup/QuadraticExtension.lean
@@ -1,5 +1,4 @@
-import Mathlib.NumberTheory.Zsqrtd.Basic
-import Mathlib.Tactic
+import Mathlib.Analysis.RCLike.Basic
 
 suppress_compilation
 

diff --git a/BrauerGroup/QuatBasic.lean b/BrauerGroup/QuatBasic.lean
@@ -1,7 +1,9 @@
 import Mathlib.Algebra.QuaternionBasis
 import BrauerGroup.QuadraticExtension
 import BrauerGroup.Con
-import Mathlib.Tactic
+import Mathlib.LinearAlgebra.FiniteDimensional
+import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
+import Mathlib.RingTheory.Valuation.ValuationRing
 
 suppress_compilation
 

diff --git a/BrauerGroup/Quaternion.lean b/BrauerGroup/Quaternion.lean
@@ -1,5 +1,7 @@
 import BrauerGroup.QuatBasic
-import BrauerGroup.BrauerGroup
+import BrauerGroup.CentralSimple
+import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.LinearAlgebra.FreeModule.PID
 
 suppress_compilation
 

diff --git a/BrauerGroup/SkolemNoether.lean b/BrauerGroup/SkolemNoether.lean
@@ -1,7 +1,5 @@
 import BrauerGroup.BrauerGroup
 import BrauerGroup.«074E»
-import BrauerGroup.MatrixCenterEquiv
-import BrauerGroup.Lemmas
 
 suppress_compilation
 

diff --git a/BrauerGroup/SplitDirect.lean b/BrauerGroup/SplitDirect.lean
@@ -1,8 +1,6 @@
 import Mathlib.LinearAlgebra.FiniteDimensional
-import Mathlib.FieldTheory.IsSepClosed
 import BrauerGroup.BrauerGroup
 import BrauerGroup.ExtendScalar
-import BrauerGroup.Quaternion
 
 namespace split_direct
 

diff --git a/BrauerGroup/SplittingOfCSA.lean b/BrauerGroup/SplittingOfCSA.lean
@@ -4,7 +4,6 @@ import BrauerGroup.AlgClosedUnion
 import BrauerGroup.ExtendScalar
 import Mathlib.LinearAlgebra.Dimension.Constructions
 import Mathlib.LinearAlgebra.Dimension.Finrank
-import Mathlib.FieldTheory.IsSepClosed
 
 suppress_compilation
 
@@ -13,7 +12,7 @@ variable (k A K: Type u) [Field k] [Field K] [Algebra k K] [Ring A]
   [Algebra k A]
 
 variable (k_bar : Type u) [Field k_bar] [Algebra k k_bar] [hk_bar : IsAlgClosure k k_bar]
-  (k_s : Type u) [Field k_s] [Algebra k k_s] [IsSepClosure k k_s]
+  (k_s : Type u) [Field k_s] [Algebra k k_s] --[IsSepClosure k k_s]
 
 open scoped TensorProduct
 open RingCon

diff --git a/BrauerGroup/Wedderburn.lean b/BrauerGroup/Wedderburn.lean
@@ -5,6 +5,7 @@ import Mathlib.Algebra.Ring.Equiv
 import Mathlib.LinearAlgebra.Matrix.IsDiag
 
 import BrauerGroup.MoritaEquivalence
+import Mathlib.FieldTheory.IsAlgClosed.Basic
 
 variable (A : Type*) [Ring A]