Localization of ℤ at p as a subring of ℚ with hom. to ℤ/pℤ?

Stream: Is there code for X?

[Michael Stoll]

Does mathlib know that {x : ℚ // padic_val_rat p x ≥ 0} is a subring of ℚ and has a canonical homomorphism onto zmod p?

[Johan Commelin]

I'm afraid it (mathlib) does not.

[Johan Commelin]

But I think you can rather easily construct the map to ℤ_[p].

[Michael Stoll]

And then compose with to_zmod? But that would defeat the purpose, since the goal would be to produce a computable definition of to_zmod.

[Michael Stoll]

I see that there is ring_theory.localization, but a cursory look gives me the impression that this is much too abstract for my purpose.

[Johan Commelin]

Aah, if you want it to be computable, then I guess you'll have to handroll it

[Junyan Xu]

This ongoing PR realizes localization as a subring of the field of fractions.

[Adam Topaz]

More precisely #13425

[Junyan Xu]

It seems easiest to define localization.subring as ring_hom.range of the natural ring_hom from the localization to the fraction ring. Then docs#is_localization.surj will supply us with the desired representation of elements as quotients.

[Junyan Xu]

@Adam Topaz Have you reviewed my change of defintion of prime_of_le? I think it's most convenient to just use this new definition. If you want the valuation characterization we should just add a lemma mem_prime_of_le_iff.

[Adam Topaz]

@Junyan Xu , yeah that looks like a good approach.

[Adam Topaz]

Junyan Xu said:

It seems easiest to define localization.subring as ring_hom.range of the natural ring_hom from the localization to the fraction ring. Then docs#is_localization.surj will supply us with the desired representation of elements as quotients.

Yeah, this will probably make the initial definitions a little shorter. But it's really nice when you can write rintro \<_,a,b,hb,rfl\> to automatically get the presentation of the element of your localization as a fraction

[Junyan Xu]

It seems easiest to define localization.subring as ring_hom.range of the natural ring_hom from the localization to the fraction ring.

@Adam Topaz Here's that definition worked out! Not just a bit shorter :) https://github.com/leanprover-community/mathlib/compare/localization_subring...loc_subring_range?expand=1

This would break defeq so valuation_subring_order needs to be fixed, but that shouldn't be hard.

[Junyan Xu]

I proceeded with the ring_hom.range definition and generalized as_subring.lean a bit to allow A not a domain / K not a field. However, the inverse is only available in a field, so I can only recover the original definition as lemma mem_iff_of_field in the field case.

Here is what it takes to adapt valuation_subring to use the new definition of localization.subring: it just involves a couple of of erw mem_iff_of_field. If you don't like it we can make a subring.copy in the field case. Everything is in the branch val_subring_order_golf and ready to be merged into #13429.

[Adam Topaz]

@Junyan Xu Nice! What do you think about the following:

1. Make (is_localization.lift (λ s, by apply is_localization.map_units K ⟨s.1, hS s.2⟩) : localization S →+* K) into a def, say map_to_fraction_ring or something.
2. Make your mem_iff lemma into a lemma about the range of the map from 1.
3. Define subring K S hS using subring.copy, using mem_iff to make the carrier defeq to the condition given by mem_iff.
   The nice definitional properties of the carrier would be essentially all the same, and I think most (if not all) of the shortened proofs would still remain.

[Adam Topaz]

In any case, I won't be able to do anything involving lean until at least Tuesday, so I changed to a WIP tag on #13425

[Adam Topaz]

If you want to merge what you wrote to my branch, please do go ahead.

[Junyan Xu]

Thanks for taking a look! What you suggest looks like a good plan, but if we do subring.copy in the general (comm_ring) case, do we want another subring.copy to get nicer defeq in the field case?

[Junyan Xu]

We won't be able to use rfl in the general case, so it's not as nice as the field case where we can use rintro \<_,a,b,hb,rfl\> .

[Adam Topaz]

Naw, I think the carrier in the more general case would be essentially just as good as the condition in the field case.

[Adam Topaz]

So I suggest keeping the statement of mem_iff_of_field the same, while making mem_iff true by refl.

[Adam Topaz]

Hmm... Maybe we should only define subring in the case of fields? If we name the map as I suggested above, using range in the general case along with your mem_iff is probably as good as it gets. In the field case, we could use subring which is useful for definitional tricks like using rcases/rintro with rfl.

[Junyan Xu]

I've made the subring -> subalgebra change, which gets rid of a bunch of instance declarations.

I changed mem_iff to a version using docs#is_localization.mk', which enables rintro rfl and can be converted to the original version using docs#is_localization.mk'_eq_iff_eq_mul, and the proof of mem_iff_of_field simplifies slightly.

https://github.com/leanprover-community/mathlib/compare/valuation_subring_order...val_subring_order_golf?expand=1

I have not done the copy stuff. If you think it needs to be done for future convenience, I suggest we rename the current subalgebra to something like subalgebra_aux, and define subalgebra using copy in the field case.

[Adam Topaz]

I'm a bit surprised we don't have a version of is_localization.lift that gives an alg_hom. Maybe I missed it?

[Adam Topaz]

@Junyan Xu I merged your branch into branch#valuation_subring_order ... No need to have divergent branches for this! Please feel free to push directly to valuation_subring_order (this is becoming a collaborative PR anyway ;))

[Junyan Xu]

@Adam Topaz Yeah that's a bit surprising, I guess maybe the alg_hom API wasn't well developed when most of ring_theory.localization was written? Searching for ₐ in ring_theory.localization.basic shows it appears in only 4 declarations.

Thanks! I was working in that branch so it was most convenient to push to it, but now that you merged it I'll work in branch#valuation_subring_order henceforth.

[Adam Topaz]

I just pushed a start to the approach using copy.

[Adam Topaz]

As you can see, I defined this map_to_fraction_ring algebra hom, and defined subalgebra by copying using the range of that.
There is still one sorry (about bijectivity) and some similar isntances to add for subalgebra_of_field.

I wonder whether it's worthwhile to add some of these localization instances for (map_to_fraction_ring _ _ _).range as well, and use subalgebra.copy_eq and subalgebra.equiv_of_eq to construct the various instances for subalgebra and subalgebra_of_field.

[Adam Topaz]

I won't be able to work on this any more tonight, but I'll probably have some more time tomorrow.

[Junyan Xu]

is_localization is Prop so we can just use the original proof:

instance is_localization_subalgebra :
  is_localization S (subalgebra K S hS) :=
by { dunfold localization.subalgebra, rw subalgebra.copy_eq, exact
is_localization.is_localization_of_alg_equiv S
{ commutes' := λ x, by { ext, apply is_localization.lift_eq } .. ring_equiv.of_bijective _
  ⟨ begin
      refine λ a b h, (is_localization.lift_injective_iff _).2 (λ a b, _) (subtype.ext_iff.1 h),
      exact ⟨ λ h, congr_arg _ (is_localization.injective _ hS h),
              λ h, congr_arg _ (is_fraction_ring.injective A K h) ⟩,
    end, ring_hom.range_restrict_surjective _ ⟩ } }