ModuleAffineInertiaCriterion.lean
Nyll.EtaleFundamentalGroups.Normalization.AffineInertiaCriterion
4 declarations indexed from sourceView source ↗ Module documentation
Original affine inertia criterion for the actual global normalization
The actual genericNormalizationChart pullback identifies etaleness of the global normalization with etaleness of its literal integral-closure charts. For a finite Galois field extension, the proved affine inertia criterion therefore identifies global etaleness with trivial original ideal inertia at every prime on every nonempty affine chart. No scheme/affine comparison is assumed and no Noetherian hypothesis is added. The final theorem uses proved chart equivariance and residue-field naturality to identify this with the original global fixed-point and trivial-residue-action condition.
Declarations
EtaleFundamentalGroups.fieldSpecQuasiCompact
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups
universe u
EtaleFundamentalGroups.etale_genericNormalization_iff_affineIntegralClosure_etale
DocumentationEtaleness of the actual global normalization is equivalent to etaleness of its original integral closures on all nonempty affine charts.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
{K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
QuasiCompact f where
isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
EtaleFundamentalGroups.etale_genericNormalization_iff_all_affine_inertia_eq_bot
DocumentationFor the original finite Galois function-field extension of an integral normal scheme, global etaleness of the literal normalization is equivalent to trivial original inertia at every prime in every nonempty affine chart.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
{K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
QuasiCompact f where
isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
EtaleFundamentalGroups.etale_genericNormalization_iff_trivial_point_residue_inertia
DocumentationFor the original finite Galois function-field extension, the literal global normalization is etale exactly when every original automorphism fixing a normalization point and acting trivially on its residue field is identity. This is the equivalence of (3) and (9) in Stacks Tag 0BTF.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
{K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
QuasiCompact f where
isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact