English
The prime coarsening recovers the target S when starting from R and idealOfLE.
Русский
Начав с R и idealOfLE, простое упрощение восстанавливает S.
LaTeX
$$ofPrime R (idealOfLE R S h) = S$$
Lean4
@[simp]
theorem ofPrime_idealOfLE (R S : ValuationSubring K) (h : R ≤ S) : ofPrime R (idealOfLE R S h) = S :=
by
ext x; constructor
· rintro ⟨a, r, hr, rfl⟩; apply mul_mem; · exact h a.2
· rw [← valuation_le_one_iff, map_inv₀, ← inv_one, inv_le_inv₀]
· exact not_lt.1 ((not_iff_not.2 <| valuation_lt_one_iff S _).1 hr)
· simpa [Valuation.pos_iff] using fun hr₀ ↦ hr₀ ▸ hr <| Ideal.zero_mem (R.idealOfLE S h)
· exact zero_lt_one
· intro hx; by_cases hr : x ∈ R; · exact R.le_ofPrime _ hr
have : x ≠ 0 := fun h => hr (by rw [h]; exact R.zero_mem)
replace hr := (R.mem_or_inv_mem x).resolve_left hr
refine ⟨1, ⟨x⁻¹, hr⟩, ?_, ?_⟩
· simp only [Ideal.primeCompl, Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_compl_iff, SetLike.mem_coe, idealOfLE,
Ideal.mem_comap, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, not_not]
change IsUnit (⟨x⁻¹, h hr⟩ : S)
apply isUnit_of_mul_eq_one _ (⟨x, hx⟩ : S)
ext; simp [field]
· simp
