instance
Localization.awayProd_isLocalization_closure
{R : Type u_1}
[CommRing R]
(s : Finset R)
:
IsLocalization (Submonoid.closure ↑s) (Localization.Away (∏ i ∈ s, i))
noncomputable def
Localization.closureFinsetEquiv
{R : Type u_1}
[CommRing R]
(s : Finset R)
:
Localization (Submonoid.closure ↑s) ≃ₐ[R] Localization.Away (∏ i ∈ s, i)
Equations
- Localization.closureFinsetEquiv s = IsLocalization.algEquiv (Submonoid.closure ↑s) (Localization (Submonoid.closure ↑s)) (Localization.Away (∏ i ∈ s, i))
Instances For
@[simp]
theorem
Localization.clousreFinset_comp
{R : Type u_1}
[CommRing R]
(s : Finset R)
:
(↑(Localization.closureFinsetEquiv s)).comp (Algebra.ofId R (Localization (Submonoid.closure ↑s))) = Algebra.ofId R (Localization.Away (∏ i ∈ s, i))
@[simp]
theorem
Localization.closureFinset_symm_comp
{R : Type u_1}
[CommRing R]
(s : Finset R)
:
(↑(Localization.closureFinsetEquiv s).symm).comp (Algebra.ofId R (Localization.Away (∏ i ∈ s, i))) = Algebra.ofId R (Localization (Submonoid.closure ↑s))
instance
Localization.awayProd_isLocalization_closure'
{R : Type u_1}
[CommRing R]
{t : Set R}
(fin : t.Finite)
:
IsLocalization (Submonoid.closure t) (Localization.Away (∏ i ∈ fin.toFinset, i))
noncomputable def
Localization.closureFiniteEquiv
{R : Type u_1}
[CommRing R]
{t : Set R}
(fin : t.Finite)
:
Localization (Submonoid.closure t) ≃ₐ[R] Localization.Away (∏ i ∈ fin.toFinset, i)
Equations
- Localization.closureFiniteEquiv fin = IsLocalization.algEquiv (Submonoid.closure t) (Localization (Submonoid.closure t)) (Localization.Away (∏ i ∈ fin.toFinset, i))
Instances For
@[simp]
theorem
Localization.clousreFinite_comp
{R : Type u_1}
[CommRing R]
{t : Set R}
(fin : t.Finite)
:
(↑(Localization.closureFiniteEquiv fin)).comp (Algebra.ofId R (Localization (Submonoid.closure t))) = Algebra.ofId R (Localization.Away (∏ i ∈ fin.toFinset, i))
@[simp]
theorem
Localization.closureFininite_symm_comp
{R : Type u_1}
[CommRing R]
{t : Set R}
(fin : t.Finite)
:
(↑(Localization.closureFiniteEquiv fin).symm).comp (Algebra.ofId R (Localization.Away (∏ i ∈ fin.toFinset, i))) = Algebra.ofId R (Localization (Submonoid.closure t))
theorem
AlgebraicGeometry.IsOpenImmersion.of_map_localization_finite_closure
{R : Type u_1}
[CommRing R]
{t : Set R}
(ht : t.Finite)
: