inf_prime_pow_eq_prod — Mathlib

English

In a Dedekind domain, for a finite family of pairwise distinct prime ideals f_i with exponents e_i, the intersection of the powers f_i^{e_i} equals the product of the powers.

Русский

В кольце Дедекинда для конечной семейства взаимно простых простых идеалов f_i с экспонентами e_i пересечение степеней f_i^{e_i} равно произведению этих степеней.

LaTeX

$$$\displaystyle \bigcap_{i\in s} f_i^{e_i} = \prod_{i\in s} f_i^{e_i}$$$

Lean4

/-- The intersection of distinct prime powers in a Dedekind domain is the product of these
prime powers. -/
theorem inf_prime_pow_eq_prod {ι : Type*} (s : Finset ι) (f : ι → Ideal R) (e : ι → ℕ) (prime : ∀ i ∈ s, Prime (f i))
    (coprime : ∀ᵉ (i ∈ s) (j ∈ s), i ≠ j → f i ≠ f j) : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i :=
  by
  letI := Classical.decEq ι
  revert prime coprime
  refine s.induction ?_ ?_
  · simp
  intro a s ha ih prime coprime
  specialize
    ih (fun i hi => prime i (Finset.mem_insert_of_mem hi)) fun i hi j hj =>
      coprime i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj)
  rw [Finset.inf_insert, Finset.prod_insert ha, ih]
  refine le_antisymm (Ideal.le_mul_of_no_prime_factors ?_ inf_le_left inf_le_right) Ideal.mul_le_inf
  intro P hPa hPs hPp
  obtain ⟨b, hb, hPb⟩ := hPp.prod_le.mp hPs
  haveI := Ideal.isPrime_of_prime (prime a (Finset.mem_insert_self a s))
  haveI := Ideal.isPrime_of_prime (prime b (Finset.mem_insert_of_mem hb))
  refine coprime a (Finset.mem_insert_self a s) b (Finset.mem_insert_of_mem hb) ?_ ?_
  · exact (ne_of_mem_of_not_mem hb ha).symm
  · refine
      ((Ring.DimensionLeOne.prime_le_prime_iff_eq ?_).mp (hPp.le_of_pow_le hPa)).trans
        ((Ring.DimensionLeOne.prime_le_prime_iff_eq ?_).mp (hPp.le_of_pow_le hPb)).symm
    · exact (prime a (Finset.mem_insert_self a s)).ne_zero
    · exact (prime b (Finset.mem_insert_of_mem hb)).ne_zero

Похожие утверждения