maximalIdeal_comap_algebraMap_eq_maximalIdeal

English

The comap of the extension map sends the maximal ideal of the larger valuation subring to the maximal ideal of the smaller valuation subring; hence LiesOver relation holds.

Русский

Обратное отображение расширения отправляет максимальный идеал большего подкольца к максимальному идеалу меньшего; следовательно, выполняется отношение LiesOver.

LaTeX

$$$(\\maximalIdeal L_0).\\mathrm{comap}(\\mathrm{algebraMap}_{K_0,L_0}) = \\ maximalIdeal K_0$$$

Lean4

theorem maximalIdeal_comap_algebraMap_eq_maximalIdeal : (maximalIdeal L₀).comap (algebraMap K₀ L₀) = maximalIdeal K₀ :=
  Ideal.ext fun _ ↦ by rw [Ideal.mem_comap, algebraMap_mem_maximalIdeal_iff]

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