ModuleNormalizationRemainderDegree.lean
Nyll.SchemeTheory.Etale.NormalizationRemainderDegree
5 declarations indexed from sourceView source ↗ Module documentation
Strict degree decrease for the normalization remainder
A supplied uniform finite bound on the geometric fibers of a separated quasi-compact étale morphism strictly decreases on its actual normalization remainder. Over the dense normalization image the residual fiber omits the normalization-graph point. The neighborhood theorem for finite sets of geometric points extends this strict bound to the entire normalization.
The final theorem supplies the original bound from the existing affine geometric-fiber theorem for maps between spectra. The very same bound is used in the strict inequality; it is not increased. This proves the degree-decrease step in the affine case of Stacks Project, Tag 09Z0. The uniform bound for a general qcqs target, the integral refinement and finite-presentation descent remain separate tasks.
Declarations
AlgebraicGeometry.Scheme.Hom.remainderFiberMap
DocumentationThe actual residual-fiber inclusion, followed by the standard pasting isomorphism to the original geometric fiber.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Hom
variable {U X : Scheme.{u}} (f : U ⟶ X) [QuasiCompact f] [IsSeparated f] [Etale f]
AlgebraicGeometry.Scheme.Hom.remainderFiberMap_isOpenImmersion
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Hom
variable {U X : Scheme.{u}} (f : U ⟶ X) [QuasiCompact f] [IsSeparated f] [Etale f]
AlgebraicGeometry.Scheme.Hom.remainder_degree_lt_over_source
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Hom
variable {U X : Scheme.{u}} (f : U ⟶ X) [QuasiCompact f] [IsSeparated f] [Etale f]
AlgebraicGeometry.Scheme.Hom.normalizationRemainder_degree_lt_of_bound
DocumentationThe normalization remainder has geometric fibers strictly smaller than any actual uniform finite bound for the original étale morphism. The bound premise is the induction parameter; the affine theorem below supplies it without an additional hypothesis.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Hom
variable {U X : Scheme.{u}} (f : U ⟶ X) [QuasiCompact f] [IsSeparated f] [Etale f]
AlgebraicGeometry.Etale.exists_normalizationRemainder_degree_bound_spec
DocumentationFor an actual étale map between spectra, the existing affine bound supplies both a uniform bound for the original fibers and a strictly smaller bound for its normalization remainder. No global-bound premise is added.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Etale