Module

UnramifiedGeometricInertia.lean

Nyll.EtaleFundamentalGroups.Normalization.UnramifiedGeometricInertia

5 declarations indexed from sourceView source ↗

Module documentation

Global geometric-point rigidity for an unramified normalization

The normalization endomorphism is the actual extension of the original field automorphism. If it fixes any field-valued point, unramified point rigidity makes it the identity. The actual generic-fiber square makes the map from Spec L into the normalization a monomorphism, so the original field automorphism itself is the identity.

The final theorem uses canonical residue-point naturality to apply this rigidity directly to the original fixed-point and trivial-residue-action condition. It proves the global unramified-to-trivial-inertia implication in Stacks Project, Tag 0BTF, for the original field automorphism itself. Galoisness is unnecessary for this forward implication.

Imports10

Nyll.EtaleFundamentalGroups.Inertia.NormalizationPointRigidity
Nyll.EtaleFundamentalGroups.Normalization.GenericExtensionFiber
Nyll.SchemeTheory.Morphisms.ResiduePointFixedness
Nyll.SchemeTheory.Normalization.FiniteSeparable
Mathlib.Algebra.Algebra.Equiv
Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Mathlib.AlgebraicGeometry.ResidueField
Mathlib.AlgebraicGeometry.Stalk
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Mathlib.FieldTheory.Finiteness

Imported by4

instance

fieldSpecQuasiCompact

L42 ↗

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

Lean source · full declaration

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

theorem

fieldAlgEquiv_eq_one_of_specMap_eq_id

L47 ↗

EtaleFundamentalGroups.fieldAlgEquiv_eq_one_of_specMap_eq_id

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

Lean source · statement

theorem fieldAlgEquiv_eq_one_of_specMap_eq_id
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    (σ : L ≃ₐ[K] L)
    (h : Spec.map (CommRingCat.ofHom σ.toRingHom) = 𝟙 (Spec (.of L))) : σ = 1

theorem

genericExtensionMorphism_specMap_algEquiv

L60 ↗

EtaleFundamentalGroups.genericExtensionMorphism_specMap_algEquiv

Documentation

An original function-field automorphism preserves the actual generic extension morphism, through its given scalar compatibility.

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

Lean source · statement

theorem genericExtensionMorphism_specMap_algEquiv
    (X : Scheme.{u}) [IsIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L]
    (σ : L ≃ₐ[X.functionField] L) :
    Spec.map (CommRingCat.ofHom σ.toRingHom) ≫ X.genericExtensionMorphism L =
      X.genericExtensionMorphism L

theorem

genericNormalization_automorphism_eq_one_of_fixed_fieldPoint

L79 ↗

EtaleFundamentalGroups.genericNormalization_automorphism_eq_one_of_fixed_fieldPoint

Documentation

A field automorphism fixing an actual field-valued point of the unramified normalization is the identity. Galoisness is unnecessary for this individual-automorphism statement.

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

Lean source · statement

theorem genericNormalization_automorphism_eq_one_of_fixed_fieldPoint
    (X : Scheme.{u}) [IsIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L]
    [FiniteDimensional X.functionField L]
    (hunram : FormallyUnramified (X.genericExtensionMorphism L).fromNormalization ∧
      LocallyOfFiniteType (X.genericExtensionMorphism L).fromNormalization)
    (σ : L ≃ₐ[X.functionField] L) {Ω : Type u} [Field Ω]
    (z : Spec (.of Ω) ⟶ (X.genericExtensionMorphism L).normalization)
    (hz : z ≫ Inertia.normalizationEndomorphism (X.genericExtensionMorphism L)
        (Spec.map (CommRingCat.ofHom σ.toRingHom))
        (genericExtensionMorphism_specMap_algEquiv X L σ) = z) : σ = 1

theorem

genericNormalization_automorphism_eq_one_of_trivial_residue

L118 ↗

EtaleFundamentalGroups.genericNormalization_automorphism_eq_one_of_trivial_residue

Documentation

The original point-and-residue inertia condition on an unramified normalization forces the original field automorphism to be the identity. This proves the forward implication to condition (9) of Tag 0BTF; it also holds for finite extensions which are not Galois.

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

Lean source · statement

theorem genericNormalization_automorphism_eq_one_of_trivial_residue
    (X : Scheme.{u}) [IsIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L]
    [FiniteDimensional X.functionField L]
    (hunram : FormallyUnramified (X.genericExtensionMorphism L).fromNormalization ∧
      LocallyOfFiniteType (X.genericExtensionMorphism L).fromNormalization)
    (σ : L ≃ₐ[X.functionField] L) (y : (X.genericExtensionMorphism L).normalization)
    (hy : Inertia.normalizationEndomorphism (X.genericExtensionMorphism L)
      (Spec.map (CommRingCat.ofHom σ.toRingHom))
      (genericExtensionMorphism_specMap_algEquiv X L σ) y = y)
    (hres : (Inertia.normalizationEndomorphism (X.genericExtensionMorphism L)
        (Spec.map (CommRingCat.ofHom σ.toRingHom))
        (genericExtensionMorphism_specMap_algEquiv X L σ)).residueFieldMap y =
      ((X.genericExtensionMorphism L).normalization.residueFieldCongr hy).hom) :
    σ = 1

Module documentation

Global geometric-point rigidity for an unramified normalization

Declarations

fieldSpecQuasiCompact

fieldAlgEquiv_eq_one_of_specMap_eq_id

genericExtensionMorphism_specMap_algEquiv

genericNormalization_automorphism_eq_one_of_fixed_fieldPoint

genericNormalization_automorphism_eq_one_of_trivial_residue