Benchmark / BrauerGroup

BrauerGroup: Mathlib v4.32.0 → v4.35.0

Partial: 12 modules repaired, 2 still red when the time box ended. The bump spans 3 Mathlib releases and produced 33 raw build errors in 4 files; an alias rewrite resolves 0 of them.

Project: Whysoserioushah/BrauerGroup. First build after the bump: 148.4 s, 46 deprecation warnings (41 with a replacement an alias rewrite would apply).

Partial. 12 modules repaired in about 160 minutes of agent time; still red:

Subfield/Separable (ZCL_equiv_ZCL_map injectivity; an Algebra instance mismatch between Subring.center and Subalgebra.center K of a centralizer at line ~365)
ToSecond (a rewrite that now needs ρ * σ * τ vs ρ * (σ * τ) in a conjFactor type; H2π applied to a cocycle of Rep.ofMulDistribMulAction vs galAct F K)

The diff

Work in progress when the time box ended; the build is still red.

diff --git a/BrauerGroup/AlgClosedUnion.lean b/BrauerGroup/AlgClosedUnion.lean

index e3c5cf8..7f74091 100644

--- a/BrauerGroup/AlgClosedUnion.lean

+++ b/BrauerGroup/AlgClosedUnion.lean

@@ -1,6 +1,7 @@

module

public import Mathlib.FieldTheory.IsAlgClosed.Basic

+public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

public import Mathlib.RingTheory.Flat.Basic

public import Mathlib.RingTheory.TensorProduct.Free

diff --git a/BrauerGroup/Azumaya/Basic.lean b/BrauerGroup/Azumaya/Basic.lean

index 0b1703f..fce80eb 100644

--- a/BrauerGroup/Azumaya/Basic.lean

+++ b/BrauerGroup/Azumaya/Basic.lean

@@ -57,15 +57,14 @@ lemma IsCentral.left_of_tensor (B C : Type*)

map_zero' := by ext; simp

map_add' := fun _ _ ↦ by ext; simp [add_tmul]

commutes' := fun _ ↦ rfl}

- have f_surj : Function.Surjective f := fun ⟨bc, ⟨b, hb⟩, h⟩ ↦ ⟨⟨b, hb⟩, by simpa [f] using h⟩

+ have f_surj : Function.Surjective f := fun ⟨bc, ⟨b, hb⟩, h⟩ ↦ ⟨⟨b, hb⟩, Subtype.ext h⟩

have e : ((Algebra.TensorProduct.includeLeft (R := K) (B := C)).comp

(Subalgebra.center K B).val).range ≃ₐ[K] (Subalgebra.center K B) :=

(AlgEquiv.ofBijective f

⟨fun ⟨b1, hb1⟩ ⟨b2, hb2⟩ h12 ↦ by

- simp only [AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,

- Subtype.mk.injEq, f] at h12

+ have h12' : b1 ⊗ₜ[K] (1 : C) = b2 ⊗ₜ[K] (1 : C) := congrArg Subtype.val h12

ext

- exact TensorProduct.flip_mk_injective _ one_ne_zero h12,

+ exact TensorProduct.flip_mk_injective (R := K) (1 : C) one_ne_zero h12',

f_surj⟩).symm

have e2 := Subalgebra.equivOfEq _ _ eq |>.trans <| Algebra.botEquiv K _

have ee: Subalgebra.center K B ≃ₐ[K] K := e.symm.trans e2

@@ -185,6 +184,7 @@ abbrev matrixAlgEquivMatrixMop (n : ℕ) :

noncomputable abbrev mopAlgEquivEnd : Rᵐᵒᵖ ≃ₐ[R] Module.End R R :=

AlgEquiv.ofRingEquiv (f := mopEquivEnd R) fun r ↦ by

ext; simp [mopEquivEnd]

+ erw [RingEquiv.ofBijective_apply]; simp

noncomputable abbrev tensorEquivEnd : R ⊗[R] Rᵐᵒᵖ ≃ₐ[R] Module.End R R :=

Algebra.TensorProduct.lid R Rᵐᵒᵖ|>.trans <| mopAlgEquivEnd R

@@ -192,6 +192,7 @@ noncomputable abbrev tensorEquivEnd : R ⊗[R] Rᵐᵒᵖ ≃ₐ[R] Module.End R

lemma equal_mulLeftRight : tensorEquivEnd R = AlgHom.mulLeftRight R R := by

ext r

simp [mopEquivEnd, AlgHom.mulLeftRight_apply]

+ erw [RingEquiv.ofBijective_apply]; simp

lemma bij_Rtensor : Function.Bijective (AlgHom.mulLeftRight R R) := by

rw [← equal_mulLeftRight]

diff --git a/BrauerGroup/Azumaya/Group.lean b/BrauerGroup/Azumaya/Group.lean

index 3f450d0..09acf02 100644

--- a/BrauerGroup/Azumaya/Group.lean

+++ b/BrauerGroup/Azumaya/Group.lean

@@ -28,7 +28,9 @@ abbrev Endmop (A : Type*) [Ring A] [Algebra R A] : Module.End R A →ₐ[R] Modu

abbrev EndmopEquiv (A : Type*) [Ring A] [Algebra R A] : Module.End R A ≃ₐ[R] Module.End R Aᵐᵒᵖ :=

AlgEquiv.ofBijective (Endmop R A) ⟨

- fun f1 f2 h ↦ by simpa using h, fun f ↦ ⟨(opLinearEquiv R).symm.toLinearMap ∘ₗ f ∘ₗ

+ fun f1 f2 h ↦ by

+ ext x

+ exact congrArg (fun g ↦ (g (MulOpposite.op x)).unop) h, fun f ↦ ⟨(opLinearEquiv R).symm.toLinearMap ∘ₗ f ∘ₗ

(opLinearEquiv R).toLinearMap, rfl⟩⟩

@@ -57,7 +59,13 @@ lemma Mopcomm_square (A : Type*) [Ring A] [Algebra R A] :

(Algebra.TensorProduct.congr (AlgEquiv.refl) (AlgEquiv.opOp R A).symm).toAlgHom) := by

ext a a'

· simp [-Algebra.lsmul_coe, AlgHom.mulLeftRight_apply]

+ erw [AlgEquiv.ofBijective_apply]

+ change a * a' = MulOpposite.op ((AlgHom.mulLeftRight R A (1 ⊗ₜ[R] a)) a'.unop)

+ simp [AlgHom.mulLeftRight_apply]

· simp [-Algebra.lsmul_coe, AlgHom.mulLeftRight_apply]

+ erw [AlgEquiv.ofBijective_apply]

+ change a' * a.unop = MulOpposite.op ((AlgHom.mulLeftRight R A (a.unop.unop ⊗ₜ[R] 1)) a'.unop)

+ simp [AlgHom.mulLeftRight_apply]

lemma mop_bij (A : Azumaya R) : Function.Bijective (AlgHom.mulLeftRight R Aᵐᵒᵖ) := by

rw [Mopcomm_square R A]

diff --git a/BrauerGroup/BrauerGroup.lean b/BrauerGroup/BrauerGroup.lean

index 804f9de..fb9a57a 100644

--- a/BrauerGroup/BrauerGroup.lean

+++ b/BrauerGroup/BrauerGroup.lean

@@ -323,11 +323,8 @@ lemma matrixEquivForward_surjective

simp only [matrixEquivForward, Algebra.TensorProduct.algHomOfLinearMapTensorProduct_apply,

TensorProduct.lift.tmul]

ext a b

- erw [Matrix.kroneckerMapBilinear_apply_apply]

- erw [Matrix.kroneckerMap_apply]

- erw [Algebra.coe_lmul_eq_mul]

- rw [LinearMap.mul]

- simp only [LinearMap.mk₂_apply]

+ change Matrix.kroneckerMap (· * ·) (Matrix.single i.1 j.1 (1 : K)) (Matrix.single i.2 j.2 (1 : K)) a b = _

+ rw [Matrix.kroneckerMap_apply]

simp only [Matrix.single, Matrix.of_apply, mul_ite, mul_one, mul_zero]

split_ifs with h1 h2 h3 h4 h5

· rfl

@@ -767,14 +764,16 @@ def e6Aux0 : (E ⊗[K] A) ⊗[E] (E ⊗[K] B) →ₐ[E] E ⊗[K] (A ⊗[K] B) :=

| zero => simp only [map_zero, zero_mul, mul_zero]

| add x x' hx hx' => simp only [map_add, mul_add, hx, hx', add_mul]

| tmul e a =>

- simp only [Algebra.TensorProduct.lift_tmul, AlgHom.coe_mk, RingHom.coe_mk]

+ erw [Algebra.TensorProduct.lift_tmul]

induction y using TensorProduct.induction_on with

| zero => simp only [map_zero, mul_zero, zero_mul]

| add y y' hy hy' => simp only [map_add, mul_add, hy, hy', add_mul]

| tmul e' b =>

- simp only [Algebra.TensorProduct.lift_tmul, AlgHom.coe_mk, RingHom.coe_mk]

- change (_ ⊗ₜ _) * (_ ⊗ₜ _) * ((_ ⊗ₜ _) * (_ ⊗ₜ _))

- = (_ ⊗ₜ _) * (_ ⊗ₜ _) * ((_ ⊗ₜ _) * (_ ⊗ₜ _))

+ erw [Algebra.TensorProduct.lift_tmul]

+ change (e ⊗ₜ[K] ((1 : A) ⊗ₜ[K] (1 : B)) * (1 : E) ⊗ₜ[K] (a ⊗ₜ[K] (1 : B))) *

+ (e' ⊗ₜ[K] ((1 : A) ⊗ₜ[K] (1 : B)) * (1 : E) ⊗ₜ[K] ((1 : A) ⊗ₜ[K] b)) =

+ (e' ⊗ₜ[K] ((1 : A) ⊗ₜ[K] (1 : B)) * (1 : E) ⊗ₜ[K] ((1 : A) ⊗ₜ[K] b)) *

+ (e ⊗ₜ[K] ((1 : A) ⊗ₜ[K] (1 : B)) * (1 : E) ⊗ₜ[K] (a ⊗ₜ[K] (1 : B)))

simp only [Algebra.TensorProduct.tmul_mul_tmul, _root_.mul_one, _root_.one_mul]

rw [mul_comm]

@@ -807,7 +806,8 @@ def e6 [Algebra.IsCentral K A] [csa_A : IsSimpleRing A]

refine ⟨(e ⊗ₜ a) ⊗ₜ[E] (1 ⊗ₜ b), ?_⟩

simp only [e6Aux0, Algebra.TensorProduct.lift_tmul, AlgHom.coe_mk, RingHom.coe_mk,

_root_.one_mul, map_one];

- change e ⊗ₜ[K] (1 ⊗ₜ[K] 1) * 1 ⊗ₜ[K] (a ⊗ₜ[K] 1) * 1 ⊗ₜ[K] (1 ⊗ₜ[K] b) = _

+ change (e ⊗ₜ[K] ((1 : A) ⊗ₜ[K] (1 : B)) * (1 : E) ⊗ₜ[K] (a ⊗ₜ[K] (1 : B))) *

+ ((1 : E) ⊗ₜ[K] ((1 : A) ⊗ₜ[K] (1 : B)) * (1 : E) ⊗ₜ[K] ((1 : A) ⊗ₜ[K] b)) = _

simp only [Algebra.TensorProduct.tmul_mul_tmul, _root_.mul_one, _root_.one_mul]

def e7 : E ≃ₐ[E] (E ⊗[K] K) := .symm <| Algebra.TensorProduct.rid _ _ _

diff --git a/BrauerGroup/BrauerOverR.lean b/BrauerGroup/BrauerOverR.lean

index 31ecd0a..b411cb1 100644

--- a/BrauerGroup/BrauerOverR.lean

+++ b/BrauerGroup/BrauerOverR.lean

@@ -233,12 +233,19 @@ abbrev C2toBrauerOverR : ZMod 2 →+ Additive (BrauerGroup ℝ) where

lemma toC2.left_inv : Function.LeftInverse C2toBrauerOverR toC2 := fun A ↦ by

induction A using Quotient.inductionOn' with | h A

+ classical

+ simp only [AddMonoidHom.coe_mk, dite_eq_ite, ZeroHom.coe_mk]

obtain h1 | h2 := BrauerOverR A

· change IsBrauerEquivalent A one_in' at h1

- simp only [AddMonoidHom.coe_mk, dite_eq_ite, ZeroHom.coe_mk, Quotient.lift_mk, h1, ↓reduceIte]

- rw [Quotient.sound']; exact h1.symm

+ refine (dif_pos ?_).trans ?_

+ · change (if IsBrauerEquivalent A one_in' then (0 : ZMod 2) else 1) = 0

+ simp [h1]

+ · exact Quotient.sound' h1.symm

· have : ¬ (IsBrauerEquivalent A one_in') := fun h ↦ QuaternionNotEquivR <| h2.symm.trans h

- simpa [this] using! Quotient.sound' h2.symm

+ refine (dif_neg ?_).trans ?_

+ · change ¬ ((if IsBrauerEquivalent A one_in' then (0 : ZMod 2) else 1) = 0)

+ simp [this]

+ · exact Quotient.sound' h2.symm

set_option backward.isDefEq.respectTransparency false in

lemma toC2.right_inv : Function.RightInverse C2toBrauerOverR toC2 := fun x ↦ by

diff --git a/BrauerGroup/CSA/ReducedCharPoly.lean b/BrauerGroup/CSA/ReducedCharPoly.lean

index 1a449bc..f16d52a 100644

--- a/BrauerGroup/CSA/ReducedCharPoly.lean

+++ b/BrauerGroup/CSA/ReducedCharPoly.lean

@@ -45,9 +45,9 @@ variable {K F E} in

def φ_m (φ : F →ₐ[K] E) : Matrix (Fin n) (Fin n) F →ₐ[K] Matrix (Fin n) (Fin n) E where

toFun M := fun i j ↦ φ (M i j)

map_one' := by ext i j; simp [Matrix.one_apply]

- map_mul' M1 M2 := by ext i j; simp [Matrix.mul_apply]

+ map_mul' M1 M2 := by ext i j; simp [Matrix.mul_apply]; try rfl

map_zero' := by ext; simp

- map_add' M1 M2 := by ext; simp

+ map_add' M1 M2 := by ext; simp; try rfl

commutes' k := by

ext i j

simp [Matrix.algebraMap_matrix_apply]

@@ -62,9 +62,9 @@ variable {K F E} in

abbrev e1Aux (φ : F →ₐ[K] E) : Matrix (Fin n) (Fin n) φ.range ≃ₐ[K] (φ_m n φ).range where

toFun M := ⟨(M · · |>.1), fun i j ↦ M i j |>.2.choose, by ext i j; exact M i j|>.2.choose_spec⟩

invFun := fun ⟨M, h⟩ i j ↦ ⟨M i j, h.choose i j, Matrix.ext_iff.2 h.choose_spec i j⟩

- left_inv _ := by simp

+ left_inv _ := by simp; try rfl

right_inv _ := by simp

- map_mul' _ _ := by ext; simp [Matrix.mul_apply]

+ map_mul' _ _ := by ext; simp [Matrix.mul_apply]; try rfl

map_add' _ _ := rfl

commutes' k := by

ext

@@ -122,6 +122,7 @@ lemma mat_over_extension (φ : F →ₐ[K] E) (a : A) :

AlgHom.mapMatrix_apply]

ext i j

simp [Matrix.map_apply]

+ try rfl

variable {K F n A} in

def ReducedCharPoly (a : A) : Polynomial F := Matrix.charpoly (e (1 ⊗ₜ a)) -- elements in F[X]

diff --git a/BrauerGroup/DoubleCentralizer.lean b/BrauerGroup/DoubleCentralizer.lean

index 602f8ff..451bf51 100644

--- a/BrauerGroup/DoubleCentralizer.lean

+++ b/BrauerGroup/DoubleCentralizer.lean

@@ -209,9 +209,9 @@ lemma centralizer_mulLeft_le_of_isCentralSimple :

ext x

simp only [LinearMap.mulLeft_apply]

simp only [tensor_self_op.equivEnd, tensor_self_op.toEnd, AlgEquiv.coe_ofBijective,

- Algebra.TensorProduct.lift_tmul, AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.coe_mk,

- OneHom.coe_mk, MulOpposite.unop_one, mul_one, Module.End.mul_apply, LinearMap.coe_mk,

- AddHom.coe_mk, eqv] ]

+ eqv]

+ erw [Algebra.TensorProduct.lift_tmul]

+ simp ]

ext b

simp only [Module.End.mul_apply, LinearMap.mulLeft_apply]

-- change y * (eqv (eqv.symm x)) b = (eqv (eqv.symm x)) (y * b)

@@ -258,9 +258,9 @@ lemma centralizer_mulLeft_le_of_isCentralSimple :

refine ⟨y.unop, ?_⟩

ext c

simp only [LinearMap.mulRight_apply, tensor_self_op.equivEnd, tensor_self_op.toEnd,

- AlgEquiv.coe_ofBijective, Algebra.TensorProduct.lift_tmul, AlgHom.coe_mk, RingHom.coe_mk,

- MonoidHom.coe_mk, OneHom.coe_mk, one_mul, Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk,

- eqv]

+ AlgEquiv.coe_ofBijective, eqv]

+ erw [Algebra.TensorProduct.lift_tmul]

+ simp

end central_simple_case

@@ -522,8 +522,11 @@ lemma Subalgebra.conj_simple_iff {B : Subalgebra F A} {x : Aˣ} :

rw [← mul_assoc x⁻¹.1, Units.inv_mul, one_mul])

(by

rintro ⟨_, ⟨a, ha, rfl⟩⟩ ⟨_, ⟨b, hb, rfl⟩⟩ ⟨c, hc1, hc2⟩

- simp only [toConj, AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,

- Subtype.mk.injEq, Units.mul_left_inj, Units.mul_right_inj] at hc2

+ have h1 : (x : A) * c.1 * ((x⁻¹ : Aˣ) : A) = x * a * ((x⁻¹ : Aˣ) : A) := congrArg Subtype.val hc2

+ have h2 : c.1 = a := by

+ have := congrArg (fun z => ((x⁻¹ : Aˣ) : A) * z * (x : A)) h1

+ simpa [mul_assoc] using this

+ replace hc2 : c = ⟨a, ha⟩ := Subtype.ext h2

refine ⟨⟨a, ha⟩ * ⟨b, hb⟩, J.mul_mem_right _ _ <| by

simp_rw [← hc2]; exact hc1, ?_⟩

ext

@@ -773,7 +776,7 @@ lemma finrank_mop (B : Type*) [Ring B] [Algebra F B] : Module.finrank F Bᵐᵒ

end centralizer_isSimple.aux

-set_option maxHeartbeats 400000 in

+set_option maxHeartbeats 1600000 in

-- Unclear

open centralizer_isSimple.aux in

lemma centralizer_isSimple {ι : Type*} (ℬ : Basis ι F <| Module.End F B) :

diff --git a/BrauerGroup/MatrixEquivTensor.lean b/BrauerGroup/MatrixEquivTensor.lean

index 60923a8..9309049 100644

--- a/BrauerGroup/MatrixEquivTensor.lean

+++ b/BrauerGroup/MatrixEquivTensor.lean

@@ -33,19 +33,16 @@ abbrev toTensorMatrix_toFun_Klinear : K ⊗[F] Matrix n n A →ₗ[K] Matrix n n

{__ := toTensorMatrix_toFun_Flinear K F A n,

map_smul' k tensor := by

induction tensor with

- | zero => simp

| tmul k0 M => simp [TensorProduct.smul_tmul', SemigroupAction.mul_smul]

| add _ _ h1 h2 => simp_all}

abbrev toTensorMatrix : K ⊗[F] Matrix n n A →ₐ[K] Matrix n n (K ⊗[F] A) := by

refine .ofLinearMap (toTensorMatrix_toFun_Klinear K F A n)

- (by simp [Algebra.TensorProduct.one_def]) fun t1 t2 ↦ ?_

Showing the first 260 of 593 lines. The full diff is the download below.

Re-run it

source bench/env.sh
python3 bench/lbbench.py setup brauergroup      # clone Whysoserioushah/BrauerGroup at v4.32.0, bump the Mathlib pin to v4.35.0
python3 bench/lbbench.py build brauergroup      # cache get + lake build; writes the raw errors to bench/runs/brauergroup/v4.35.0/errors.json

Files

Correct this page

Something wrong on this row, or you maintain this project and want it off the benchmark? Correct this row or remove my project.