From c0c1e5f7b14eae3c20bdfdedbe6ddd82876d15ce Mon Sep 17 00:00:00 2001 From: Yunzhou Xie Date: Sat, 27 Jul 2024 15:17:57 +0100 Subject: [PATCH] check the statement? --- BrauerGroup/SplittingOfCSA.lean | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/BrauerGroup/SplittingOfCSA.lean b/BrauerGroup/SplittingOfCSA.lean index 71c1f15..97c72a1 100644 --- a/BrauerGroup/SplittingOfCSA.lean +++ b/BrauerGroup/SplittingOfCSA.lean @@ -242,11 +242,10 @@ def deg (A : CSA k): ℕ := dim_is_sq k A k_bar A.is_central_simple|>.choose lemma deg_sq_eq_dim (A : CSA k): (deg k k_bar A) ^ 2 = FiniteDimensional.finrank k A := by rw [pow_two]; exact dim_is_sq k A k_bar A.is_central_simple|>.choose_spec.symm -lemma deg_pos (A : CSA k): 0 < deg k k_bar A := by +lemma deg_pos (A : CSA k): deg k k_bar A ≠ 0 := by by_contra! h - have eq_zero : deg k k_bar A = 0 := by omega - apply_fun (λ x => x^2) at eq_zero - rw [deg_sq_eq_dim k k_bar A, pow_two, mul_zero] at eq_zero + apply_fun (λ x => x^2) at h + rw [deg_sq_eq_dim k k_bar A, pow_two, mul_zero] at h haveI := A.is_central_simple.is_simple.1 have Nontriv : Nontrivial A := inferInstance have := FiniteDimensional.finrank_pos_iff (R := k) (M := A)|>.2 Nontriv @@ -256,6 +255,10 @@ structure split (A : CSA k) (K : Type*) [Field K] [Algebra k K] := (n : ℕ) (hn : n ≠ 0) (iso : K ⊗[k] A ≃ₐ[K] Matrix (Fin n) (Fin n) K) +def isSplit : Prop := + ∃(n : ℕ)(L : Type u)(_ : n ≠ 0)(_ : Field L)(_ : Algebra k L), + Nonempty (L ⊗[k] A ≃ₐ[L] Matrix (Fin n) (Fin n) L) + def split_by_alg_closure (A : CSA k): split k A k_bar where n := deg k k_bar A hn := by haveI := deg_pos k k_bar A; omega @@ -323,7 +326,8 @@ def extension_over_split (A : CSA k) (L L': Type u) [Field L] [Field L'] [Algebr exact Nat.mul_self_inj.mp (id (this.trans e6).symm) exact (e3.trans e4).trans $ Matrix.reindexAlgEquiv L' (finCongr e5) -theorem exist_sep_over_CSA (A : CSA k): ∃(L : Type u)(_ : Field L)(_ : Algebra k L) - (split : split k A L), Algebra.IsSeparable k L := by - -- use +theorem exist_sep_over_CSA (A : CSA k): ∃(L : Type u)(_: Field L)(_ : Algebra k L), + isSplit k A ∧ Algebra.IsSeparable k L := by + refine ⟨k_s, _, _, + ⟨⟨deg k k_bar A, k_s, deg_pos k k_bar A, _, inferInstance, ⟨?_⟩⟩, inferInstance⟩⟩ sorry