noncomputable def DVRIntersection {F : Type u_1} [Field F] (n : ℕ) (v : Fin n → AddValuation F (WithTop ℤ)) : Subring F

The intersection $\bigcap_i R_{v_i}$ of the valuation subrings of finitely many discrete valuations $v_i$ on a field $F$, viewed as a subring of $F$.

instance DVRIntersection_IsDomain {F : Type u_1} [Field F] (n : ℕ) (v : Fin n → AddValuation F (WithTop ℤ)) : IsDomain ↥(DVRIntersection n v)

A subring of a field is an integral domain; in particular the intersection of valuation subrings is a domain.

theorem val_zero_mem {F : Type u_1} [Field F] {n : ℕ} {v : Fin n → AddValuation F (WithTop ℤ)} {x : F} (hv : ∀ (i : Fin n), (v i) x = ↑0) : x ∈ DVRIntersection n v

An element with valuation $0$ under all $v_i$ lies in the intersection $\bigcap_i R_{v_i}$.

theorem val_zero_inv_mem {F : Type u_1} [Field F] {n : ℕ} {v : Fin n → AddValuation F (WithTop ℤ)} {x : F} (hv : ∀ (i : Fin n), (v i) x = ↑0) : x⁻¹ ∈ DVRIntersection n v

If every $v_i x = 0$, then $x^{-1}$ also has all valuations $0$ and so lies in the intersection.

theorem isUnit_of_val_zero {F : Type u_1} [Field F] {n : ℕ} {v : Fin n → AddValuation F (WithTop ℤ)} {x : F} (hx : x ≠ 0) (hv : ∀ (i : Fin n), (v i) x = ↑0) : IsUnit ⟨x, ⋯⟩

A nonzero element with all valuations equal to $0$ is a unit in the intersection $\bigcap_i R_{v_i}$.

theorem val_nonneg_int {F : Type u_1} [Field F] {n : ℕ} {v : Fin n → AddValuation F (WithTop ℤ)} {x : F} (hx : x ≠ 0) (hmem : x ∈ DVRIntersection n v) (i : Fin n) : ∃ (a : ℕ), (v i) x = ↑↑a

For a nonzero element $x$ of the intersection, each valuation $v_i(x)$ equals a nonnegative integer.

theorem not_isUnit_of_inv_not_mem {F : Type u_1} [Field F] {n : ℕ} {v : Fin n → AddValuation F (WithTop ℤ)} {x : F} (hx_mem : x ∈ DVRIntersection n v) (hxi_not_mem : x⁻¹ ∉ DVRIntersection n v) : ¬IsUnit ⟨x, hx_mem⟩

If $x \in R$ but $x^{-1} \notin R$, then $x$ is not a unit in $R$.

theorem withtop_neg_coe (a : ℤ) : -↑a = ↑(-a)

Commuting negation with coercion $\mathbb{Z} \hookrightarrow \mathbb{Z} \cup \{\infty\}$.

theorem withtop_coe_nonneg {a : ℤ} (ha : 0 ≤ a) : 0 ≤ ↑a

Coercion $\mathbb{Z} \hookrightarrow \mathbb{Z} \cup \{\infty\}$ preserves nonnegativity.

theorem withtop_not_nonneg_neg_one (h : 0 ≤ -1) : False

$-1$ is not nonnegative in $\mathbb{Z} \cup \{\infty\}$.

theorem uniformizer_mem {F : Type u_1} [Field F] {n : ℕ} {v : Fin n → AddValuation F (WithTop ℤ)} {t : Fin n → F} (ht : ∀ (i j : Fin n), (v i) (t j) = ↑(if i = j then 1 else 0)) (j : Fin n) : t j ∈ DVRIntersection n v

A simultaneous uniformizer $t_j$ (with $v_i(t_j) = \delta_{ij}$) lies in $\bigcap_i R_{v_i}$.

theorem uniformizer_ne_zero {F : Type u_1} [Field F] {n : ℕ} {v : Fin n → AddValuation F (WithTop ℤ)} {t : Fin n → F} (ht : ∀ (i j : Fin n), (v i) (t j) = ↑(if i = j then 1 else 0)) (j : Fin n) : t j ≠ 0

A simultaneous uniformizer $t_j$ is nonzero (since $v_j(t_j) = 1 \neq \infty$).

theorem uniformizer_prime {F : Type u_1} [Field F] {n : ℕ} {v : Fin n → AddValuation F (WithTop ℤ)} {t : Fin n → F} (ht : ∀ (i j : Fin n), (v i) (t j) = ↑(if i = j then 1 else 0)) (j : Fin n) : Prime ⟨t j, ⋯⟩

Each simultaneous uniformizer $t_j$ is a prime element of the intersection $\bigcap_i R_{v_i}$.

theorem uniformizer_ideal_isPrime {F : Type u_1} [Field F] {n : ℕ} {v : Fin n → AddValuation F (WithTop ℤ)} {t : Fin n → F} (ht : ∀ (i j : Fin n), (v i) (t j) = ↑(if i = j then 1 else 0)) (j : Fin n) : (Ideal.span {⟨t j, ⋯⟩}).IsPrime

The principal ideal generated by a simultaneous uniformizer $t_j$ is a prime ideal of $\bigcap_i R_{v_i}$.

theorem dvr_intersection_factorization {F : Type u_1} [Field F] {n : ℕ} (v : Fin n → AddValuation F (WithTop ℤ)) (t : Fin n → F) (ht : ∀ (i j : Fin n), (v i) (t j) = ↑(if i = j then 1 else 0)) (a : F) (ha_ne : a ≠ 0) (ha_mem : a ∈ DVRIntersection n v) : ∃ (e : Fin n → ℕ) (u : (↥(DVRIntersection n v))ˣ), (∀ (i : Fin n), (v i) a = ↑↑(e i)) ∧ ⟨a, ha_mem⟩ = ↑u * ∏ j : Fin n, ⟨t j, ⋯⟩ ^ e j

Factorization in the intersection of DVRs: every nonzero $a \in \bigcap_i R_{v_i}$ factors uniquely as $a = u \cdot \prod_j t_j^{v_j(a)}$ with $u$ a unit.

theorem mem_uniformizer_ideal_iff {F : Type u_1} [Field F] {n : ℕ} {v : Fin n → AddValuation F (WithTop ℤ)} {t : Fin n → F} (ht : ∀ (i j : Fin n), (v i) (t j) = ↑(if i = j then 1 else 0)) (j : Fin n) (x : ↥(DVRIntersection n v)) : x ∈ Ideal.span {⟨t j, ⋯⟩} ↔ 1 ≤ (v j) ↑x

Membership in the prime ideal $(t_j)$: $x \in (t_j) \iff v_j(x) \geq 1$.

theorem nonunit_in_some_uniformizer_ideal {F : Type u_1} [Field F] {n : ℕ} {v : Fin n → AddValuation F (WithTop ℤ)} {t : Fin n → F} (ht : ∀ (i j : Fin n), (v i) (t j) = ↑(if i = j then 1 else 0)) (x : ↥(DVRIntersection n v)) (hx_ne : x ≠ 0) (hx_nu : ¬IsUnit x) : ∃ (j : Fin n), x ∈ Ideal.span {⟨t j, ⋯⟩}

Any nonzero non-unit element of $\bigcap_i R_{v_i}$ lies in some uniformizer prime ideal $(t_j)$.