English
In the power series ring k[[X]], the maximal ideal is generated by X: (X).
Русский
В кольце степенных рядов k[[X]] максимальный идеал порождается X: (X).
LaTeX
$$\operatorname{maximalIdeal}(k[[X]]) = (X).$$
Lean4
/-- The maximal ideal of `k⟦X⟧` is generated by `X`. -/
theorem maximalIdeal_eq_span_X : IsLocalRing.maximalIdeal (k⟦X⟧) = Ideal.span { X } :=
by
have hX : (Ideal.span {(X : k⟦X⟧)}).IsMaximal :=
by
rw [Ideal.isMaximal_iff]
constructor
· rw [Ideal.mem_span_singleton]
exact Prime.not_dvd_one X_prime
· intro I f hI hfX hfI
rw [Ideal.mem_span_singleton, X_dvd_iff] at hfX
have hfI0 : C (f 0) ∈ I :=
by
have : C (f 0) = f - (f - C (f 0)) := by rw [sub_sub_cancel]
rw [this]
apply Ideal.sub_mem I hfI
apply hI
rw [Ideal.mem_span_singleton, X_dvd_iff, map_sub, constantCoeff_C, ← coeff_zero_eq_constantCoeff_apply,
sub_eq_zero, coeff_zero_eq_constantCoeff]
rfl
rw [← Ideal.eq_top_iff_one]
apply Ideal.eq_top_of_isUnit_mem I hfI0 (IsUnit.map C (Ne.isUnit hfX))
rw [IsLocalRing.eq_maximalIdeal hX]
