ModuleFiniteEtaleGeometricallyReduced.lean
Nyll.SchemeTheory.Morphisms.FiniteEtaleGeometricallyReduced
2 declarations indexed from sourceView source ↗ Module documentation
Geometric reducedness under finite etale covers
A finite etale morphism has reduced fibres after every field extension. A finite etale cover of a geometrically reduced family of finite type is therefore geometrically reduced over the original base. No Noetherian condition is imposed on that base: the intermediate geometric fibre is locally Noetherian because it is of finite type over its field.
Imports6
- Mathlib.AlgebraicGeometry.Geometrically.Reduced
- Mathlib.AlgebraicGeometry.Morphisms.Etale
- Mathlib.AlgebraicGeometry.Morphisms.Finite
- Mathlib.AlgebraicGeometry.Noetherian
- Mathlib.RingTheory.RingHom.Etale
- Mathlib.RingTheory.Unramified.Field
Imported by3
Declarations
AlgebraicGeometry.geometricallyReduced_of_isFinite_of_etale
DocumentationFinite etale morphisms are geometrically reduced.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
AlgebraicGeometry.GeometricallyReduced.comp_of_isFinite_of_etale
DocumentationA finite etale cover preserves geometric reducedness of a family locally of finite type over its original base.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u