Module

AffineGeometricPoint.lean

Nyll.EtaleFundamentalGroups.Inertia.AffineGeometricPoint

2 declarations indexed from sourceView source ↗

Module documentation

Ideal inertia and affine geometric-point stabilizers

Let a group G act on a commutative ring B. A geometric point Spec Ω ⟶ Spec B represented by φ : B →+* Ω is fixed by an element of G exactly when that element acts trivially modulo ker φ. Thus the scheme-theoretic geometric-point stabilizer is ideal inertia, rather than the decomposition group that merely preserves the underlying prime.

For the geometric point obtained by embedding the residue field of a prime P into its algebraic closure, the kernel is P, so the comparison gives the usual ideal-inertia subgroup without any additional compatibility input. The statements apply in particular to the affine charts of a normalization.

This is the affine geometric-point/ideal-inertia part of the divisorial comparison. It does not identify either group with the image of the fundamental group of the fraction field of a strict henselization; that identification additionally requires the construction and local properties of the strict henselization.

Imports5

Mathlib.Algebra.Ring.Action.Basic
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Imported by4

theorem

mem_idealInertia_iff_fixes_affineGeometricPoint

L44 ↗

EtaleFundamentalGroups.Inertia.mem_idealInertia_iff_fixes_affineGeometricPoint

Documentation

An element fixes an affine geometric point precisely when its action on the coordinate ring is trivial modulo the point's prime kernel.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem mem_idealInertia_iff_fixes_affineGeometricPoint
    (G : Type v) [Group G]
    {B Ω : Type u} [CommRing B] [Field Ω] [MulSemiringAction G B]
    (φ : B →+* Ω) (σ : G) :
    σ ∈ (RingHom.ker φ).inertia G ↔
      Spec.map (CommRingCat.ofHom φ) ≫
          Spec.map (CommRingCat.ofHom (MulSemiringAction.toRingHom G B σ)) =
        Spec.map (CommRingCat.ofHom φ)

theorem

mem_idealInertia_iff_fixes_residueGeometricPoint

L68 ↗

EtaleFundamentalGroups.Inertia.mem_idealInertia_iff_fixes_residueGeometricPoint