NYLL
Module

FiniteLevelCyclotomicInversion.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.CyclicInertia.FiniteLevelCyclotomicInversion
5 declarations indexed from sourceView source ↗

Module documentation

Cyclotomic inversion in finite-level inertia

The normal residue extension attached to a decomposition group is embedded in a genuine separable closure. Cyclotomic inversion restricts to that normal extension and the residue exact sequence lifts it back to the decomposition group. The selected residue field itself need not be a separable closure.

Imports1
Imported by2

Declarations

theorem

exists_inertiaConjugate_eq_inv_of_geometricallyIntegral_residueExtension_of_ratEquiv

L34 ↗
TameAbhyankar.SGA1.exists_inertiaConjugate_eq_inv_of_geometricallyIntegral_residueExtension_of_ratEquiv
Documentation

Geometric integrality over a rational base produces one decomposition element which conjugates every finite inertia element to its inverse.

The selected residue field is only used as its actual normal separable extension of the decomposition residue field. In particular, it is not assumed to be a separable closure.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
Lean source · statement
theorem
    exists_inertiaConjugate_eq_inv_of_geometricallyIntegral_residueExtension_of_ratEquiv
    (k : Type v) [Field k] (e : k ≃+* ℚ)
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    [IsGalois K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    [Finite (inertiaGroup K V)]
    [Algebra k (decompositionResidueField K V)]
    [Algebra k (selectedResidueField V)]
    [IsScalarTower k (decompositionResidueField K V)
      (selectedResidueField V)]
    (hgeo : AlgebraicGeometry.GeometricallyIntegral
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom
        (algebraMap k (decompositionResidueField K V))))) :
    ∃ g : decompositionGroup K V,
      ∀ sigma : inertiaGroup K V,
        inertiaConjugate K V g sigma = sigma⁻¹
theorem

inertia_isConj_inv_of_geometricallyIntegral_residueExtension_of_ratEquiv

L97 ↗
TameAbhyankar.SGA1.inertia_isConj_inv_of_geometricallyIntegral_residueExtension_of_ratEquiv
Documentation

Under the same finite-level residue input, every inertia element is conjugate to its inverse inside the decomposition group, without identifying the selected residue field with a separable closure.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
Lean source · statement
theorem
    inertia_isConj_inv_of_geometricallyIntegral_residueExtension_of_ratEquiv
    (k : Type v) [Field k] (e : k ≃+* ℚ)
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    [IsGalois K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    [Finite (inertiaGroup K V)]
    [Algebra k (decompositionResidueField K V)]
    [Algebra k (selectedResidueField V)]
    [IsScalarTower k (decompositionResidueField K V)
      (selectedResidueField V)]
    (hgeo : AlgebraicGeometry.GeometricallyIntegral
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom
        (algebraMap k (decompositionResidueField K V))))) :
    ∀ sigma : inertiaGroup K V,
      IsConj (sigma : decompositionGroup K V)
        ((sigma⁻¹ : inertiaGroup K V) : decompositionGroup K V)
instance

(anonymous instance)

L123 ↗
Source context 6 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
section IntegerBase
Lean source · statement
instance : IsDomain (ULift.{v} ℤ)
abbrev

integerGenericResidueField

L126 ↗
TameAbhyankar.SGA1.integerGenericResidueField
Source context 7 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
section IntegerBase
local instance : IsDomain (ULift.{v} ℤ) :=
  (ULift.ringEquiv : ULift.{v} ℤ ≃+* ℤ).toMulEquiv.isDomain ℤ
Lean source · statement
abbrev integerGenericResidueField : Type v
theorem

inertia_isConj_inv_of_geometricallyIntegral_residueExtension_over_integers

L135 ↗
TameAbhyankar.SGA1.inertia_isConj_inv_of_geometricallyIntegral_residueExtension_over_integers
Documentation

The generic residue field of the integer base supplies finite-level cyclotomic inversion without requiring the selected residue field to be a separable closure.

Source context 7 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
section IntegerBase
local instance : IsDomain (ULift.{v} ℤ) :=
  (ULift.ringEquiv : ULift.{v} ℤ ≃+* ℤ).toMulEquiv.isDomain ℤ
Lean source · statement
theorem
    inertia_isConj_inv_of_geometricallyIntegral_residueExtension_over_integers
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    [IsGalois K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    [Finite (inertiaGroup K V)]
    [Algebra integerGenericResidueField (decompositionResidueField K V)]
    [Algebra integerGenericResidueField (selectedResidueField V)]
    [IsScalarTower integerGenericResidueField
      (decompositionResidueField K V) (selectedResidueField V)]
    (hgeo : AlgebraicGeometry.GeometricallyIntegral
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom
        (algebraMap integerGenericResidueField
          (decompositionResidueField K V))))) :
    ∀ sigma : inertiaGroup K V,
      IsConj (sigma : decompositionGroup K V)
        ((sigma⁻¹ : inertiaGroup K V) : decompositionGroup K V)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.