Localization.card_le

Stream: Is there code for X?

[Jz Pan]

import Mathlib.GroupTheory.MonoidLocalization.Basic
import Mathlib.SetTheory.Cardinal.Basic

namespace Localization

variable {M : Type*} [CommMonoid M] (S : Submonoid M)

/-- The cardinality of the `Localization` of `M` at `S` is at most `#M * #S`. -/
@[to_additive "The cardinality of the `AddLocalization` of `M` at `S` is at most `#M * #S`."]
theorem card_le' : Cardinal.mk (Localization S) ≤ Cardinal.mk M * Cardinal.mk S := by
  let i : M × S → Localization S := fun x ↦ Localization.mk x.1 x.2
  have h : Function.Surjective i := Quotient.surjective_Quotient_mk''
  simpa using Cardinal.mk_le_of_surjective h

/-- The cardinality of the `Localization` of `M` at `S` is at most `#M * #M`. -/
@[to_additive "The cardinality of the `AddLocalization` of `M` at `S` is at most `#M * #M`."]
theorem card_le : Cardinal.mk (Localization S) ≤ Cardinal.mk M * Cardinal.mk M :=
  (Localization.card_le' S).trans (by gcongr; exact Cardinal.mk_subtype_le _)

end Localization

Do we have these in mathlib?

In fact, what result I need to use is the cardinality of total fraction ring. But it turns out that mathlib has stronger result for this: docs#IsLocalization.card. Do we want FractionRing.card or IsFractionRing.card which is a direct application of this?

[Johan Commelin]

If it's a direct application, I don't think it needs to be separately stated

[Jz Pan]

Basically it is

-- TODO: move to suitable place
theorem _root_.FractionRing.card (R : Type u) [CommRing R] :
    Cardinal.mk (FractionRing R) = Cardinal.mk R :=
  (IsLocalization.card (FractionRing R) (nonZeroDivisors R) (le_refl _)).symm

and it's convenient to write rw [FractionRing.card]. Otherwise it can be rw [← IsLocalization.card (FractionRing _) (nonZeroDivisors _) (le_refl _)] which is a little bit longer I think.

[Johan Commelin]

Yeah, that's complicated enough to make it a separate lemma.
Additional benefit: you can tag it with @[simp]

[Yaël Dillies]

(le_refl _) can simply be le_rfl

[Jz Pan]

Do you think there should be a stronger version of Cardinal.mk (Localization S) ≤ Cardinal.mk M * Cardinal.mk S? My current version is only a very rough estimation.

[Violeta Hernández]

Note that for infinite M, #M * #M = #M

[Jz Pan]

Johan Commelin said:

Yeah, that's complicated enough to make it a separate lemma.
Additional benefit: you can tag it with @[simp]

Next question is: What file should it stay? I believe that Mathlib.RingTheory.Localization.Cardinality does not import FractionRing, vice versa.

[Jz Pan]

Violeta Hernández said:

Note that for infinite M, #M * #M = #M

I know this. The docs#IsLocalization.card_le actually suggests that Cardinal.mk (Localization S) ≤ Cardinal.mk M, at least for rings. But what about the original setup of Localization?

[Johan Commelin]

I think it should go in a new file.

[Junyan Xu]

For a finite commutative monoid, it is also true that the canonical map to any localization is surjective. The reason is that for any element m in the submonoid, there exists natural numbers i > j such that m ^ i = m ^ j, by finiteness. Since m becomes invertible in the localization, we can check that m ^ (i - j - 1) maps to the inverse of m in the localization, so the localization is not adjoining any new element.

My proof of the same fact for finite comm. rings in mathlib3 follows roughly the same idea, but it uses finiteness of the localization instead. The proof was later replaced by the more general fact for Artinian comm. rings, so it's no longer in mathlib4.

[Jz Pan]

What about non-commutative monoid? In this case the multiplicative subset should satisfy certain condition (Ore condition) and we should use docs#OreLocalization instead. Is it still true in this case?

[Junyan Xu]

Yeah I think the argument still works. The inverses of elements in the submonoid still generate the localized monoid over the original monoid.

[Jz Pan]

Here it goes:

import Mathlib.GroupTheory.OreLocalization.Basic
import Mathlib.Data.Fintype.Card

namespace OreLocalization

@[to_additive]
theorem numeratorHom_surj_of_finite
    {R : Type*} [Monoid R] (S : Submonoid R) [OreSet S]
    [Finite S] : Function.Surjective (numeratorHom (S := S)) := by
  refine OreLocalization.ind fun r s ↦ ?_
  obtain ⟨i, j, hne, heq⟩ := Finite.exists_ne_map_eq_of_infinite (α := ℕ) (s ^ ·)
  wlog hlt : j < i generalizing i j
  · exact this j i hne.symm heq.symm (hne.lt_of_le (not_lt.1 hlt))
  use (s ^ (i - j - 1)).1 * r
  rw [numeratorHom_apply, oreDiv_eq_iff]
  refine ⟨s ^ j, (s ^ (j + 1)).1, ?_, ?_⟩
  · change (s ^ j).1 * r = (s ^ (j + 1)).1 * ((s ^ (i - j - 1)).1 * r)
    simp_rw [← heq, SubmonoidClass.coe_pow, ← mul_assoc, ← pow_add, Nat.sub_sub,
      Nat.add_sub_cancel' hlt]
  · simp_rw [SubmonoidClass.coe_pow, OneMemClass.coe_one, mul_one, pow_succ]

end OreLocalization

But I need to use Finite.exists_ne_map_eq_of_infinite from Mathlib.Data.Fintype.Card. Should this be added to Mathlib.GroupTheory.OreLocalization.Basic or a new file?

[Jz Pan]

Another problem: docs#OreLocalization can also define localization of modules; is #X[S⁻¹] ≤ #X still true? The above proof also works in this case if #S or #X is finite. But I have no idea when both of them are infinite, since there are no assumptions on the comparison of #S and #X.

[Antoine Chambert-Loir]

one has Card (localization) at most Card(X)xCard(S) hence at most Card(X) when X is infinite (Hessenberg).

[Antoine Chambert-Loir]

a more general result holds even without the Ore condition: if X to Y is a morphism of monoids and Y is generated by its image and a subset of cardinality at most Card(X), then Card(Y) is at most Card(X).
This bound can be used to prove that a localization exists even when the Ore condition doesn't hold— the natural direct limit can be bounded over a set.

[Jz Pan]

Antoine Chambert-Loir said:

Card(X)xCard(S) hence at most Card(X)

Note that X is only an R-module, but not the ring R itself. So a priori it's possible that R and its multiplicative subset S are uncountable, but X is countable, and this argument breaks.

[Jz Pan]

I think it's still true but I need a different arguments.

[Antoine Chambert-Loir]

i was thinking about the case of monoids. if you have a module, you first need to consider the quotient ring that acts faithfully (and won't be larger than X)

[Jz Pan]

Antoine Chambert-Loir said:

ring that acts faithfully (and won't be larger than X)

I can't prove the last step; if R acts faithfully on X I can only conclude that R injects into End(X) which is of cardinality 2 ^ #X I think.

[Jz Pan]

My plan is to prove #{x/s | s \in S} ≤ #X for each x \in X. Suppose s x = s' x then I want to prove x/s = x/s'. I can only prove this if s and s' commutes. Otherwise I have no idea on it; I try to back and forth using Ore's condition, but till now there is no progress.

[Jz Pan]

FYI This is the formalized code:

import Mathlib.GroupTheory.OreLocalization.Basic
import Mathlib.SetTheory.Cardinal.Arithmetic

universe u v

open Cardinal

namespace OreLocalization

variable {R : Type u} [Monoid R] (S : Submonoid R) [OreLocalization.OreSet S]
  (X : Type v) [MulAction R X]

@[to_additive]
theorem oreDiv_one_surj_of_finite_right [Finite X] :
    Function.Surjective (fun x ↦ x /ₒ (1 : ↥S) : X → OreLocalization S X) := by
  refine OreLocalization.ind fun x s ↦ ?_
  obtain ⟨i, j, hne, heq⟩ := Finite.exists_ne_map_eq_of_infinite (α := ℕ) (s ^ · • x)
  wlog hlt : j < i generalizing i j
  · exact this j i hne.symm heq.symm (hne.lt_of_le (not_lt.1 hlt))
  use s ^ (i - (j + 1)) • x
  rw [oreDiv_eq_iff]
  refine ⟨s ^ j, (s ^ (j + 1)).1, ?_, ?_⟩
  · change s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
    rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]
  · simp_rw [SubmonoidClass.coe_pow, OneMemClass.coe_one, mul_one, pow_succ]

-- TODO How to remove the Commute condition
@[to_additive]
theorem card_le_lift_card_of_commute (hc : ∀ s s' : S, Commute s s') :
    #(OreLocalization S X) ≤ lift.{u} #X := by
  rcases finite_or_infinite X with _ | _
  · have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surj_of_finite_right S X)
    rwa [lift_umax.{v, u}, lift_id'] at this
  have key (x : X) (s s' : S) (h : s • x = s' • x) (hc : Commute s s') : x /ₒ s = x /ₒ s' := by
    rw [oreDiv_eq_iff]
    refine ⟨s, s'.1, h, ?_⟩
    · exact_mod_cast hc
  let i (x : X × S) := x.1 /ₒ x.2
  have hsurj : Function.Surjective i := Quotient.surjective_Quotient_mk''
  have hi := Function.rightInverse_surjInv hsurj
  let j := (fun x : X × S ↦ (x.1, x.2 • x.1)) ∘ Function.surjInv hsurj
  suffices Function.Injective j by
    have := lift_mk_le_lift_mk_of_injective this
    rwa [lift_umax.{v, u}, lift_id', mk_prod, lift_id, lift_mul, mul_eq_self (by simp)] at this
  intro y y' heq
  rw [← hi y, ← hi y']
  simp_rw [j, Function.comp_apply, Prod.ext_iff] at heq
  simp_rw [i]
  set x := Function.surjInv hsurj y
  set x' := Function.surjInv hsurj y'
  obtain ⟨h1, h2⟩ := heq
  rw [← h1] at h2 ⊢
  exact key x.1 x.2 x'.2 h2 (hc _ _)

end OreLocalization

[Jz Pan]

PR created as #18004.

[Junyan Xu]

For the noncommutative case, there's still a description of localized module as a filtered colimit of copies of X (DirectLimit in mathlib): see https://ocw.mit.edu/courses/18-706-noncommutative-algebra-spring-2023/mit18_706_s23_lec20.pdf However, I don't know how one could bound this particular colimit.

[Jz Pan]

Junyan Xu said:

there's still a description of localized module as a filtered colimit of copies of X

It's the #S copies of X. So it seems to be a restatement of S × X / ~... but I don't know if there are new insights.

[Jz Pan]

Unfortunately, using mathlib's definition of OreLocalization.OreSet I can't prove that it forms a filtered system. More precisely, for s, t \in S I can't find u, v \in S such that u s = v t; mathlib's definition only gives v \in R. Did I miss something?

[Antoine Chambert-Loir]

in the mathlib definition of an Ore set, i can't recognize that the docstring says the same as the definition.

[Jz Pan]

Mathlib's definition coincides with Wikipedia's (modulo left Ore vs right Ore). I think it's the lecture note which is too sloppy on this.

Anyways, I think the filtered or not does not significantly change the nature of the question.

[Jz Pan]

OK I think I'll give up on this and keep PR #18004 as its current form. Any comments on it?

[Junyan Xu]

Jz Pan said:

Unfortunately, using mathlib's definition of OreLocalization.OreSet I can't prove that it forms a filtered system. More precisely, for s, t \in S I can't find u, v \in S such that u s = v t; mathlib's definition only gives v \in R. Did I miss something?

I think we may need to take the saturation of the Ore set, as explained in this thesis.
image.png

[Junyan Xu]

Jz Pan said:

Another problem: docs#OreLocalization can also define localization of modules; is #X[S⁻¹] ≤ #X still true? The above proof also works in this case if #S or #X is finite. But I have no idea when both of them are infinite, since there are no assumptions on the comparison of #S and #X.

Two observations: 1) if you get a counterexample for a monoid M acting on a set X, you can probably linearize it to get a counterexample for the ring R[M] acting on R[X], for a commutative ring R. 2) we may assume X is "cyclic" (generated by one element over M), so it's a "quotient" of M (we have been implicitly restricting to the "orbit" of x, but this change of viewpoint might still help).

[Antoine Chambert-Loir]

Mathlib should really refrain using Wikipedia as a reference for mathematical definitions. One difficult aspect of a unified library of mathematics such as mathlib lies in providing a long-range consistency of definitions/notation, while Wikipedia (despite its tremendous usefulness) has no such constraint.

[Ruben Van de Velde]

I'm not sure I'd go that far - we should use the definitions that work best and agree as much as is reasonable with the literature - including tertiary sources like wikipedia (which will probably be the first definition many people see)

[Antoine Chambert-Loir]

My claim is that Wikipedia has no relevance as for definitions that work best on the long term. (They could even be incompatible from one page to another.)

[Yaël Dillies]

I don't really see how the purported poor consistency of Wikipedia definitions undermines it as a reference. References don't have to be followed closely

[Jz Pan]

Junyan Xu said:

I think we may need to take the saturation of the Ore set, as explained in this thesis.

Great! Maybe I'll come back to this later.

[Jz Pan]

Interesting. We only have docs#Subgroup.Saturated and it is not used in other parts of mathlib. Now we need Submonoid.Saturated(or even Subsemigroup.Saturated), and the saturation (of a multiplicative subset, which I think is used frequently in commutative algebra --- don't we have this in mathlib ??).

[Junyan Xu]

Note that Subgroup.Saturated is a distinct notion, see previous discussion. In noncommutative setting there's notions of left/right-saturated.

[Jz Pan]

ping any new comments on PR #18004? Besides cardinal_mk vs cardinalMk debate...

[Johan Commelin]

borsified