[Merged by Bors] - feat(field_theory/cardinality): cardinality of fields & localizations

[ericrbg]

---

• depends on: [Merged by Bors] - chore(ring_theory/localization): localization_map_bijective rename & field instance version #12375
• depends on: [Merged by Bors] - feat(ring_theory/integral_domain): finite integral domain is a field #12376

[riccardobrasca]

Can you generalize localization_map_bijective_of_field to integral domains and then prove this lemma directly?

[ericrbg]

I don't think this is true, right? the Z -> Q algebra map is clearly not bijective

[riccardobrasca]

Sorry, I meant for finite integral domains. So the literal statement you proved, just with a different formulation.

[ericrbg]

Oh, I see! Yes, I'll do that. I think the real missing glue is a way to automagically turn a finite ID into a field, so I'll add that

[riccardobrasca]

Or something like is_field_of_is_domain_of_fintype.

[ericrbg]

hmm, do you think I should split some stuff now with all these changes?

[riccardobrasca]

Yes, it's probably a good idea to open a smaller PR that only talk about fields and integral domains, without cardinality involved.

About cardinality, essentially the same proof shows that this is also the list of a cardinalities of integral domains.

[ericrbg]

added a couple of these leafs. I'll extend the proof to integral domains too!

[ericrbg]

Actually, I realised that it's not so obvious to state this for integral domains, as integral domains are bundled. You'd have to have a spec lemma, and so on...

[riccardobrasca]

I see... don't bother too much about that

[alreadydone]

I think it's good to split the equality of cardinalities into two inequalities. And I have been able to show that #L ≤ #R holds universally. (edit: probably one inequality version and one equality version is enough, as in my branch.)

[leanprover-community-bot-assistant]

This PR/issue depends on:

• [Merged by Bors] - chore(ring_theory/localization): localization_map_bijective rename & field instance version #12375
• [Merged by Bors] - feat(ring_theory/integral_domain): finite integral domain is a field #12376
  By Dependent Issues (🤖). Happy coding!

[ericrbg]

thanks so much! I merged your changes, if that's ok :)

[alreadydone]

Sure, you're welcome!

[alreadydone]

The surjective result can be generalized to Artinian rings, see e.g. https://math.stackexchange.com/questions/1531139/localizations-of-an-artinian-ring-are-isomorphic-to-quotients
It seems mathlib doesn't know that all primes are maximal in Artinian rings, finiteness of the prime spectrum, and the product decompmosition, though it does know rings on fintypes are Artinian.

[ericrbg]

isn't this a tiny bit more specialized, though? because not all ideals are prime? This seems like a fun result to get in regardless, however :)

[alreadydone]

Oh yes it only deals with the at_prime case, not general localization. I think it's true in full generality nonetheless. I'll see if I can find or come up with a proof, but I think that would be deferred to another PR.

[riccardobrasca]

Yes, let's not transform this in a whole API for artinians rings :D

[jcommelin]

bors d+

[bors]

✌️ ericrbg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ericrbg]

bors r+ (below 100 chars)

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[alreadydone]

There is indeed a simple proof of the fact that localization of (commutative) artinian rings are surjections: it suffices to show that for all s in the submonoid, 1/s is in the image. The decreasing sequence of ideals (s^n) stabilizes, say (s^n) = (s^(n+1)), then s^n = s^(n+1) r for some r in the original ring, so 1/s is the image of r.

I have tried a bit to formalize it and this is as far as I get; I haven't had time to continue it so someone interested may finish and PR it. However I'm not sure if this result is worth being in mathlib; maybe we should construct the product decomposition for artinian rings and could probably show localizations are projections to certain factors.

section -- line 304
variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M] [is_artinian R M]

lemma is_artinian.range_smul_pow_stabilizes (r : R) : ∃ n : ℕ, ∀ m, n ≤ m →
  (r^n • linear_map.id : M →ₗ[R] M).range = (r^m • linear_map.id).range :=
is_artinian.monotone_stabilizes
  ⟨λ n, (r^n • linear_map.id : M →ₗ[R] M).range, λ n m h x ⟨y,hy⟩, ⟨r^(m-n) • y,
    by { dsimp at hy ⊢, rw ← smul_assoc, dsimp, rw ← pow_add, simp [h, hy] }⟩⟩

lemma is_artinian.exists_pow_succ_smul_dvd (r : R) (x : M) :
  ∃ (n : ℕ) (y : M), r ^ n • x = r ^ n.succ • y := sorry

end

[ericrbg]

Do we know that that really is 1/s? We can't cancel, right? [sorry to necro this, I decided to use this as an exercise - it's probably worth being in mathlib if it's true as it's a generalisation of something we already have]

[alreadydone]

Here's a full proof; s is a unit in the localization so cancelling is not problematic.

import ring_theory.artinian

variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M] [is_artinian R M]

namespace is_artinian

lemma range_smul_pow_stabilizes (r : R) : ∃ n : ℕ, ∀ m, n ≤ m →
  (r^n • linear_map.id : M →ₗ[R] M).range = (r^m • linear_map.id).range :=
is_artinian.monotone_stabilizes
  ⟨λ n, (r^n • linear_map.id : M →ₗ[R] M).range,
   λ n m h x ⟨y, hy⟩, ⟨r^(m-n) • y, by { convert hy using 1, simp [← smul_assoc, ← pow_add, h] }⟩⟩

lemma exists_pow_succ_smul_dvd (r : R) (x : M) :
  ∃ (n : ℕ) (y : M), r^n • x = r^n.succ • y :=
begin
  obtain ⟨n, hn⟩ := @range_smul_pow_stabilizes R M _ _ _ _ r,
  have : r^n • x ∈ (r^n • linear_map.id : M →ₗ[R] M).range := ⟨x, rfl⟩,
  obtain ⟨y, hy⟩ := (hn n.succ n.le_succ).subst this,
  exact ⟨n, y, hy.symm⟩,
end

variables {R' : Type*} [comm_ring R'] [algebra R R']

theorem localization_surjective [is_artinian_ring R] (S : submonoid R) [is_localization S R'] :
  function.surjective (algebra_map R R') :=
λ r', begin
  obtain ⟨r₁, s, rfl⟩ := is_localization.mk'_surjective S r',
  suffices : ∀ s : S, ∃ r : R, is_localization.mk' R' 1 s = algebra_map R R' r,
  { obtain ⟨r₂, h⟩ := this s, use r₁ * r₂, rw [is_localization.mk'_eq_mul_mk'_one, map_mul, h] },
  intro s,
  obtain ⟨n, r, hr⟩ := exists_pow_succ_smul_dvd (s : R) (1 : R),
  rw [smul_eq_mul, smul_eq_mul, pow_succ, mul_comm ↑s, mul_assoc] at hr,
  replace hr := congr_arg (algebra_map R R') hr,
  rw [map_mul, map_mul, mul_comm ↑s] at hr, simp only [← submonoid.coe_pow] at hr,
  use r, rw [← is_localization.mk'_one R', is_localization.mk'_eq_iff_eq],
  convert (is_localization.map_units R' _).mul_left_cancel hr, apply mul_one,
end

#check @localization_surjective
/- localization_surjective :
  ∀ {R : Type u_4} [_inst_1 : comm_ring R] {R' : Type u_5} [_inst_5 : comm_ring R']
  [_inst_6 : algebra R R'] [_inst_7 : is_artinian_ring R] (S : submonoid R)
  [_inst_8 : is_localization S R'], function.surjective ⇑(algebra_map R R') -/

end is_artinian

[ericrbg]

oh, of course, we only have to worry about the problem in the localisation itself. many thanks! I'll PR this under your authorship, if that's okay!