mk_surjective — Mathlib

English

The image of the awayMap under mk covers the range of the base valuation map.

Русский

Образ awayMap через mk покрывает диапазон исходного отображения value.

LaTeX

$$$$ \text{range}(Away 𝒜 hg hx) \subseteq \text{range}(\mathrm{val}). $$$$

Lean4

protected theorem mk_surjective {d : ι} (hf : f ∈ 𝒜 d) (x : Away 𝒜 f) : ∃ n a ha, Away.mk 𝒜 hf n a ha = x :=
  by
  obtain ⟨⟨N, ⟨s, hs⟩, ⟨b, hn⟩, ⟨n, (rfl : _ = b)⟩⟩, rfl⟩ := mk_surjective x
  by_cases hfn : f ^ n = 0
  · have := HomogeneousLocalization.subsingleton 𝒜 (x := .powers f) ⟨n, hfn⟩
    exact ⟨0, 0, zero_mem _, Subsingleton.elim _ _⟩
  obtain rfl := DirectSum.degree_eq_of_mem_mem 𝒜 hn (SetLike.pow_mem_graded n hf) hfn
  exact ⟨n, s, hs, by ext; simp⟩

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