Does every type permit a semiring?

Stream: maths

[Eric Wieser]

Here's my attempt:

import Mathlib

def cardinalLeSubsemiring {c : Cardinal.{u}} (hc : .aleph0 ≤ c) :
    Subsemiring Cardinal.{u} where
  carrier := Set.Ioc c
  zero_mem' := by simp
  one_mem' := Cardinal.one_le_aleph0.trans hc
  add_mem' := Cardinal.add_le_of_le hc
  mul_mem' := fun ha hb =>
    (Cardinal.mul_le_max _ _).trans <| max_le (max_le ha hb) hc

def cardinalLtSubsemiring {c : Cardinal.{u}} (hc : .aleph0 ≤ c) :
    Subsemiring Cardinal.{u} where
  carrier := Set.Iio c
  zero_mem' := Cardinal.aleph0_pos.trans_le hc
  one_mem' := Cardinal.one_lt_aleph0.trans_le hc
  add_mem' := Cardinal.add_lt_of_lt hc
  mul_mem' := Cardinal.mul_lt_of_lt hc

open scoped Cardinal in
theorem nonempty_semiring {R : Type u} [Nonempty R] : Nonempty (Semiring R) := by
  obtain hR | hR := finite_or_infinite R
  · obtain ⟨x⟩ := nonempty_fintype R
    classical
    obtain ⟨e⟩ := Fintype.truncEquivFin R
    have : NeZero (Fintype.card R) := by
      constructor; inhabit R; simp
    exact ⟨e.semiring⟩
  · have := Cardinal.infinite_iff.mp hR
    have e : R ≃ cardinalLtSubsemiring this := sorry -- is this true?
    exact ⟨e.semiring⟩

[Daniel Weber]

Is carrier in cardinalLeSubsemiring supposed to be carrier := {x | x ≤ c}?

[Daniel Weber]

Aren't there א0 cardinals less than א1?

[Eric Wieser]

Yes, ordinals seem plausible here

[Daniel Weber]

You need commutative addition. Nimbers might work, but it's probably easiest to use a free semiring

[Yaël Dillies]

I think you need something like ordinals with saturating natural addition and multiplication

[Daniel Weber]

import Mathlib

open scoped Cardinal

instance {R : Type*} [Infinite R] : Infinite (FreeMonoid R) := Infinite.of_injective FreeMonoid.of FreeMonoid.of_injective

@[simp]
theorem card_additive {R : Type*} : #(Additive R) = #R := rfl

theorem extracted_2.{u} {R : Type u} [Infinite R] :
    #(FreeMonoid R) = #R := by simp [FreeMonoid]

theorem theorem1.{u} {R : Type u} [Group R] :
    #(Abelianization R) ≤ #R := Cardinal.mk_le_of_injective Quotient.out_injective

theorem theorem2.{u} {R : Type u} [Infinite R] :
    #(FreeGroup R) = #R := by classical
  apply le_antisymm
  · apply (Cardinal.mk_le_of_injective (FreeGroup.toWord_injective (α := R))).trans
    simp
    rw [Cardinal.mul_eq_left (by simp) _ (by simp)]
    exact (Cardinal.nat_lt_aleph0 2).le.trans (by simp)
  · apply Cardinal.mk_le_of_injective FreeGroup.of_injective

theorem extracted_1.{u} {R : Type u} [Infinite R] :
    #(FreeAbelianGroup R) ≤ #R := by
  simp [FreeAbelianGroup]
  apply theorem1.trans
  simp [theorem2]

theorem nonempty_semiring {R : Type u} [Nonempty R] : Nonempty (Semiring R) := by
  obtain hR | hR := finite_or_infinite R
  · obtain ⟨x⟩ := nonempty_fintype R
    classical
    obtain ⟨e⟩ := Fintype.truncEquivFin R
    have : NeZero (Fintype.card R) := by
      constructor; inhabit R; simp
    exact ⟨e.semiring⟩
  · have ⟨e⟩ : Nonempty (R ≃ FreeRing R) := by
      rw [← Cardinal.eq]
      apply le_antisymm
      · apply Cardinal.mk_le_of_injective FreeRing.of_injective
      · unfold FreeRing
        exact extracted_2 (R := R) ▸ extracted_1
    exact ⟨e.semiring⟩

[Eric Wieser]

Very nice!

[Eric Wieser]

I guess that gets a Nonempty (Ring R) instance for free too

[Eric Wieser]

I set out to PR some of that, but got distracted by #18363 first

[Eric Wieser]

#18364 has all the lemmas in your above sample, thanks @Daniel Weber!

[Violeta Hernández]

Yaël Dillies said:

I think you need something like ordinals with saturating natural addition and multiplication

Ordinals with natural addition/multiplication up to w^w^a should do the trick

[Violeta Hernández]

Note that docs#Infinite.nonempty_field already exists by the way

[Antoine Chambert-Loir]

Yeah, it gives the example I was thinking of, field of rational functions in approriately many indeterminates over the rational. (One could take its algebraic closure, or work over a field of finite characteristic if one needed that.) Which brings to the natural question: shouldn't docs#Infinite.nonempty_field be rewritten so that its main result (cardinality of the field of rational functions) isn't hidden in it, and similarly for other algebraic structures, such as vector spaces?

[Eric Wieser]

Antoine Chambert-Loir said:

rewritten so that its main result (cardinality of the field of rational functions) isn't hidden in it

Folded into #18364

[Jz Pan]

Hi, I noticed that #18364 added Cardinal.mk_fractionRing which is the same as FractionRing.card in my PR #18004. Could you also review my PR?

Discussion is in #Is there code for X? > Localization.card_le

[Eric Wieser]

I think @Bhavik Mehta and I argued recently that we should not be using card in the names of such lemmas

[Eric Wieser]

(also apologies for the overlap, and thanks for spotting it!)