Structures · Algebra
Algebra.EssFiniteType
An R-algebra is essentially of finite type if
it is the localization of an algebra of finite type.
See essFiniteType_iff_exists_subalgebra.
For field extensions, this is equivalent to being finitely generated as a field.
See IntermediateField.fg_top_iff.
- Defined in
- Mathlib.RingTheory.EssentialFiniteness
- Shape
- 2 explicit arguments · adds cond
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Ideal.ResidueField
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by84
- Algebra.EssFiniteType.of_comp
- Algebra.EssFiniteType.comp
- Algebra.FormallyUnramified.finite_of_free
- Algebra.FormallyUnramified.elem
- Algebra.FormallyUnramified.isReduced_of_field
- Algebra.EssFiniteType.subalgebra
- Algebra.EssFiniteType.finset
- Algebra.FormallyUnramified.map_maximalIdeal
- Algebra.EssFiniteType.submonoid
- Ideal.ramificationIdx_eq_one_iff
- Algebra.FormallyUnramified.sec
- Ideal.ramificationIdx_eq_one
- Algebra.FormallyUnramified.comp_sec
- Algebra.FormallyEtale.equivPiOfIsSepClosed
- IntermediateField.fg_top
- Algebra.FormallyUnramified.iff_map_maximalIdeal_eq
- Algebra.isOpen_unramifiedLocus
- Algebra.EssFiniteType.isNoetherianRing
- Algebra.FormallyUnramified.isSeparable
- Algebra.exists_formallyUnramified_of_isUnramifiedAt
- Algebra.isUnramifiedAt_iff_map_eq
- KaehlerDifferential.ideal_fg
- Algebra.smoothLocus_eq_compl_support_inter
- Algebra.FormallyUnramified.iff_isSeparable
- Algebra.FormallyUnramified.lmul_elem
- Algebra.EssFiniteType.algHom_ext
- Algebra.EssFiniteType.of_surjective
- Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton
- Algebra.FormallyUnramified.iff_exists_tensorProduct
- Algebra.FormallyEtale.iff_isSeparable
- Algebra.FormallyEtale.of_isSeparable_aux
- Algebra.EssFiniteType.comp_iff
- Algebra.FormallyUnramified.range_eq_top_of_isPurelyInseparable
- Ideal.ramificationIdx'_eq_one_iff
- IsUnramifiedAt.of_liesOver_of_ne_bot
- Algebra.FormallyEtale.iff_exists_algEquiv_prod
- Algebra.FormallyEtale.of_formallyUnramified_of_field
- IntermediateField.exists_finset_maximalFor_isTranscendenceBasis_separableClosure
- Algebra.finite_of_essFiniteType_of_isAlgebraic
- exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType
- Ideal.ramificationIdx_eq_one_of_isUnramifiedAt
- Algebra.FormallyUnramified.one_tmul_sub_tmul_one_mul_elem
- Algebra.IsUnramifiedIn.ramificationIdx_eq_one
- Algebra.FormallyUnramified.one_tmul_mul_elem
- Algebra.FormallyUnramified.exists_algEquiv_prod
- Algebra.FormallyUnramified.of_map_maximalIdeal
- Algebra.FormallyUnramified.isRadical_map_isMaximal
- Algebra.FormallyUnramified.isField_quotient_map_maximalIdeal
- Algebra.EssFiniteType.adjoin_mem_finset
- Algebra.FormallyUnramified.bijective_of_isAlgClosed_of_isLocalRing
Ancestors0
No ancestors.