Module

AffineNormalizationGeometricPoint.lean

Nyll.EtaleFundamentalGroups.Inertia.AffineNormalizationGeometricPoint

8 declarations indexed from sourceView source ↗

Module documentation

Geometric-point inertia in an affine relative normalization

For an R-algebra B, an automorphism of B extends to the relative normalization of Spec B → Spec R by normalizationDesc. Under the canonical identification with Spec (integralClosure R B), this extension is exactly the spectrum of the restricted algebra automorphism. This compatibility is proved from the integral-closure inclusion; it is not an additional hypothesis.

Consequently, the stabilizer of an actual geometric point of the normalization is the ideal-inertia subgroup for the restricted action on the integral closure. For a point obtained from the algebraic closure of the residue field of P, the ideal is literally P. No integrality, normality, finiteness, or Galois assumption on R or B is required for this affine comparison.

Imports4

Nyll.EtaleFundamentalGroups.Inertia.AffineGeometricPoint
Nyll.SchemeTheory.Normalization.Affine
Mathlib.Algebra.Algebra.Equiv
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Imported by6

def

integralClosureAutHom

L39 ↗

EtaleFundamentalGroups.Inertia.integralClosureAutHom

Documentation

Restrict algebra automorphisms to the actual integral closure.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · full declaration

def integralClosureAutHom :
    (B ≃ₐ[R] B) →* (integralClosure R B ≃ₐ[R] integralClosure R B) where
  toFun σ := σ.mapIntegralClosure
  map_one' := by
    apply AlgEquiv.ext
    intro b
    apply Subtype.ext
    rfl
  map_mul' σ τ := by
    apply AlgEquiv.ext
    intro b
    apply Subtype.ext
    rfl

abbrev

integralClosureAutAction

L55 ↗

EtaleFundamentalGroups.Inertia.integralClosureAutAction

Documentation

The restriction action of Aut_R(B) on the integral closure of R in B. It is kept explicit, so it does not introduce a competing global instance.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

abbrev integralClosureAutAction :
    MulSemiringAction (B ≃ₐ[R] B) (integralClosure R B)

def

affineNormalizationDeck

L61 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationDeck

Documentation

Extend an actual algebra automorphism by the universal property of relative normalization, using the same normalizationDesc construction as for deck maps.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

def affineNormalizationDeck (σ : B ≃ₐ[R] B) :
    (Spec.map (CommRingCat.ofHom (algebraMap R B))).normalization ⟶
      (Spec.map (CommRingCat.ofHom (algebraMap R B))).normalization

theorem

affineNormalizationDeck_specNormalizationIso_hom

L79 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationDeck_specNormalizationIso_hom

Documentation

The canonical affine normalization isomorphism intertwines the extension by normalizationDesc with the literal restricted ring automorphism.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

theorem affineNormalizationDeck_specNormalizationIso_hom
    (σ : B ≃ₐ[R] B) :
    affineNormalizationDeck R B σ ≫ (specNormalizationIso R B).hom =
      (specNormalizationIso R B).hom ≫
        Spec.map (CommRingCat.ofHom σ.toAlgHom.mapIntegralClosure.toRingHom)

theorem

mem_idealInertia_iff_fixes_affineNormalizationGeometricPoint

L107 ↗

EtaleFundamentalGroups.Inertia.mem_idealInertia_iff_fixes_affineNormalizationGeometricPoint

Documentation

An algebra automorphism belongs to ideal inertia exactly when its actual normalization extension fixes the corresponding geometric point.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · full declaration

theorem mem_idealInertia_iff_fixes_affineNormalizationGeometricPoint
    {Ω : Type u} [Field Ω]
    (φ : integralClosure R B →+* Ω) (σ : B ≃ₐ[R] B) :
    letI : MulSemiringAction (B ≃ₐ[R] B) (integralClosure R B) :=
      integralClosureAutAction R B
    σ ∈ (RingHom.ker φ).inertia (B ≃ₐ[R] B) ↔
      (Spec.map (CommRingCat.ofHom φ) ≫ (specNormalizationIso R B).inv) ≫
          affineNormalizationDeck R B σ =
        Spec.map (CommRingCat.ofHom φ) ≫ (specNormalizationIso R B).inv := by
  let : MulSemiringAction (B ≃ₐ[R] B) (integralClosure R B) :=
    integralClosureAutAction R B
  have haction : MulSemiringAction.toRingHom (B ≃ₐ[R] B)
      (integralClosure R B) σ = σ.toAlgHom.mapIntegralClosure.toRingHom := by
    apply RingHom.ext
    intro b
    rfl
  have hfix :
      ((Spec.map (CommRingCat.ofHom φ) ≫ (specNormalizationIso R B).inv) ≫
          affineNormalizationDeck R B σ =
        Spec.map (CommRingCat.ofHom φ) ≫ (specNormalizationIso R B).inv) ↔
      Spec.map (CommRingCat.ofHom φ) ≫
          Spec.map (CommRingCat.ofHom σ.toAlgHom.mapIntegralClosure.toRingHom) =
        Spec.map (CommRingCat.ofHom φ) := by
    rw [← cancel_mono (specNormalizationIso R B).hom]
    simp only [Category.assoc, affineNormalizationDeck_specNormalizationIso_hom,
      Iso.inv_hom_id_assoc, Iso.inv_hom_id, Category.comp_id]
  have hmem := mem_idealInertia_iff_fixes_affineGeometricPoint
    (B ≃ₐ[R] B) φ σ
  rw [haction] at hmem
  exact hmem.trans hfix.symm

def

affineNormalizationGeometricPointStabilizer

L140 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationGeometricPointStabilizer

Documentation

The stabilizer uses equality of geometric-point morphisms into the relative normalization, rather than equality of their underlying topological points.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

def affineNormalizationGeometricPointStabilizer
    {Ω : Type u} [Field Ω] (φ : integralClosure R B →+* Ω) :
    Subgroup (B ≃ₐ[R] B)

theorem

affineNormalizationGeometricPointStabilizer_eq_idealInertia

L166 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationGeometricPointStabilizer_eq_idealInertia

Documentation

The actual normalization geometric-point stabilizer is the ideal-inertia subgroup for the integral-closure restriction action.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · full declaration

theorem affineNormalizationGeometricPointStabilizer_eq_idealInertia
    {Ω : Type u} [Field Ω] (φ : integralClosure R B →+* Ω) :
    letI : MulSemiringAction (B ≃ₐ[R] B) (integralClosure R B) :=
      integralClosureAutAction R B
    affineNormalizationGeometricPointStabilizer R B φ =
      (RingHom.ker φ).inertia (B ≃ₐ[R] B) := by
  let : MulSemiringAction (B ≃ₐ[R] B) (integralClosure R B) :=
    integralClosureAutAction R B
  ext σ
  exact (mem_idealInertia_iff_fixes_affineNormalizationGeometricPoint R B φ σ).symm

theorem

affineNormalizationResidueGeometricPointStabilizer_eq_idealInertia

L179 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationResidueGeometricPointStabilizer_eq_idealInertia

Documentation

For the canonical geometric point obtained from a prime's residue field, the stabilizer ideal is the given prime itself.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · full declaration

theorem affineNormalizationResidueGeometricPointStabilizer_eq_idealInertia
    (P : Ideal (integralClosure R B)) [P.IsPrime] :
    letI : MulSemiringAction (B ≃ₐ[R] B) (integralClosure R B) :=
      integralClosureAutAction R B
    affineNormalizationGeometricPointStabilizer R B
        ((algebraMap P.ResidueField (AlgebraicClosure P.ResidueField)).comp
          (algebraMap (integralClosure R B) P.ResidueField)) =
      P.inertia (B ≃ₐ[R] B) := by
  let : MulSemiringAction (B ≃ₐ[R] B) (integralClosure R B) :=
    integralClosureAutAction R B
  rw [affineNormalizationGeometricPointStabilizer_eq_idealInertia,
    RingHom.ker_comp_of_injective (algebraMap (integralClosure R B) P.ResidueField)
      (algebraMap P.ResidueField (AlgebraicClosure P.ResidueField)).injective,
    Ideal.ker_algebraMap_residueField]

Module documentation

Geometric-point inertia in an affine relative normalization

Declarations