feat(RingTheory/Valuation/Discrete/Basic): add exists_zpow_Uniformizer

[mariainesdff]

Co-authored-by: @Louddy

---

[github-actions]

PR summary 108075f42a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ exists_zpow_Uniformizer

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[erdOne]

I am a bit confused about the state of this part of the library but isn't the right thing to do to show that the valuation subring is a DVR and to use the DVR API?

Or is this lemma useful in showing that?

[mariainesdff]

I am a bit confused about the state of this part of the library but isn't the right thing to do to show that the valuation subring is a DVR and to use the DVR API?

Or is this lemma useful in showing that?

@faenuccio and I already proved that (see Valuation.valuationSubring_isDiscreteValuationRing.

I am adding this lemma for completeness of the API.

[erdOne]

In that case, I think the right lemma should be

theorem div_smul_div_comm {G K : Type*}
    [Group G] [Field K] [DistribMulAction G K] [IsScalarTower G K K]
    (g h : G) (a b : K) (hb : b ≠ 0) :  
    (g / h) • (a / b) = (g • a) / (h • b) := by
  rw [eq_div_iff_mul_eq (ne_of_apply_ne (h⁻¹ • ·) (by simpa)), smul_mul_smul_comm]
  simp [hb]
 
lemma IsDiscreteValuationRing.exists_units_eq_smul_zpow_of_irreducible
    {R K : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    [Field K] [Algebra R K] [IsFractionRing R K] {ϖ : R} (hϖ : Irreducible ϖ) (x : K) (hx : x ≠ 0) :
    ∃ (n : ℤ) (u : Rˣ), x = u • algebraMap R K ϖ ^ n := by
  obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := R) x
  obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible (x := x) (by simp_all) hϖ
  obtain ⟨m, v, rfl⟩ := eq_unit_mul_pow_irreducible (by simpa using hy) hϖ
  have hϖ' : algebraMap R K ϖ ≠ 0 := by simpa using hϖ.ne_zero
  refine ⟨n - m, u / v, ?_⟩
  simp [hϖ', zpow_sub₀, div_smul_div_comm, Units.smul_def u, Units.smul_def v, Algebra.smul_def]

[mariainesdff]

In that case, I think the right lemma should be

I think that the version I am proposing is more consistent with Valuation.exists_pow_Uniformizer (this lemma is just supposed to be the zpow version of that one).

[erdOne]

I don't think one should use Valuation.exists_pow_Uniformizer at all. One should just add IsUniformizer.irreducible and use IsDiscreteValuationRing.eq_unit_mul_pow_irreducible. I would even claim that Valuation.exists_pow_Uniformizer should be private.

More generally, it seems like there is some duplication going on about DVRs on field, and we should think (or have a discussion on Zulip) about what API to provide. My initial guess would be that the general picture is

{R K v} [CommRIng R] [Field K] [Algebra R K] [IsFractionRing R K]
[v.IsRankOneDiscrete] [v.IsIntegers R] [IsDiscreteValuationRing R] 

And for each statement, we take the subset of the above variables that appear in the statement. In particular, for this particular theorem, the statement doesn't mention v so we shouldn't assume the existence of such a v, and the theorem should be stated in terms of general R instead of only for the v.integers.