Module

StrictHenselianKernel.lean

Nyll.EtaleFundamentalGroups.Inertia.StrictHenselianKernel

2 declarations indexed from sourceView source ↗

Module documentation

Strict-Henselian generic inertia lies in the boundary kernel

The actual local generic morphism factors through the spectrum of its geometric etale stalk after composition with the open inclusion. The latter spectrum has trivial fundamental group. Comparing the two factorizations therefore kills its local generic inertia in the ambient scheme.

Imports4

Imported by2

theorem

image_le_ker_of_trivial_factorization

L30 ↗

EtaleFundamentalGroups.Inertia.image_le_ker_of_trivial_factorization

Source context 4 commands

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

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

Lean source · statement

theorem image_le_ker_of_trivial_factorization
    {T U S X : Scheme.{u}}
    (j : T ⟶ U) (i : U ⟶ X) (q : T ⟶ S) (b : S ⟶ X)
    (h : j ≫ i = q ≫ b)
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ T) [Subsingleton π₁ᵉᵗ(point ≫ q)] :
    fundamentalGroupImageOfMorphism j point ≤
      (fundamentalGroupHom i (point ≫ j)).toMonoidHom.ker

theorem

geometricStalkFractionField_image_le_boundaryKernel

L55 ↗

EtaleFundamentalGroups.Inertia.geometricStalkFractionField_image_le_boundaryKernel

Documentation

The fundamental-group image of the fraction field of the actual geometric etale stalk over a normal local domain is killed by the Cartier-complement inclusion.