English
For a finite subset σ ⊆ S, the localization condition is equivalent to the following: every s ∈ S can be written as s = u^{-1} t with u a unit in adjoin(R,σ) and t ∈ adjoin(R,σ).
Русский
Для конечного подмножества σ ⊆ S локализационное условие эквивалентно тому, что каждый элемент s ∈ S можно записать как s = u^{-1} t, где u — единица в adjoin(R,σ), a t ∈ adjoin(R,σ).
LaTeX
$$$IsLocalization\ (IsUnit.submonoid S).comap (algebraMap (Subtype fun x => x.1 ∈ σ) S) S \iff\forall s\in S, \exists t\in Adjoin(R,σ), IsUnit t ∧ s t\in Adjoin(R,σ)$$$
Lean4
theorem essFiniteType_cond_iff (σ : Finset S) :
IsLocalization ((IsUnit.submonoid S).comap (algebraMap (adjoin R (σ : Set S)) S)) S ↔
(∀ s : S, ∃ t ∈ Algebra.adjoin R (σ : Set S), IsUnit t ∧ s * t ∈ Algebra.adjoin R (σ : Set S)) :=
by
constructor <;> intro hσ
· intro s
obtain ⟨⟨⟨x, hx⟩, ⟨t, ht⟩, ht'⟩, h⟩ := hσ.2 s
exact ⟨t, ht, ht', h ▸ hx⟩
· constructor
· exact fun y ↦ y.prop
· intro s
obtain ⟨t, ht, ht', h⟩ := hσ s
exact ⟨⟨⟨_, h⟩, ⟨t, ht⟩, ht'⟩, rfl⟩
· intro x y e
exact ⟨1, by simpa using Subtype.ext e⟩
