Theorems · Definition · commutative algebra

Algebra.WeaklyQuasiFiniteAt

(R : Type u_1) →
  {S : Type u_2} → [inst : CommRing R] → [inst_1 : 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.

Defined in

Mathlib.RingTheory.QuasiFinite.Weakly

Cited by

18 results in Mathlib

Foundations

Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraIdeal.IsPrime