Documentation

Mathlib.RingTheory.RingHom.FiniteType

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 : If S is a finite type R-algebra, then S' = M⁻¹S is a finite type R' = M⁻¹R-algebra.
finiteType_ofLocalizationSpan : S is a finite type R-algebra if there exists a set { r } that spans R such that Sᵣ is a finite type Rᵣ-algebra. *RingHom.finiteType_isLocal: RingHom.FiniteType is a local property.

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) :

∃ (m : ↥M), m • x ∈ A

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)) :

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)) :

theorem RingHom.finiteType_stableUnderComposition :

StableUnderComposition @FiniteType

theorem RingHom.finiteType_respectsIso :

RespectsIso @FiniteType

theorem RingHom.finiteType_isStableUnderBaseChange :

IsStableUnderBaseChange @FiniteType

theorem RingHom.finiteType_localizationPreserves :

LocalizationPreserves @FiniteType

If S is a finite type R-algebra, then S' = M⁻¹S is a finite type R' = M⁻¹R-algebra.

theorem RingHom.localization_away_map_finiteType (R S R' S' : Type u) [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R R'] (f : R →+* S) [Algebra S S'] (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] (hf : f.FiniteType) :

(IsLocalization.Away.map R' S' f r).FiniteType

theorem RingHom.finiteType_ofLocalizationSpan :

OfLocalizationSpan @FiniteType

theorem RingHom.finiteType_holdsForLocalizationAway :

HoldsForLocalizationAway @FiniteType

theorem RingHom.finiteType_ofLocalizationSpanTarget :

OfLocalizationSpanTarget @FiniteType

theorem RingHom.finiteType_isLocal :

PropertyIsLocal @FiniteType

@[deprecated RingHom.finiteType_isLocal (since := "2025-03-01")]

theorem RingHom.finiteType_is_local :

PropertyIsLocal @FiniteType

Alias of RingHom.finiteType_isLocal.

@[deprecated IsLocalization.lift_mem_adjoin_finsetIntegerMultiple (since := "2025-03-14")]

theorem RingHom.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 ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

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.

@[deprecated IsLocalization.exists_smul_mem_of_mem_adjoin (since := "2025-03-14")]

theorem RingHom.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₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A) (hA₂ : M ≤ A.toSubmonoid) (hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s) :

∃ (m : ↥M), m • x ∈ A

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.