Theorems · Inductive type · commutative algebra
Algebra.QuasiFinite
(R : Type u_1) → (S : Type u_2) → [inst : CommRing R] → [inst_1 : 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](https://stacks.math.columbia.edu/tag/00PL),
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 algebras.
- Defined in
- Mathlib.RingTheory.QuasiFinite.Basic
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by32
Results whose statement or proof uses this declaration.
- Algebra.QuasiFiniteAtproof · cited by 29
- RingHom.QuasiFiniteproof · cited by 21
- Algebra.QuasiFinite.transstatement and proof · cited by 8
- Algebra.QuasiFinite.of_surjective_algHomstatement and proof · cited by 7
- Module.Finite.of_quasiFinitestatement and proof · cited by 7
- RingHom.quasiFinite_algebraMapstatement and proof · cited by 7
- Algebra.QuasiFinite.iff_finite_comap_preimage_singletonstatement and proof · cited by 4
- Algebra.QuasiFinite.of_isLocalizationstatement and proof · cited by 4
- Algebra.QuasiFinite.finite_comap_preimage_singletonstatement and proof · cited by 3
- Algebra.QuasiFinite.of_forall_exists_mul_mem_rangestatement and proof · cited by 3
- Algebra.QuasiFinite.of_restrictScalarsstatement and proof · cited by 3
- Algebra.QuasiFinite.isDiscrete_comap_preimage_singletonstatement and proof · cited by 2