of_finite_maximals_of_isUnit — Mathlib

English

If an invertible fractional ideal becomes principal after a suitable map, then the original ideal is principal.

Русский

Если обратимый дробный идеал становится главным после подходящего отображения, то исходный идеал — главный.

LaTeX

$$$$\\text{Principal after map} \\Rightarrow \\text{Principal}$$$$

Lean4

/-- An invertible ideal in a commutative ring with finitely many maximal ideals is principal.

https://math.stackexchange.com/a/95857 -/
theorem of_finite_maximals_of_isUnit (hf : {I : Ideal R | I.IsMaximal}.Finite) {I : Ideal R}
    (hI : IsUnit (I : FractionalIdeal R⁰ (FractionRing R))) : I.IsPrincipal :=
  (IsLocalization.coeSubmodule_isPrincipal _ le_rfl).mp
    (FractionalIdeal.isPrincipal.of_finite_maximals_of_inv le_rfl hf I
      (↑hI.unit⁻¹ : FractionalIdeal R⁰ (FractionRing R)) hI.unit.mul_inv)

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