English
If an invertible fractional ideal I over the localized ring corresponds to a unit under the localization, then I is principal.
Русский
Если обратимый дробный идеал I над локализованной окружностью соответствует единице под локализацией, то I — главный идеал.
LaTeX
$$$$I^{\\flat} \\text{ principal}$$$$
Lean4
/-- An invertible fractional ideal of a commutative ring with finitely many maximal ideals is principal.
https://math.stackexchange.com/a/95857 -/
theorem of_finite_maximals_of_inv {A : Type*} [CommRing A] [Algebra R A] {S : Submonoid R} [IsLocalization S A]
(hS : S ≤ R⁰) (hf : {I : Ideal R | I.IsMaximal}.Finite) (I I' : FractionalIdeal S A) (hinv : I * I' = 1) :
Submodule.IsPrincipal (I : Submodule R A) := by
have hinv' := hinv
rw [coe_ext_iff, coe_mul] at hinv
let s := hf.toFinset
haveI := Classical.decEq (Ideal R)
have coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤ :=
by
simp_rw [s, Finset.mem_erase, hf.mem_toFinset]
rintro M hM M' ⟨hne, hM'⟩
exact Ideal.IsMaximal.coprime_of_ne hM hM' hne.symm
have nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M := fun M hM =>
left_lt_sup.1 ((hf.mem_toFinset.1 hM).ne_top.lt_top.trans_eq (Ideal.sup_iInf_eq_top <| coprime M hM).symm)
have : ∀ M ∈ s, ∃ a ∈ I, ∃ b ∈ I', a * b ∉ IsLocalization.coeSubmodule A M :=
by
intro M hM; by_contra! h
obtain ⟨x, hx, hxM⟩ :=
SetLike.exists_of_lt
((IsLocalization.coeSubmodule_strictMono hS (hf.mem_toFinset.1 hM).ne_top.lt_top).trans_eq hinv.symm)
exact hxM (Submodule.mul_le.2 h hx)
choose! a ha b hb hm using this
choose! u hu hum using fun M hM => SetLike.not_le_iff_exists.1 (nle M hM)
let v := ∑ M ∈ s, u M • b M
have hv : v ∈ I' := Submodule.sum_mem _ fun M hM => Submodule.smul_mem _ _ <| hb M hM
refine
FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top (Units.mkOfMulEqOne I I' hinv') hv
(of_not_not fun h => ?_)
obtain ⟨M, hM, hJM⟩ := Ideal.exists_le_maximal _ h
replace hM := hf.mem_toFinset.2 hM
have : ∀ a ∈ I, ∀ b ∈ I', ∃ c, algebraMap R _ c = a * b :=
by
intro a ha b hb; have hi := hinv.le
obtain ⟨c, -, hc⟩ := hi (Submodule.mul_mem_mul ha hb)
exact ⟨c, hc⟩
have hmem : a M * v ∈ IsLocalization.coeSubmodule A M :=
by
obtain ⟨c, hc⟩ := this _ (ha M hM) v hv
refine IsLocalization.coeSubmodule_mono _ hJM ⟨c, ?_, hc⟩
have := Submodule.mul_mem_mul (ha M hM) (Submodule.mem_span_singleton_self v)
rwa [← hc] at this
simp_rw [v, Finset.mul_sum, mul_smul_comm] at hmem
rw [← s.add_sum_erase _ hM, Submodule.add_mem_iff_left] at hmem
· refine hm M hM ?_
obtain ⟨c, hc : algebraMap R A c = a M * b M⟩ := this _ (ha M hM) _ (hb M hM)
rw [← hc] at hmem ⊢
rw [Algebra.smul_def, ← map_mul] at hmem
obtain ⟨d, hdM, he⟩ := hmem
rw [IsLocalization.injective _ hS he] at hdM
exact
Submodule.mem_map_of_mem (f := Algebra.linearMap _ _)
(((hf.mem_toFinset.1 hM).isPrime.mem_or_mem hdM).resolve_left <| hum M hM)
· refine Submodule.sum_mem _ fun M' hM' => ?_
rw [Finset.mem_erase] at hM'
obtain ⟨c, hc⟩ := this _ (ha M hM) _ (hb M' hM'.2)
rw [← hc, Algebra.smul_def, ← map_mul]
specialize hu M' hM'.2
simp_rw [Ideal.mem_iInf, Finset.mem_erase] at hu
exact Submodule.mem_map_of_mem (f := Algebra.linearMap _ _) (M.mul_mem_right _ <| hu M ⟨hM'.1.symm, hM⟩)
