English
Every local subring A is dominated by some valuation subring B, i.e., A ≤ B.toLocalSubring for some valuation subring B.
Русский
Каждое локальное подкольцо A доминируется некоторым оценочным подкольцом B, то есть A ≤ B.toLocalSubring.
LaTeX
$$$\\exists B:\\mathrm{ValuationSubring}(K),\\; A \\le B^{\\mathrm{toLocalSubring}}.$$$
Lean4
@[stacks 00IA]
theorem exists_le_valuationSubring (A : LocalSubring K) : ∃ B : ValuationSubring K, A ≤ B.toLocalSubring :=
by
suffices ∃ B, A ≤ B ∧ IsMax B by
obtain ⟨B, hB, hB'⟩ := this
obtain ⟨B, rfl⟩ := B.exists_valuationRing_of_isMax hB'
exact ⟨B, hB⟩
refine zorn_le_nonempty_Ici₀ _ ?_ _ le_rfl
intro s hs H y hys
have inst : Nonempty s := ⟨⟨y, hys⟩⟩
have hdir := H.directed.mono_comp _ LocalSubring.toSubring_mono
refine ⟨@LocalSubring.mk _ _ (⨆ i : s, i.1.toSubring) ⟨?_⟩, ?_⟩
· intro ⟨a, ha⟩ ⟨b, hb⟩ e
obtain ⟨A, haA : a ∈ A.1.toSubring⟩ := (Subring.mem_iSup_of_directed hdir).mp ha
obtain ⟨B, hbB : b ∈ B.1.toSubring⟩ := (Subring.mem_iSup_of_directed hdir).mp hb
obtain ⟨C, hCA, hCB⟩ := hdir A B
refine (C.1.2.2 (a := ⟨a, hCA haA⟩) (b := ⟨b, hCB hbB⟩) (Subtype.ext congr(($e).1))).imp ?_ ?_
· exact fun h ↦ h.map (Subring.inclusion (le_iSup (fun i : s ↦ i.1.toSubring) C))
· exact fun h ↦ h.map (Subring.inclusion (le_iSup (fun i : s ↦ i.1.toSubring) C))
· intro A hA
refine ⟨le_iSup (fun i : s ↦ i.1.toSubring) ⟨A, hA⟩, ⟨?_⟩⟩
rintro ⟨a, haA⟩ h
obtain ⟨⟨b, hb⟩, e⟩ := isUnit_iff_exists_inv.mp h
obtain ⟨B, hbB : b ∈ B.1.toSubring⟩ := (Subring.mem_iSup_of_directed hdir).mp hb
obtain ⟨C, hCA, hCB⟩ := H.directed ⟨A, hA⟩ B
apply hCA.2.1
exact isUnit_iff_exists_inv.mpr ⟨⟨b, hCB.1 hbB⟩, Subtype.ext congr(($e).1)⟩
