Quasi-finite algebras

In this file, we define the notion of quasi-finite algebras and prove basic properties about them

Main definition and results

• Algebra.QuasiFinite: The class of quasi-finite algebras. We say that an R-algebra S is quasi-finite if κ(p) ⊗[R] S is finite-dimensional over κ(p) for all primes p of R.
• Algebra.QuasiFinite.finite_comap_preimage_singleton: Quasi-finite algebras have finite fibers.
• Algebra.QuasiFinite.iff_of_isArtinianRing: Over an artinian ring, an algebra is quasi-finite iff it is module-finite.
• Algebra.QuasiFinite.iff_finite_comap_preimage_singleton: For a finite-type R-algebra S, S is quasi-finite if and only if Spec S → Spec R has finite fibers.
• Algebra.QuasiFiniteAt: If S is an R-algebra and p a prime of S, we say that S is R-quasi-finite at p if Sₚ is R-quasi-finite.

class Algebra.QuasiFinite (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] : Prop

We say that an R-algebra S is quasi-finite if κ(p) ⊗[R] S is finite-dimensional over κ(p) for all primes p of R.

This is slightly different from the stacks projects definition, which requires S to be of finite type over R.

Also see Algebra.QuasiFinite.iff_finite_comap_preimage_singleton that this is equivalent to having finite fibers for finite-type algebas.

• finite_fiber (P : Ideal R) [P.IsPrime] : Module.Finite P.ResidueField (P.Fiber S)

theorem Algebra.quasiFinite_iff (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] : QuasiFinite R S ↔ autoParam (∀ (P : Ideal R) [inst : P.IsPrime], Module.Finite P.ResidueField (P.Fiber S)) QuasiFinite.finite_fiber._autoParam

Stacks Tag 00PM

instance Algebra.QuasiFinite.instIsArtinianRingFiber {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [QuasiFinite R S] (P : Ideal R) [P.IsPrime] : IsArtinianRing (P.Fiber S)

theorem Algebra.QuasiFinite.finite_comap_preimage_singleton {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [QuasiFinite R S] (P : PrimeSpectrum R) : (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {P}).Finite

theorem Algebra.QuasiFinite.finite_primesOver {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [QuasiFinite R S] (I : Ideal R) : (I.primesOver S).Finite

theorem Algebra.QuasiFinite.finite_comap_preimage {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [QuasiFinite R S] {s : Set (PrimeSpectrum R)} (hs : s.Finite) : (PrimeSpectrum.comap (algebraMap R S) ⁻¹' s).Finite

theorem Algebra.QuasiFinite.isDiscrete_comap_preimage_singleton {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [QuasiFinite R S] (P : PrimeSpectrum R) : IsDiscrete (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {P})

theorem Algebra.QuasiFinite.isDiscrete_comap_preimage {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [QuasiFinite R S] {s : Set (PrimeSpectrum R)} (hs : IsDiscrete s) : IsDiscrete (PrimeSpectrum.comap (algebraMap R S) ⁻¹' s)

@[instance 100]

instance Algebra.QuasiFinite.instOfFinite {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S] : QuasiFinite R S

instance Algebra.QuasiFinite.baseChange {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [QuasiFinite R S] {A : Type u_4} [CommRing A] [Algebra R A] : QuasiFinite A (TensorProduct R A S)

Stacks Tag 00PP ((3))

theorem Module.Finite.of_quasiFinite {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsArtinianRing R] [Algebra.QuasiFinite R S] : Module.Finite R S

theorem Algebra.QuasiFinite.iff_of_isArtinianRing {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsArtinianRing R] : QuasiFinite R S ↔ Module.Finite R S

theorem Algebra.QuasiFinite.trans (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [QuasiFinite R S] [QuasiFinite S T] : QuasiFinite R T

Stacks Tag 00PO

theorem Algebra.QuasiFinite.of_surjective_algHom {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [QuasiFinite R S] (f : S →ₐ[R] T) (hf : Function.Surjective ⇑f) : QuasiFinite R T

instance Algebra.QuasiFinite.instQuotientIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (I : Ideal S) [QuasiFinite R S] : QuasiFinite R (S ⧸ I)

theorem Algebra.QuasiFinite.of_isLocalization {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (M : Submonoid S) [IsLocalization M T] [QuasiFinite R S] : QuasiFinite R T

instance Algebra.QuasiFinite.instLocalization {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (M : Submonoid S) [QuasiFinite R S] : QuasiFinite R (Localization M)

@[instance 100]

instance Algebra.QuasiFinite.instOfIsFractionRing {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsFractionRing R S] : QuasiFinite R S

instance Algebra.QuasiFinite.instResidueField {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Ideal S) [P.IsPrime] [QuasiFinite R S] : QuasiFinite R P.ResidueField

theorem Algebra.QuasiFinite.of_restrictScalars (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [QuasiFinite R T] : QuasiFinite S T

theorem Algebra.QuasiFinite.discreteTopology_primeSpectrum (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [DiscreteTopology (PrimeSpectrum R)] [QuasiFinite R S] : DiscreteTopology (PrimeSpectrum S)

theorem Algebra.QuasiFinite.finite_primeSpectrum (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [Finite (PrimeSpectrum R)] [QuasiFinite R S] : Finite (PrimeSpectrum S)

theorem Algebra.QuasiFinite.of_forall_exists_mul_mem_range {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [QuasiFinite R S] (f : S →ₐ[R] T) (H : ∀ (x : T), ∃ (s : S), IsUnit (f s) ∧ x * f s ∈ f.range) : QuasiFinite R T

theorem Algebra.QuasiFinite.eq_of_le_of_under_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [QuasiFinite R S] (P Q : Ideal S) [P.IsPrime] [Q.IsPrime] (h₁ : P ≤ Q) (h₂ : Ideal.under R P = Ideal.under R Q) : P = Q

instance Algebra.QuasiFinite.instFiniteResidueField {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [QuasiFinite R S] (P : Ideal R) [P.IsPrime] (Q : Ideal S) [Q.IsPrime] [Q.LiesOver P] : Module.Finite P.ResidueField Q.ResidueField

theorem Algebra.QuasiFinite.iff_finite_comap_preimage_singleton {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FiniteType R S] : QuasiFinite R S ↔ ∀ (x : PrimeSpectrum R), (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {x}).Finite

theorem Algebra.QuasiFinite.iff_finite_primesOver {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FiniteType R S] : QuasiFinite R S ↔ ∀ (I : Ideal R), I.IsPrime → (I.primesOver S).Finite

theorem Algebra.QuasiFinite.of_isIntegral_of_finiteType {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.IsIntegral R S] [FiniteType R T] (s : S) [IsLocalization.Away s T] : QuasiFinite R T

If T is both a finite type R-algebra, and the localization of an integral R-algebra (away from an element), then T is quasi-finite over R

@[reducible, inline]

abbrev Algebra.QuasiFiniteAt (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal S) [p.IsPrime] : Prop

If S is an R-algebra and p a prime of S, we say that S is R-quasi-finite at p if Sₚ is R-quasi-finite. In the case where S is (essentially) of finite type over R, this is equivalent to the usual definition that p is isolated in its fiber. See Ideal.exists_notMem_forall_mem_of_ne_of_liesOver.

Equations

• Algebra.QuasiFiniteAt R p = Algebra.QuasiFinite R (Localization.AtPrime p)

theorem Algebra.QuasiFiniteAt.baseChange {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal S) [p.IsPrime] [QuasiFiniteAt R p] {A : Type u_4} [CommRing A] [Algebra R A] (q : Ideal (TensorProduct R A S)) [q.IsPrime] (hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q) : QuasiFiniteAt A q

theorem Algebra.QuasiFiniteAt.of_surjectiveOnStalks {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (p : Ideal S) [p.IsPrime] [QuasiFiniteAt R p] (f : S →ₐ[R] T) (hf : f.SurjectiveOnStalks) (q : Ideal T) [q.IsPrime] (hq : p = Ideal.comap f.toRingHom q) : QuasiFiniteAt R q

theorem Algebra.QuasiFiniteAt.of_surjectiveOnStalks_of_liesOver {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (p : Ideal S) [p.IsPrime] [QuasiFiniteAt R p] (hf : (algebraMap S T).SurjectiveOnStalks) (q : Ideal T) [q.IsPrime] [q.LiesOver p] : QuasiFiniteAt R q

instance Algebra.QuasiFiniteAt.comap_algEquiv {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (p : Ideal S) [p.IsPrime] [QuasiFiniteAt R p] (f : T ≃ₐ[R] S) : QuasiFiniteAt R (Ideal.comap f.toRingEquiv.toRingHom p)

theorem Algebra.QuasiFiniteAt.of_le {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P Q : Ideal S} [P.IsPrime] [Q.IsPrime] (h₁ : P ≤ Q) [QuasiFiniteAt R Q] : QuasiFiniteAt R P

theorem Algebra.QuasiFiniteAt.eq_of_le_of_under_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P Q : Ideal S} [P.IsPrime] [Q.IsPrime] (h₁ : P ≤ Q) (h₂ : Ideal.under R P = Ideal.under R Q) [QuasiFiniteAt R Q] : P = Q

instance Algebra.instFiniteResidueFieldOfQuasiFiniteAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p] [QuasiFiniteAt R P] : Module.Finite p.ResidueField P.ResidueField

theorem Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal S) [p.IsPrime] [IsArtinianRing R] [EssFiniteType R S] [QuasiFiniteAt R p] : ∃ f ∉ p, ↑(PrimeSpectrum.basicOpen f) = {{ asIdeal := p, isPrime := inst✝ }}

theorem Algebra.QuasiFiniteAt.isClopen_singleton {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum S) [IsArtinianRing R] [FiniteType R S] [QuasiFiniteAt R p.asIdeal] : IsClopen {p}

If R is an artinian ring, and S is a finite type R-algebra R-quasi-finite at p, then {p} is clopen in Spec S.

theorem Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] [Algebra.EssFiniteType R S] [Algebra.QuasiFiniteAt R q] : ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'

theorem Polynomial.not_quasiFiniteAt {R : Type u_1} [CommRing R] (P : Ideal (Polynomial R)) [P.IsPrime] : ¬Algebra.QuasiFiniteAt R P

R[X] is not quasi-finite over R at any prime.

theorem Polynomial.map_under_lt_comap_of_quasiFiniteAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (f : Polynomial R →ₐ[R] S) (P : Ideal S) [P.IsPrime] [Algebra.QuasiFiniteAt R P] : Ideal.map C (Ideal.under R P) < Ideal.comap (↑f) P

theorem Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (f : Polynomial R →ₐ[R] S) (hf : Function.Surjective ⇑f) (P : Ideal S) [P.IsPrime] [Algebra.QuasiFiniteAt R P] : ¬RingHom.ker f ≤ Ideal.map C (Ideal.under R P)

If P is a prime of R[X]/I that is quasi finite over R, then I is not contained in (P ∩ R)[X].

For usability, we replace I by the kernel of a surjective map R[X] →ₐ[R] S.