Structures · Algebra
Algebra.FiniteType
An algebra over a commutative semiring is of FiniteType if it is finitely generated
over the base ring as algebra.
- Defined in
- Mathlib.RingTheory.FiniteType
- Shape
- 2 explicit arguments · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Int
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by66
- Algebra.FiniteType.out
- Algebra.FiniteType.of_surjective
- Algebra.FiniteType.isNoetherianRing
- isJacobsonRing_of_finiteType
- Algebra.IsIntegral.finite
- finite_of_finite_type_of_isJacobsonRing
- Algebra.QuasiFinite.iff_finite_comap_preimage_singleton
- Algebra.ZariskisMainProperty.of_finiteType
- Algebra.FiniteType.of_finiteType_tensorProduct_of_faithfullyFlat
- Algebra.FiniteType.of_restrictScalars_finiteType
- Algebra.ZariskisMainProperty.of_finiteType_of_weaklyQuasiFiniteAt
- Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective
- Module.finite_iff_isArtinianRing
- Algebra.QuasiFiniteAt.isClopen_singleton
- Algebra.FinitePresentation.of_restrict_scalars_finitePresentation
- GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero
- Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq
- GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous
- exists_integral_inj_algHom_of_fg
- Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂
- Algebra.ZariskisMainProperty.quasiFiniteAt
- finite_of_algHom_finiteType_of_isJacobsonRing
- trdeg_lt_aleph0_of_finiteType
- Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux
- Algebra.QuasiFiniteAt.of_isOpen_singleton
- Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn
- Algebra.FiniteType.exists_fgAlgCatSkeleton
- AddMonoidAlgebra.exists_finset_adjoin_eq_top
- Algebra.QuasiFinite.of_isIntegral_of_finiteType
- Algebra.exists_unramified_of_isUnramifiedAt
- Module.finite_of_isSemisimpleRing
- Module.finite_of_isArtinianRing
- Algebra.QuasiFiniteAt.of_isOpen_singleton_fiber
- Algebra.quasiFiniteAt_iff_isOpen_singleton_fiber
- Algebra.QuasiFiniteAt.of_quasiFiniteAt_residueField
- Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐ
- Algebra.QuasiFiniteAt.of_weaklyQuasiFiniteAt
- Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver
- Ideal.Fiber.lift_residueField_surjective
- AlgebraicGeometry.Proj.instIsProperToSpecZeroOfFiniteTypeSubtypeMemOfNatNat
- Algebra.EssFiniteType.of_finiteType
- AlgebraicGeometry.Proj.valuativeCriterion_existence
- AdjoinRoot.finiteType
- Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective
- Algebra.FiniteType.instPolynomial
- Algebra.FiniteType.instMvPolynomialOfFinite
- Module.finite_iff_krullDimLE_zero
- AlgebraicGeometry.Proj.instQuasiCompactToSpecZeroOfFiniteTypeSubtypeMemOfNatNat
- Algebra.FiniteType.prod
- Algebra.QuasiFinite.iff_finite_primesOver
Ancestors0
No ancestors.