ModuleGenericKernelPointNormalGeneration.lean
Nyll.EtaleFundamentalGroups.Inertia.GenericKernelPointNormalGeneration
4 declarations indexed from sourceView source ↗ Module documentation
The generic kernel generated by inertia at actual normalization points
The generators here are original automorphisms fixing an actual point of the normalization in the separable closure and inducing its identity residue action. Their union equals the original affine ideal-inertia generator set.
One direction uses the actual residue point of a prime and normalization-chart equivariance. For the converse, the canonical residue point at a scheme point lifts through an affine normalization chart. Cancellation of this monomorphism and the affine spectrum adjunction give membership in the original inertia of the prime kernel. No chart-action or point-inertia identification is assumed.
Declarations
EtaleFundamentalGroups.Inertia.fieldSpecQuasiCompact
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
EtaleFundamentalGroups.Inertia.pointNormalizationInertiaGenerators
DocumentationOriginal inertia elements indexed by the actual points of the normalization in the same separable closure of the function field.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
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.Inertia.affineNormalizationInertiaGenerators_eq_pointNormalizationInertiaGenerators
DocumentationThe affine and actual scheme-point inertia generators are the same elements of the original absolute Galois group, also for the infinite separable closure.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
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.Inertia.genericAbsoluteGaloisHom_ker_eq_normalClosure_pointNormalizationInertia
DocumentationThe original generic-point kernel is the closed normal subgroup generated by inertia at the actual points of the normalization in the separable closure, with the literal point and residue-field action.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
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