The meta properties of finite ring homomorphisms.

Main results

Let R be a commutative ring, S is an R-algebra, M be a submonoid of R.

• finite_localizationPreserves : If S is a finite R-algebra, then S' = M⁻¹S is a finite R' = M⁻¹R-algebra.
• finite_ofLocalizationSpan : S is a finite R-algebra if there exists a set { r } that spans R such that Sᵣ is a finite Rᵣ-algebra.

theorem RingHom.finite_stableUnderComposition : RingHom.StableUnderComposition @RingHom.Finite

theorem RingHom.finite_respectsIso : RingHom.RespectsIso @RingHom.Finite

theorem RingHom.finite_containsIdentities : RingHom.ContainsIdentities @RingHom.Finite

theorem RingHom.finite_isStableUnderBaseChange : RingHom.IsStableUnderBaseChange @RingHom.Finite

theorem Module.Finite_of_isLocalization (R : Type u_1) (S : Type u_2) (Rₚ : Type u_3) (Sₚ : Type u_4) [CommSemiring R] [CommRing S] [CommRing Rₚ] [CommRing Sₚ] [Algebra R S] [Algebra R Rₚ] [Algebra R Sₚ] [Algebra S Sₚ] [Algebra Rₚ Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] (M : Submonoid R) [IsLocalization M Rₚ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [hRS : Module.Finite R S] : Module.Finite Rₚ Sₚ

theorem RingHom.finite_localizationPreserves : RingHom.LocalizationPreserves @RingHom.Finite

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

theorem RingHom.localization_away_map_finite {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (R' S' : Type u) [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] (hf : f.Finite) : (IsLocalization.Away.map R' S' f r).Finite

theorem IsLocalization.smul_mem_finsetIntegerMultiple_span {R S : Type u} [CommRing R] [CommRing S] (M : Submonoid R) (S' : Type u) [CommRing S'] [Algebra S S'] [Algebra R 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 ∈ Submodule.span R ↑s) : ∃ (m : ↥M), m • x ∈ Submodule.span R ↑(IsLocalization.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 span of some finite s ⊆ S' over R, then there exists some m : M such that m • x falls in the span of IsLocalization.finsetIntegerMultiple _ s over R.

theorem multiple_mem_span_of_mem_localization_span {R : Type u} [CommRing R] (M : Submonoid R) (R' : Type u) [CommRing R'] [Algebra R R'] {N : Type u_1} [AddCommMonoid N] [Module R N] [Module R' N] [IsScalarTower R R' N] [IsLocalization M R'] (s : Set N) (x : N) (hx : x ∈ Submodule.span R' s) : ∃ (t : ↥M), t • x ∈ Submodule.span R s

If M is an R' = S⁻¹R module, and x ∈ span R' s, then t • x ∈ span R s for some t : S.

theorem multiple_mem_adjoin_of_mem_localization_adjoin {R S : Type u} [CommRing R] [CommRing S] (M : Submonoid R) (R' : Type u) [CommRing R'] [Algebra R R'] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S] [IsLocalization M R'] (s : Set S) (x : S) (hx : x ∈ Algebra.adjoin R' s) : ∃ (t : ↥M), t • x ∈ Algebra.adjoin R s

If S is an R' = M⁻¹R algebra, and x ∈ adjoin R' s, then t • x ∈ adjoin R s for some t : M.

theorem RingHom.finite_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom.Finite

S is a finite R-algebra if there exists a set { r } that spans R such that Sᵣ is a finite Rᵣ-algebra.