Documentation

Mathlib.RingTheory.QuasiFinite.Weakly

Weakly Quasi-finite primes #

The definition Algebra.QuasiFiniteAt is equivalent to the usual definition "isolated in fibers" mathematically for algebras of finite type, but this requires Zariski's main theorem to prove. Hence we introduce a weaker notion of being Algebra.WeaklyQuasiFiniteAt that we shall state Zariski's main theorem in terms of, and deduce from this that Algebra.WeaklyQuasiFiniteAt is equivalent to Algebra.QuasiFiniteAt under all relevant scenarios.

This class should only be used in stating (and proving) Zariski's main theorem and should not be used elsewhere, and all public API shall have a Algebra.QuasiFiniteAt version.

Implementation details #

The definition of Algebra.QuasiFiniteAt R q as is says that the whole S_q is quasi-finite, which requires not only q to be quasi-finite, but also all primes below it (i.e. all generic points that specialize to it) to also be quasi-finite. This is fine mathematically because the set of quasi-finite primes is open (according to Zariski's Main theorem). But this requires the statement of Zariski's main to be stated with an a priori weaker notion of quasi-finite. Hence we introduce Algebra.WeaklyQuasiFiniteAt where we mod out all the primes that lie in a different fiber.

source
@[reducible, inline]
abbrev Algebra.WeaklyQuasiFiniteAt (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (q : Ideal S) [q.IsPrime] :
Prop

(Implementation) An a priori weaker notion of being quasi-finite at a prime, which turns out to be equivalent to Algebra.QuasiFiniteAt (for finite type algebras) due to Zariski's main theorem.

This class should not be used outside of this context, and Algebra.QuasiFiniteAt should be used instead. See Algebra.QuasiFiniteAt.of_weaklyQuasiFiniteAt.

Equations
Instances For
    source
    theorem Algebra.weaklyQuasiFiniteAt_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (q : Ideal S) [q.IsPrime] :
    WeaklyQuasiFiniteAt R q ↔ QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))
    source
    @[instance 100]
    instance Algebra.WeaklyQuasiFiniteAt.instOfQuasiFiniteAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (q : Ideal S) [q.IsPrime] [QuasiFiniteAt R q] :
    WeaklyQuasiFiniteAt R q
    source
    theorem Algebra.WeaklyQuasiFiniteAt.of_algHom_localization {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] (p : Ideal S) [p.IsPrime] [WeaklyQuasiFiniteAt R p] (q : Ideal T) [q.IsPrime] (f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q) (hf : Function.Surjective ⇑f) :
    WeaklyQuasiFiniteAt R q

    Use Algebra.QuasiFinite.of_surjective_algHom instead for Algebra.QuasiFiniteAt R p.

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

    Use Algebra.QuasiFiniteAt.of_surjectiveOnStalks instead for Algebra.QuasiFiniteAt R p.

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

    By infer_instance for Algebra.QuasiFiniteAt R p.

    source
    theorem Algebra.WeaklyQuasiFiniteAt.finite_residueField {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [q.IsPrime] [p.IsPrime] [q.LiesOver p] [WeaklyQuasiFiniteAt R q] :
    Module.Finite p.ResidueField q.ResidueField

    By infer_instance for Algebra.QuasiFiniteAt R p.

    source
    theorem Algebra.WeaklyQuasiFiniteAt.finite_locoalization {S : Type u_2} [CommRing S] (q : Ideal S) [q.IsPrime] {K : Type u_4} [Field K] [Algebra K S] [WeaklyQuasiFiniteAt K q] :
    Module.Finite K (Localization.AtPrime q)

    By infer_instance for Algebra.QuasiFiniteAt R p.

    source
    theorem Algebra.WeaklyQuasiFiniteAt.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) [WeaklyQuasiFiniteAt R Q] :
    P = Q

    Use Algebra.QuasiFiniteAt.eq_of_le_of_under_eq instead for Algebra.QuasiFiniteAt R p.

    source
    theorem Algebra.WeaklyQuasiFiniteAt.baseChange {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal S) [p.IsPrime] [WeaklyQuasiFiniteAt 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) :
    WeaklyQuasiFiniteAt A q

    Use Algebra.QuasiFiniteAt.baseChange instead for Algebra.QuasiFiniteAt R p.

    source
    theorem Algebra.WeaklyQuasiFiniteAt.of_restrictScalars (R : Type u_1) (S : Type u_2) {T : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal T) [q.IsPrime] [WeaklyQuasiFiniteAt R q] :
    WeaklyQuasiFiniteAt S q

    Use Algebra.QuasiFinite.of_restrictScalars instead for Algebra.QuasiFiniteAt R p.