LocalDVR.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Principal maximal ideals and local factor divisibility

A nonzero principal maximal ideal in a Noetherian local domain gives a DVR and uniformizer factorizations. Its canonical additive valuation, valued in ℕ∞, splits a product of a prime power and a unit.

theorem OAI.CirculantHadamard.LocalDVR.isDiscreteValuationRing_of_maximalIdeal_eq_span line 29
Source documentation
A nonzero generator of the maximal ideal of a Noetherian local domain proves that the ring is a DVR.
```
theorem isDiscreteValuationRing_of_maximalIdeal_eq_span {π : R}
    (hπ : π ≠ 0) (hspan : maximalIdeal R = Ideal.span {π}) :
    IsDiscreteValuationRing R := by
…
```

theorem OAI.CirculantHadamard.LocalDVR.eq_unit_mul_pow_of_maximalIdeal_eq_span line 42

Source documentation

The actual chosen generator factors every nonzero element into a unit times a natural power.

theorem eq_unit_mul_pow_of_maximalIdeal_eq_span {π x : R}
    (hπ : π ≠ 0) (hspan : maximalIdeal R = Ideal.span {π}) (hx : x ≠ 0) :
    ∃ (n : ℕ) (u : Rˣ), x = (u : R) * π ^ n := by
…

theorem OAI.CirculantHadamard.LocalDVR.addVal_eq_of_unit_mul_uniformizer_pow line 56

Source documentation

Normalize the additive valuation using the concrete uniformizer relation.

theorem addVal_eq_of_unit_mul_uniformizer_pow {π p : R} {u : Rˣ} {D : ℕ}
    (hspan : maximalIdeal R = Ideal.span {π}) (hp : p = (u : R) * π ^ D) :
    addVal R p = (D : ℕ∞) :=
…

theorem OAI.CirculantHadamard.LocalDVR.addVal_eq_of_uniformizer_pow_mul_unit line 62

Source documentation

Right-unit version, convenient for the factorization of a rational prime.

theorem addVal_eq_of_uniformizer_pow_mul_unit {π p b : R} {D : ℕ}
    (hspan : maximalIdeal R = Ideal.span {π}) (hb : IsUnit b)
    (hp : p = π ^ D * b) : addVal R p = (D : ℕ∞) := by
…

theorem OAI.CirculantHadamard.LocalDVR.finite_add_eq line 68

theorem OAI.CirculantHadamard.LocalDVR.dvd_or_dvd_of_mul_eq_pow_mul_unit line 84

Source documentation

If the valuation of a product is at least twice that of p, one factor is divisible by p. The value of p is allowed to be ramified.

theorem dvd_or_dvd_of_mul_eq_pow_mul_unit {p x y b : R} {D e : ℕ}
    (_hp : p ≠ 0) (_hD : 0 < D) (hpval : addVal R p = (D : ℕ∞))
    (he : 2 ≤ e) (hb : IsUnit b) (hxy : x * y = p ^ e * b) :
    p ∣ x ∨ p ∣ y := by
…

theorem OAI.CirculantHadamard.LocalDVR.isUnit_or_isUnit_of_mul_eq_uniformizer_mul_unit line 108
Source documentation
A product with valuation one has a unit factor. This is the unramified base case of the integral division argument.
```
theorem isUnit_or_isUnit_of_mul_eq_uniformizer_mul_unit {p x y b : R}
    (hpval : addVal R p = 1) (hb : IsUnit b) (hxy : x * y = p * b) :
    IsUnit x ∨ IsUnit y := by
…
```