map_algebraMap_eq_valuationSubring

English

The image of the top subring under the algebra map equals the valuation subring associated to the maximal ideal of A.

Русский

Изображение верхнего подкольца под алгебраическим отображением равно оценочному подкольцу, ассоциированному с максимальным идеалом A.

LaTeX

$$$ \\mathrm{Subring.map}(\\mathrm{algebraMap}\\ A\\ K)\\ (\\top) = \\big( (\\maximalIdeal A).valuation K\\big).valuationSubring\\text{.toSubring} $$$

Lean4

theorem map_algebraMap_eq_valuationSubring :
    Subring.map (algebraMap A K) ⊤ = ((maximalIdeal A).valuation K).valuationSubring.toSubring :=
  by
  ext
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨_, _, rfl⟩ := Subring.mem_map.mp h
    apply valuation_le_one
  · obtain ⟨y, rfl⟩ := exists_lift_of_le_one h
    rw [Subring.mem_map]
    exact ⟨y, mem_top _, rfl⟩

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