Structures · Algebra
Algebra.FinitePresentation
An algebra over a commutative semiring is Algebra.FinitePresentation if it is the quotient of
a polynomial ring in n variables by a finitely generated ideal.
- Defined in
- Mathlib.RingTheory.FinitePresentation
- 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 instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by50
- Algebra.FinitePresentation.equiv
- Algebra.FinitePresentation.trans
- Algebra.FinitePresentation.ker_fG_of_surjective
- Algebra.FinitePresentation.out
- Algebra.FinitePresentation.quotient
- Algebra.basicOpen_subset_smoothLocus_iff
- Algebra.smoothLocus_eq_univ_iff
- Algebra.FinitePresentation.of_surjective
- Algebra.Smooth.of_formallySmooth_fiber
- Module.FinitePresentation.of_finite_of_finitePresentation
- Algebra.Etale.of_formallyUnramified_of_flat
- Algebra.IsStandardSmooth.of_basis_kaehlerDifferential
- PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation
- Algebra.Generators.exists_presentation_of_basis_cotangent
- Algebra.IsSmoothAt.exists_notMem_smooth
- Algebra.FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlat
- Algebra.FinitePresentation.of_restrict_scalars_finitePresentation
- Algebra.isOpen_smoothLocus
- Algebra.IsSmoothAt.exists_notMem_isStandardSmooth
- Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential
- Algebra.FinitePresentation.of_span_eq_top_target_aux
- Algebra.Presentation.ofFinitePresentation
- Algebra.Presentation.ofFinitePresentationRels
- Algebra.IsSmoothAt.of_formallySmooth_fiber
- Algebra.FinitePresentation.of_isLocalizationAway
- Algebra.IsEtaleAt.exists_isStandardEtale
- Algebra.exists_etale_of_isEtaleAt
- Algebra.basicOpen_subset_etaleLocus_iff_etale
- Algebra.Generators.fg_ker_of_finitePresentation
- Algebra.FormallySmooth.of_formallySmooth_residueField_tensor
- Algebra.FinitePresentation.ker_fg_of_mvPolynomial
- Algebra.Presentation.ofFinitePresentationVars
- Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial
- Algebra.isOpen_etaleLocus
- instFinitePresentationAway
- Algebra.FinitePresentation.baseChange
- Algebra.IsEtaleAt.of_isUnramifiedAt_of_flat
- Algebra.Presentation.exists_presentation_fin
- Algebra.FiniteType.of_finitePresentation
- Algebra.FinitePresentation.polynomial
- Algebra.FinitePresentation.mvPolynomial_of_finitePresentation
- Algebra.FinitePresentation.pi
- Algebra.basicOpen_subset_smoothLocus_iff_smooth
- Algebra.Generators.exists_presentation_of_free_cotangent
- Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway
- Algebra.instFinitePresentationKaehlerDifferentialOfFinitePresentation
- Algebra.instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential
- Algebra.etaleLocus_eq_univ_iff_etale
- AdjoinRoot.finitePresentation
- Algebra.FinitePresentation.mvPolynomial
Ancestors0
No ancestors.