Structures · Algebra
Algebra.QuasiFinite
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
- Shape
- 2 explicit arguments · adds finite_fiber
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by23
- Algebra.QuasiFinite.trans
- Algebra.QuasiFinite.of_surjective_algHom
- Module.Finite.of_quasiFinite
- Algebra.QuasiFinite.of_isLocalization
- Algebra.QuasiFinite.of_forall_exists_mul_mem_range
- Algebra.QuasiFinite.finite_comap_preimage_singleton
- Algebra.QuasiFinite.of_restrictScalars
- Algebra.QuasiFinite.isDiscrete_comap_preimage_singleton
- Algebra.QuasiFinite.finite_primesOver
- Algebra.QuasiFinite.isDiscrete_comap_preimage
- Algebra.QuasiFinite.eq_of_le_of_under_eq
- Algebra.QuasiFinite.finite_comap_preimage
- Ideal.sum_ramification_inertia_eq_finrank_fiber
- Algebra.QuasiFinite.instFiniteResidueFieldAtPrimeFiber
- Algebra.QuasiFinite.instFiniteResidueField
- Algebra.QuasiFinite.instIsArtinianRingFiber
- Algebra.QuasiFinite.instLocalization
- Algebra.QuasiFinite.discreteTopology_primeSpectrum
- Algebra.QuasiFinite.finite_fiber
- Algebra.QuasiFinite.finite_primeSpectrum
- Algebra.QuasiFinite.baseChange
- Algebra.QuasiFinite.instResidueField
- Algebra.QuasiFinite.instQuotientIdeal
Ancestors0
No ancestors.