A commutative simple ring is a field

Stream: Is there code for X?

[Snir Broshi]

import Mathlib

noncomputable instance {R : Type*} [CommRing R] [IsSimpleRing R] : Field R :=
  Field.ofIsUnitOrEqZero fun a ↦ isSimpleRing_iff_isTwoSided_imp.mp ‹_› |>.right (Ideal.span {a})
    (Ideal.instIsTwoSided _) |>.elim (fun h ↦ Or.inr <| Ideal.span_singleton_eq_bot.mp h)
    (fun h ↦ Or.inl <| Ideal.span_singleton_eq_top.mp h)

I tried Loogle with IsSimpleRing, Field but didn't find such a theorem, but maybe this exists with weaker assumptions than IsSimpleRing

[Aaron Liu]

docs#isSimpleRing_iff_isField

[Aaron Liu]

not an instance or anything since we don't want to make data

[Aaron Liu]

docs#IsField.toField

[Snir Broshi]

Thanks, I didn't know IsField existed
I have a theorem that requires CommRing and IsSimpleRing, and I'm considering replacing both with Field, but this not being an instance means the Field version would be harder to use, right?

[Aaron Liu]

I guess yeah

[Aaron Liu]

what's the theorem

[Snir Broshi]

theorem aroots_card_eq_natDegree_from_field {A B : Type*}
    [CommRing A] [IsSimpleRing A]
    [Field B] [IsAlgClosed B]
    [Algebra A B] {p : A[X]} : (p.aroots B).card = p.natDegree :=
  ...

[Kenny Lau]

you probably want FaithfulSMul A B and no IsSimpleRing A

[Kenny Lau]

i apologise if i said something else on one of your PR's

[Snir Broshi]

The PR in question is #29956 (I resolved everything btw).
I'm not sure how FaithfulSMul helps here, can you elaborate?
The current proof relies on a theorem that requires IsSimpleRing

[Aaron Liu]

all you want is that the algebra map is injective right

[Aaron Liu]

I don't think you actually need a field

[Aaron Liu]

like if A := ℤ and B is char-zero then the theorem still holds

[Snir Broshi]

Yes I can require Function.Injective (algebraMap A B)

[Kenny Lau]

FaithfulSMul is exactly equivalent to algebraMap injective

[Snir Broshi]

Opinions on adding this instance?

import Mathlib
variable {A B : Type*} [CommRing A] [IsSimpleRing A] [Semiring B] [Nontrivial B] [Algebra A B]

instance : FaithfulSMul A B :=
  faithfulSMul_iff_algebraMap_injective A B |>.mpr (algebraMap A B).injective

[Riccardo Brasca]

LGTM

[Snir Broshi]

Added to #29956, which allowed me to remove a theorem about simple rings

[Edison Xie]

(deleted)

[Kenny Lau]

I just don't see how [CommRing A] [IsSimpleRing A] is a good idea in general.

[Kevin Buzzard]

This is just a complicated way of saying Field A right?

[Aaron Liu]

Field A comes with more data (how to do division and multiplicative inverses, as well as raising to an integer power)

[Kenny Lau]

well it is at least equivalent to [CommRing A] [IsField A] already, without using classical

[Junyan Xu]

docs#IsField isn't a class ... (and it also includes commutativity)

[Riccardo Brasca]

Yeah that was my idea: the point is that we don't want a Field instance on [CommRIng A] [IsSimpleRing A], so it still makes sense to have other instances that can be found automatically

[Riccardo Brasca]

But I don't know how much this would be used in practice

[Edison Xie]

Riccardo Brasca said:

But I don't know how much this would be used in practice

Sometimes I use them but I only have IsField A as a lemma

[Edison Xie]

Junyan Xu said:

docs#IsField isn't a class ... (and it also includes commutativity)

I’m thinking maybe we should get rid of IsField and just have IsDivisionRing

[Snir Broshi]

Snir Broshi said:

Opinions on adding this instance?

import Mathlib
variable {A B : Type*} [CommRing A] [IsSimpleRing A] [Semiring B] [Nontrivial B] [Algebra A B]

instance : FaithfulSMul A B :=
  faithfulSMul_iff_algebraMap_injective A B |>.mpr (algebraMap A B).injective

Update: this instance was added in #29356 (even before I opened this thread) and is now docs#instFaithfulSMul_1