ModuleEtaleReduced.lean
Nyll.SchemeTheory.Morphisms.EtaleReduced
2 declarations indexed from sourceView source ↗ Module documentation
Reducedness of etale morphisms
An etale algebra over a field is reduced, because it is essentially of finite type and formally unramified. Applying this on an affine cover after an arbitrary field-valued base change shows that every etale morphism is geometrically reduced. Combined with Mathlib's flat descent theorem, this also gives reducedness of an etale source over a locally Noetherian reduced base.
Mathlib defines Etale, GeometricallyReduced, and the relevant reducedness descent theorem, but currently does not provide the implication proved here.
Imports3
- Mathlib.AlgebraicGeometry.Geometrically.Reduced
- Mathlib.AlgebraicGeometry.Morphisms.Etale
- Mathlib.RingTheory.Etale.Field
Imported by3
Declarations
AlgebraicGeometry.Etale.geometricallyReduced
DocumentationAn etale morphism of schemes is geometrically reduced.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
universe u
AlgebraicGeometry.Etale.isReduced_of_isLocallyNoetherian
DocumentationThe source of an etale morphism over a locally Noetherian reduced scheme is reduced.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
universe u