Cardinality of division ring generated by ...

Stream: Is there code for X?

[Junyan Xu]

I'd like to show the cardinality of the sub-division ring generated by an infinite set s is at most the cardinality of s. If the ambient division ring is a field then there is a surjection from MvPolynomial s ℤ to the subring generated by s, and every element in the subfield generated by s is a quotient of two elements in the subring, so we are good. In the noncommutative setting the subring admits a surjection from FreeRing, but nothing has been proven about its cardinality, and not every element in the sub-division ring can be written as a quotient of two elements in the subring.

The usual mathematical proof would be start with the set {0,1} ∪ s and enlarge it recursively with the four operations +, -, *, /. After countably many steps (read: take union over ℕ), the result is a sub-division ring, and is exactly the one generated by s. We prove by induction that the cardinality is #s at each step (clearly it's bounded by 4 times the square of the cardinality of the previous step), so the cardinality of the union is also #s.

The mathlib way of doing this argument seems to be using docs#WType which encapsulates tree structures like this; my current plan is to adapting a replaced old proof by @Chris Hughes for (Mv)Polynomials. I wonder whether the model theory framework to work with algebraic structures could be used to state and prove such cardinality results in full generality.

(Background: I'm trying to formalize this proof of Erdős-Kaplansky (a TODO item added by @Julian Külshammer) for division rings, and I'm about to open a PR to generalize the ambient Field in docs#Subfield.closure to DivisionRing.)

P.S. does mathlib really doesn't have Dual R (ι →₀ R) ≃ₗ[R] (ι → R) for commutative R? (Of course for noncommutative R this would be a R^mop-LinearEquiv.

[Eric Wieser]

Junyan Xu said:

does mathlib really doesn't have Dual R (ι →₀ R) ≃ₗ[R] (ι → R) for commutative R? (Of course for noncommutative R this would be a R^mop-LinearEquiv.

That would be a docs#Module.IsReflexive instance I think

[Junyan Xu]

I don't think so? It reads: the dual of Finsupp is Pi.

[Eric Wieser]

Oh sorry, I'm crippled by Android unicode (and the instance isn't there anyway)

[Riccardo Brasca]

I am on mobile, but this is the universal property of the direct sum, I would look there

[Eric Wieser]

Junyan Xu said:

The mathlib way of doing this argument seems to be using docs#WType which encapsulates tree structures like this;

Really? I though we just used inductive types, and WType is more of a "types without the inductive keyword" building block like Sum and Prod

[Junyan Xu]

Re: reflexive modules: It would be a fun (undergraduate level) project to prove that Dual ℤ (ℕ → ℤ) ≃ₗ[ℤ] (ℕ →₀ ℤ) though, which implies both Finsupp ℕ ℤ and ℕ → ℤ are reflexive.
https://en.wikipedia.org/wiki/Baer%E2%80%93Specker_group#Properties

[Junyan Xu]

Eric Wieser said:

Really? I though we just used inductive types, and WType is more of a "types without the inductive keyword" building block like Sum and Prod

Well the original proof for the cardinality of Polynomial uses WType (see the link in my original post). I think it's not used much because it's not necessary when you can explicitly construct the universal object.

[Junyan Xu]

We know the cardinality of WType, so we just need to construct a surjection from it.

[Eric Wieser]

I think at one point there was a plan to make an attribute that constructs the isomorphism between an inductive type and a suitable WType

[Junyan Xu]

The Subfield PR is #8941. The previous commit that only changes one file built without trouble, and I just pushed docstring fixes plus slight generalizations.

[Junyan Xu]

and the cardinality PR is #8942

[Junyan Xu]

To answer myself: Dual R (ι →₀ R) ≃ₗ[R] (ι → R) is a special case of docs#Basis.constr (applied to docs#Finsupp.basisSingleOne)

[Junyan Xu]

Erdős-Kaplansky theorem is PR'd as #9159; depends on two PRs.