Structures · Algebra
Algebra.Smooth
An R algebra A is smooth if it is formally smooth and of finite presentation.
- Defined in
- Mathlib.RingTheory.Smooth.Basic
- Shape
- 2 explicit arguments · adds formallySmooth, finitePresentation
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every Algebra.Smooth is also a
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 by14
- Algebra.Smooth.of_smooth_tensorProduct_of_faithfullyFlat
- Algebra.Smooth.exists_subalgebra_fg
- Algebra.Smooth.comp
- Algebra.Smooth.exists_span_eq_top_isStandardSmooth
- Algebra.Smooth.formallySmooth
- Algebra.Smooth.exists_subalgebra_finiteType
- TensorProduct.toIntegralClosure_bijective_of_smooth
- Algebra.Smooth.baseChange
- Algebra.Smooth.flat_of_isNoetherianRing
- Algebra.Smooth.finitePresentation
- Algebra.Smooth.of_equiv
- Algebra.Smooth.exists_finiteType
- Algebra.Smooth.flat
- Algebra.smoothLocus_eq_univ