a little bit

BrauerGroup/CentralSimple.lean

@@ -959,3 +959,89 @@ theorem CSA_implies_CSA (K : Type*) (B : Type*) [Field K] [Ring B] [Algebra K B]
 -- restrict to 4d case
 -- theorem exists_quaternionAlgebra_iso (hK : (2 : K) ≠ 0) :
 --     ∃ a b : K, Nonempty (D ≃ₐ[K] ℍ[K, a, b]) := sorry
+
+section
+
+lemma isSimpleOrder_iff (α : Type*) [LE α] [BoundedOrder α] :
+    IsSimpleOrder α ↔ Nontrivial α ∧ ∀ (a : α), a = ⊥ ∨ a = ⊤ := by
+  constructor
+  · intro h; refine ⟨inferInstance, fun a => h.2 a⟩
+  · rintro ⟨h, h'⟩; constructor; exact h'
+
+open TensorProduct in
+lemma IsSimpleRing.left_of_tensor (B C : Type*)
+    [Ring B] [Ring C] [Algebra K C] [Algebra K B]
+    [hbc : IsSimpleOrder (RingCon (B ⊗[K] C))] :
+    IsSimpleOrder (RingCon B) := by
+  have hB : Subsingleton B ∨ Nontrivial B := subsingleton_or_nontrivial B
+  have hC : Subsingleton C ∨ Nontrivial C := subsingleton_or_nontrivial B
+  rcases hB with hB|hB
+  · have : Subsingleton (B ⊗[K] C) := by
+      rw [← subsingleton_iff_zero_eq_one, show (0 : B ⊗[K] C) = 0 ⊗ₜ 0 by simp,
+        show (1 : B ⊗[K] C) = 1 ⊗ₜ 1 by rfl, show (1 : B) = 0 from Subsingleton.elim _ _]
+      simp only [tmul_zero, zero_tmul]
+    have : Subsingleton (RingCon (B ⊗[K] C)) := by
+      constructor
+      intro I J
+      refine SetLike.ext fun x => ?_
+      rw [show x = 0 from Subsingleton.elim _ _]
+      refine ⟨fun _ => RingCon.zero_mem _, fun _ => RingCon.zero_mem _⟩
+    have H := hbc.1
+    rw [← not_subsingleton_iff_nontrivial] at H
+    contradiction
+
+  rcases hC with hC|hC
+  · have : Subsingleton (B ⊗[K] C) := by
+      rw [← subsingleton_iff_zero_eq_one, show (0 : B ⊗[K] C) = 0 ⊗ₜ 0 by simp,
+        show (1 : B ⊗[K] C) = 1 ⊗ₜ 1 by rfl, show (1 : C) = 0 from Subsingleton.elim _ _]
+      simp only [tmul_zero, zero_tmul]
+    have : Subsingleton (RingCon (B ⊗[K] C)) := by
+      constructor
+      intro I J
+      refine SetLike.ext fun x => ?_
+      rw [show x = 0 from Subsingleton.elim _ _]
+      refine ⟨fun _ => RingCon.zero_mem _, fun _ => RingCon.zero_mem _⟩
+    have H := hbc.1
+    rw [← not_subsingleton_iff_nontrivial] at H
+    contradiction
+
+  by_contra h
+  rw [RingCon.IsSimpleOrder.iff_eq_zero_or_injective' (k := K) (A := B)] at h
+  push_neg at h
+  obtain ⟨B', _, _, f, h1, h2⟩ := h
+  have : Nontrivial B' := by
+    contrapose! h1
+    rw [← not_subsingleton_iff_nontrivial, not_not] at h1
+    refine SetLike.ext ?_
+    intro b
+    simp only [RingCon.mem_ker]
+    refine ⟨fun _ => trivial, fun _ => Subsingleton.elim _ _⟩
+  let F : B ⊗[K] C →ₐ[K] (B' ⊗[K] C) := Algebra.TensorProduct.map f (AlgHom.id _ _)
+  have hF := RingCon.IsSimpleOrder.iff_eq_zero_or_injective' (B ⊗[K] C) K |>.1 inferInstance F
+  -- have h : (RingCon.ker F) = ⊥ ∨ (RingCon.ker F) = ⊤ := hbc.2 (RingCon.ker F)
+  rcases hF with hF|hF
+  · have : Nontrivial (B' ⊗[K] C) := by
+      rw [← rank_pos_iff_nontrivial (R := K), rank_tensorProduct]
+      simp only [gt_iff_lt, CanonicallyOrderedCommSemiring.mul_pos, Cardinal.zero_lt_lift_iff]
+      rw [rank_pos_iff_nontrivial, rank_pos_iff_nontrivial]
+      aesop
+    have : 1 ∈ RingCon.ker F := by rw [hF]; trivial
+    simp only [RingCon.mem_ker, _root_.map_one, one_ne_zero] at this
+  · -- Since `F` is injective, `f` must be injective, this is because `C` is faithfully flat, but
+    -- we don't have this
+
+    sorry
+
+open TensorProduct in
+lemma IsSimpleRing.right_of_tensor (B C : Type*)
+    [Ring B] [Ring C] [Algebra K C] [Algebra K B]
+    [hbc : IsSimpleOrder (RingCon (B ⊗[K] C))] :
+    IsSimpleOrder (RingCon C) := by
+  haveI : IsSimpleOrder (RingCon (C ⊗[K] B)) := by
+    let e : C ⊗[K] B ≃ₐ[K] (B ⊗[K] C) := Algebra.TensorProduct.comm _ _ _
+    have := RingCon.orderIsoOfRingEquiv e.toRingEquiv
+    exact (OrderIso.isSimpleOrder_iff this).mpr hbc
+  apply IsSimpleRing.left_of_tensor (K := K) (B := C) (C := B)
+
+
+end

BrauerGroup/Con.lean

@@ -235,11 +235,20 @@ def comap {F : Type*} [FunLike F R R'] [RingHomClass F R R'] (J : RingCon R') (f
   __ := J.toCon.comap f (map_mul f)
   __ := J.toAddCon.comap f (map_add f)
 
-@[simp] lemma mem_comap {F : Type*} [FunLike F R R'] [RingHomClass F R R'] (J : RingCon R') (f : F) (x) :
+@[simp] lemma mem_comap {F : Type*} [FunLike F R R'] [RingHomClass F R R']
+    (J : RingCon R') (f : F) (x) :
     x ∈ J.comap f ↔ f x ∈ J := by
   change J (f x) (f 0) ↔ J (f x) 0
   simp
 
+lemma comap_injective {F : Type*} [FunLike F R R'] [RingHomClass F R R']
+    (f : F) (hf : Function.Surjective f) :
+    Function.Injective (fun J : RingCon _ ↦ J.comap f) := by
+  intro I J h
+  refine SetLike.ext fun x => ?_
+  simp only [mem_comap] at h
+  obtain ⟨x, rfl⟩ := hf x
+  rw [← mem_comap, ← mem_comap, h]
 
 instance : Module Rᵐᵒᵖ I where
   smul r x := ⟨x.1 * r.unop, I.mul_mem_right _ _ x.2⟩
@@ -449,6 +458,63 @@ lemma IsSimpleOrder.iff_eq_zero_or_injective [Nontrivial A] :
       rw [h] at mem
       exact mem
 
+lemma IsSimpleOrder.iff_eq_zero_or_injective'
+    (k : Type*) [CommRing k] [Algebra k A] [Nontrivial A] :
+    IsSimpleOrder (RingCon A) ↔
+    ∀ ⦃B : Type u⦄ [Ring B] [Algebra k B] (f : A →ₐ[k] B),
+      RingCon.ker f = ⊤ ∨ Function.Injective f := by
+  classical
+  constructor
+  · intro so B _ _ f
+    if hker : RingCon.ker f.toRingHom = ⊤
+    then exact Or.inl hker
+    else
+      replace hker := so.2 (RingCon.ker f) |>.resolve_right hker
+      rw [injective_iff_ker_eq_bot]
+      exact Or.inr hker
+  · intro h
+    refine ⟨fun I => ?_⟩
+    letI : Algebra k I.Quotient :=
+    { __ := I.mk'.comp (algebraMap k A)
+      smul := fun a => Quotient.map' (fun b => a • b) fun x y (h : I x y) => show I _ _ by
+        simp only
+        rw [Algebra.smul_def, Algebra.smul_def]
+        exact I.mul (I.refl (algebraMap k A a)) h
+      commutes' := by
+        simp only [RingHom.coe_comp, Function.comp_apply]
+        intro a b
+        induction b using Quotient.inductionOn' with
+        | h b =>
+          change _ * I.mk' b = I.mk' b * _
+          simp only [← map_mul, Algebra.commutes a b]
+
+      smul_def' := fun a b => by
+        simp only [RingHom.coe_comp, Function.comp_apply]
+        change Quotient.map' _ _ _ = _
+        induction b using Quotient.inductionOn' with
+        | h b =>
+          change _ = _ * I.mk' _
+          simp only [Quotient.map'_mk'', ← map_mul, Algebra.smul_def]
+          rfl }
+    rcases @h I.Quotient _ _ {I.mk' with commutes' := fun a => rfl } with h|h
+    · right
+      rw [eq_top_iff, le_iff]
+      rintro x -
+      simp only at h
+      have mem : x ∈ RingCon.ker I.mk' := by erw [h]; trivial
+      rw [mem_ker] at mem
+      change _ = I.mk' 0 at mem
+      exact I.eq.mp mem
+    · left
+      rw [injective_iff_ker_eq_bot] at h
+      rw [eq_bot_iff, le_iff]
+      intro x hx
+      have mem : x ∈ RingCon.ker I.mk' := by
+        rw [mem_ker]
+        exact I.eq.mpr hx
+      erw [h] at mem
+      exact mem
+
 end IsSimpleOrder
 
 end RingCon