ModuleSmoothReduced.lean
Nyll.SchemeTheory.RingTheory.SmoothReduced
3 declarations indexed from sourceView source ↗ Module documentation
Reducedness of smooth algebras over fields
The etale generic-fiber argument and local standard-etale presentations prove reducedness directly. This is the reusable ring part of the pinned FLT proof previously maintained in AlgebraicCurves.
Imports4
- Mathlib.RingTheory.Unramified.LocalStructure
- Mathlib.RingTheory.Unramified.Field
- Mathlib.RingTheory.Localization.FractionRing
- Mathlib.RingTheory.Flat.Basic
Imported by3
Declarations
Algebra.Etale.isReduced_of_field
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct
namespace Algebra.Etale
Algebra.Etale.isReduced_of_isDomain
DocumentationAn etale algebra over a domain is reduced, by flat injection into its generic fiber.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct
Algebra.Smooth.isReduced_of_field
DocumentationA smooth algebra over a field is reduced, by its standard-etale local presentations.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct
namespace Algebra.Smooth