From e8a2813739f789ba7ff6f30144887f45da73e7e5 Mon Sep 17 00:00:00 2001
From: Yunzhou Xie <yx3021@ic.ac.uk>
Date: Tue, 20 Aug 2024 17:00:36 +0100
Subject: [PATCH] fix

---
 BrauerGroup/GaloisSplit.lean | 18 ------------------
 BrauerGroup/Subfield.lean    |  0
 2 files changed, 18 deletions(-)
 create mode 100644 BrauerGroup/Subfield.lean

diff --git a/BrauerGroup/GaloisSplit.lean b/BrauerGroup/GaloisSplit.lean
index a025890..1edba4d 100644
--- a/BrauerGroup/GaloisSplit.lean
+++ b/BrauerGroup/GaloisSplit.lean
@@ -58,7 +58,6 @@ lemma coe_b_as_K' (e : split K A K_bar := split_by_alg_closure K K_bar A) (i j :
     (k : Fin (FiniteDimensional.finrank K A)) :
     (b_as_K' (e := e) i j k : K_bar) = b e i j k := rfl
 
-
 open IntermediateField in
 instance (e : split K A K_bar := split_by_alg_closure K K_bar A) :
     FiniteDimensional K (K' K K_bar A e) := by
@@ -69,14 +68,10 @@ instance (e : split K A K_bar := split_by_alg_closure K K_bar A) :
     exact Algebra.IsIntegral.isIntegral i
   apply finiteDimensional_iSup_of_finset
 
-
--- local notation "K'" => K' K K_bar A
-
 set_option synthInstance.maxHeartbeats 60000 in
 instance (e : split K A K_bar) :
   Algebra ((K' K K_bar A e)) ((K' K K_bar A e) ⊗[K] A.carrier) := inferInstance
 
-
 set_option synthInstance.maxHeartbeats 60000 in
 instance (e : split K A K_bar) :
   Module ((K' K K_bar A e)) ((K' K K_bar A e) ⊗[K] A.carrier) := inferInstance
@@ -85,7 +80,6 @@ set_option synthInstance.maxHeartbeats 60000 in
 instance (e : split K A K_bar) :
   DistribSMul ((K' K K_bar A e)) ((K' K K_bar A e) ⊗[K] A.carrier) := inferInstance
 
-
 private def emb (e : split K A K_bar := split_by_alg_closure K K_bar A) :
     K' K K_bar A e ⊗[K] A →ₐ[K' K K_bar A e] K_bar ⊗[K] A :=
   Algebra.TensorProduct.map (Algebra.ofId (K' (e := e)) _) (AlgHom.id _ _)
@@ -97,8 +91,6 @@ private lemma emb_tmul (e : split K A K_bar := split_by_alg_closure K K_bar A) :
   simp only [emb, Algebra.TensorProduct.map_tmul, AlgHom.coe_id, id_eq]
   rfl
 
--- set_option synthInstance.maxHeartbeats 60000 in
-
 lemma basis'_li (e) : LinearIndependent ↥(K' K K_bar A e) fun i : Fin e.n × Fin e.n ↦
   ∑ j : Fin (FiniteDimensional.finrank K A.carrier),
     b_as_K' K K_bar A e i.1 i.2 j ⊗ₜ[K] (FiniteDimensional.finBasis K A.carrier) j := by
@@ -151,7 +143,6 @@ def e'Aux (e : split K A K_bar := split_by_alg_closure K K_bar A) :
     Matrix (Fin e.n) (Fin e.n) (K' K K_bar A e) :=
   Basis.equiv (b := basis' (e := e)) (b' := Matrix.stdBasis (K' K K_bar A e) (Fin e.n) (Fin e.n)) $
     Equiv.refl _
-  -- Algebra.TensorProduct.equiv K (K' K K_bar A e) A
 
 lemma e'Aux_apply_basis (e : split K A K_bar := split_by_alg_closure K K_bar A)
     (i j : Fin e.n) :
@@ -165,7 +156,6 @@ lemma e'Aux_apply_basis (e : split K A K_bar := split_by_alg_closure K K_bar A)
   ext
   simp only [Equiv.refl_apply, Matrix.stdBasis_eq_stdBasisMatrix, Matrix.stdBasisMatrix]
 
-
 def emb' (e : split K A K_bar := split_by_alg_closure K K_bar A):
     Matrix (Fin e.n) (Fin e.n) (K' K K_bar A e) →ₐ[K' K K_bar A e]
     Matrix (Fin e.n) (Fin e.n) K_bar :=
@@ -181,10 +171,6 @@ lemma emb'_inj (e : split K A K_bar := split_by_alg_closure K K_bar A):
     IntermediateField.algebraMap_apply, SetLike.coe_eq_coe] at h ⊢
   exact h
 
--- def embemb (e : split K A K_bar := split_by_alg_closure K K_bar A) :
---     (K' K K_bar A e) ⊗[K] A →ₐ[K' K K_bar A e] K_bar ⊗[K] A :=
---   Algebra.TensorProduct.map (Algebra.ofId (K' (e := e)) _) (AlgHom.id _ _)
-
 set_option synthInstance.maxHeartbeats 60000 in
 instance (e) : NonUnitalNonAssocSemiring (↥(K' K K_bar A e) ⊗[K] A.carrier) := inferInstance
 
@@ -224,7 +210,6 @@ lemma e'_map_mul (e : split K A K_bar := split_by_alg_closure K K_bar A)
   rw [← eq, (emb (e := e)).map_mul, _root_.map_mul (f := e.iso), (emb' (e := e)).map_mul,
     ← eqx, ← eqy]
 
-
 lemma e'_map_one (e : split K A K_bar := split_by_alg_closure K K_bar A) :
     (e'Aux K K_bar A e) 1 = 1 := by
   have eq := congr($(emb_comm_square (e := e)) 1)
@@ -233,12 +218,9 @@ lemma e'_map_one (e : split K A K_bar := split_by_alg_closure K K_bar A) :
     AlgHom.toLinearMap_apply, AlgEquiv.toLinearMap_apply, LinearEquiv.coe_coe] at eq
   rw [← eq, (emb (e := e)).map_one, _root_.map_one (f := e.iso), (emb' (e := e)).map_one]
 
-
-
 def e' (e : split K A K_bar := split_by_alg_closure K K_bar A) :
     (K' K K_bar A e) ⊗[K] A ≃ₐ[K' K K_bar A e]
     Matrix (Fin e.n) (Fin e.n) (K' K K_bar A e) :=
   AlgEquiv.ofLinearEquiv (e'Aux (e := e)) (e'_map_one (e := e)) (e'_map_mul (e := e))
 
-
 end one
diff --git a/BrauerGroup/Subfield.lean b/BrauerGroup/Subfield.lean
new file mode 100644
index 0000000..e69de29