The meta properties of finite-type ring homomorphisms. #
Main results #
Let R
be a commutative ring, S
is an R
-algebra, M
be a submonoid of R
.
finiteType_localizationPreserves
: IfS
is a finite typeR
-algebra, thenS' = M⁻¹S
is a finite typeR' = M⁻¹R
-algebra.finiteType_ofLocalizationSpan
:S
is a finite typeR
-algebra if there exists a set{ r }
that spansR
such thatSᵣ
is a finite typeRᵣ
-algebra. *RingHom.finiteType_isLocal
:RingHom.FiniteType
is a local property.
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
.
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
.
Finite-type can be checked on a standard covering of the target.
If S
is a finite type R
-algebra, then S' = M⁻¹S
is a finite type R' = M⁻¹R
-algebra.
Alias of RingHom.finiteType_isLocal
.
Alias of IsLocalization.lift_mem_adjoin_finsetIntegerMultiple
.
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
.
Alias of IsLocalization.exists_smul_mem_of_mem_adjoin
.
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
.