All.lean
Nyll.SchemeTheory.Normalization.All
0 declarations indexed from sourceView source ↗
Module documentation
Normalization of affine curves
This facade collects normalization finiteness, conductor-quotient, and prime-separation results.
Imports30
- Nyll.SchemeTheory.Normalization.SubalgebraPreimage
- Nyll.SchemeTheory.Normalization.Affine
- Nyll.SchemeTheory.Normalization.CompositumEmbedding
- Nyll.SchemeTheory.Normalization.ConductorQuotient
- Nyll.SchemeTheory.Normalization.FiniteEtaleOpen
- Nyll.SchemeTheory.Normalization.FiniteSeparable
- Nyll.SchemeTheory.Normalization.GenericFiber.All
- Nyll.SchemeTheory.Normalization.HenselianIntegralSection
- Nyll.SchemeTheory.Normalization.HenselianSectionFactor
- Nyll.SchemeTheory.Normalization.IntegralClosure.All
- Nyll.SchemeTheory.Normalization.IntegralOpen
- Nyll.SchemeTheory.Normalization.Localization.All
- Nyll.SchemeTheory.Normalization.Normal
- Nyll.SchemeTheory.Normalization.PrimeSeparation
- Nyll.SchemeTheory.Normalization.Products.All
- Nyll.SchemeTheory.Normalization.QuotientFiniteFactor
- Nyll.SchemeTheory.Normalization.AffineFiniteEtale
- Nyll.SchemeTheory.Normalization.NativeNormalizationPrime
- Nyll.SchemeTheory.Normalization.IntegralClosureAutomorphisms
- Nyll.SchemeTheory.Normalization.NormalizationAutomorphismSurjectivity
- Nyll.SchemeTheory.Normalization.NormalizationGaloisSurjectivity
- Nyll.SchemeTheory.Normalization.IntegralClosureAutomorphismRestriction
- Nyll.SchemeTheory.Normalization.NormalizationAutomorphismGroupMap
- Nyll.SchemeTheory.Normalization.ScalarRestrictionGroupMap
- Nyll.SchemeTheory.Normalization.NativeAutomorphismRingMaps
- Nyll.SchemeTheory.Normalization.AmbientNormalizationGroupMap
- Nyll.SchemeTheory.Normalization.NativeNormalizationRingMap
- Nyll.SchemeTheory.Normalization.SubalgebraNormalizationTower
- Nyll.SchemeTheory.Normalization.SubalgebraNormalizationTowerRamification
- Nyll.SchemeTheory.Normalization.FiniteNormalSource
Imported by1
This module has no indexed declarations. Its imports and full source are available here.