Structures · Algebra
Algebra.Etale
An R-algebra A is étale if it is formally étale and of finite presentation.
- Defined in
- Mathlib.RingTheory.Etale.Basic
- Shape
- 2 explicit arguments · adds formallyEtale, finitePresentation
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every Algebra.Etale is also a
Concrete types that are instances1
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by24
- CommAlgCat.FiniteEtale.of
- CommAlgCat.FiniteEtale.ofHom
- Algebra.Etale.of_etale_tensorProduct_of_faithfullyFlat
- Algebra.Etale.of_equiv
- IsLocalRing.finrank_eq_finrank_residueField
- HasStandardEtaleSurjectionOn.isStandardEtale
- Algebra.IsStandardEtale.of_surjective
- IsLocalRing.minpoly_map_residue
- Algebra.Etale.comp
- Algebra.Etale.baseChange
- Algebra.Etale.formallyEtale
- Algebra.Etale.instSmooth
- Algebra.FormallyEtale.instEtaleForallOfFinite
- Algebra.Etale.finitePresentation
- Algebra.Etale.instAway
- CommAlgCat.FiniteEtale.of_obj
- Algebra.Etale.exists_subalgebra_fg
- IsLocalRing.isUnit_aeval_derivative_minpoly_of_adjoin_eq_top
- Algebra.Etale.instUnramified
- CommAlgCat.FiniteEtale.of.congr_simp
- CommAlgCat.FiniteEtale.ofHom_hom
- Algebra.Etale.of_restrictScalars
- Algebra.IsFiniteSplit.exists_tensorProduct_of_etale
- Algebra.WeaklyEtale.instOfEtale