Locality of Algebra.FiniteType #
In this file we show that finite-type is local on the source and the target.
Main results #
Algebra.FiniteType.of_span_eq_top_source: finite-type is local on the (algebraic) sourceAlgebra.FiniteType.of_span_eq_top_target: finite-type is local on the (algebraic) target
theorem
IsLocalization.exists_smul_mem_of_mem_adjoin
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
{S' : Type u_4}
[CommRing S']
[Algebra S S']
[Algebra R S']
[IsScalarTower R S S']
(M : Submonoid S)
[IsLocalization M S']
(x : S)
(s : Finset S')
(A : Subalgebra R S)
(hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A)
(hA₂ : M ≤ A.toSubmonoid)
(hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s)
:
Let S be an R-algebra, M a submonoid of S, S' = M⁻¹S.
Suppose the image of some x : S falls in the adjoin of some finite s ⊆ S' over R,
and A is an R-subalgebra of S containing both M and the numerators of s.
Then, there exists some m : M such that m • x falls in A.
theorem
IsLocalization.lift_mem_adjoin_finsetIntegerMultiple
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Submonoid R)
{S' : Type u_4}
[CommRing S']
[Algebra S S']
[Algebra R S']
[IsScalarTower R S S']
[IsLocalization (Submonoid.map (algebraMap R S) M) S']
(x : S)
(s : Finset S')
(hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s)
:
∃ (m : ↥M), m • x ∈ Algebra.adjoin R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
Let S be an R-algebra, M a submonoid of R, and S' = M⁻¹S.
If the image of some x : S falls in the adjoin of some finite s ⊆ S' over R,
then there exists some m : M such that m • x falls in the
adjoin of IsLocalization.finsetIntegerMultiple _ s over R.
theorem
Algebra.FiniteType.of_span_eq_top_target
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(s : Set S)
(hs : Ideal.span s = ⊤)
(h : ∀ x ∈ s, FiniteType R (Localization.Away x))
:
FiniteType R S
Finite-type can be checked on a standard covering of the target.
theorem
Algebra.FiniteType.of_span_eq_top_source
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(s : Set R)
(hs : Ideal.span s = ⊤)
(h : ∀ i ∈ s, FiniteType (Localization.Away i) (TensorProduct R (Localization.Away i) S))
:
FiniteType R S