Module

CyclotomicInversion.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.CyclicInertia.CyclotomicInversion

15 declarations indexed from sourceView source ↗

Module documentation

Cyclotomic inversion and tame inertia

This file constructs the rational cyclotomic automorphism with character -1, transports it to a separable closure of a regular characteristic-zero field, and connects its residue lift to conjugation on finite tame inertia.

Imports5

Imported by2

theorem

exists_rationalCyclotomicAutomorphism_inverting_torsionUnits

L32 ↗

EtaleFundamentalGroups.exists_rationalCyclotomicAutomorphism_inverting_torsionUnits

Documentation

The rational cyclotomic extension has an automorphism which inverts every finite-order unit.

Source context 4 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups
open ClassFormation KummerTheory

Lean source · statement

theorem exists_rationalCyclotomicAutomorphism_inverting_torsionUnits :
    ∃ sigma : rationalCyclotomicField ≃ₐ[ℚ] rationalCyclotomicField,
      ∀ z : rationalCyclotomicFieldˣ, IsOfFinOrder z →
        Units.mapEquiv sigma.toMulEquiv z = z⁻¹

theorem

exists_rationalCyclotomicAutomorphism_inverting_torsion

L160 ↗

EtaleFundamentalGroups.exists_rationalCyclotomicAutomorphism_inverting_torsion

Source context 4 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups
open ClassFormation KummerTheory

Lean source · statement

theorem exists_rationalCyclotomicAutomorphism_inverting_torsion :
    ∃ sigma : rationalCyclotomicField ≃ₐ[ℚ] rationalCyclotomicField,
      ∀ z : rationalCyclotomicField, IsOfFinOrder z → sigma z = z⁻¹

theorem

exists_separableClosureRatAutomorphism_inverting_torsion

L185 ↗

EtaleFundamentalGroups.exists_separableClosureRatAutomorphism_inverting_torsion

Documentation

The separable closure of ℚ has an automorphism which inverts every finite-order element.

Source context 4 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups
open ClassFormation KummerTheory

Lean source · statement

theorem exists_separableClosureRatAutomorphism_inverting_torsion :
    ∃ sigma : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ,
      ∀ z : SeparableClosure ℚ, IsOfFinOrder z → sigma z = z⁻¹

theorem

exists_separableClosureAutomorphism_inverting_torsion_of_ratEquiv

L228 ↗

EtaleFundamentalGroups.exists_separableClosureAutomorphism_inverting_torsion_of_ratEquiv

Documentation

If a field is isomorphic to ℚ, a separable closure of ℚ, regarded through that isomorphism as an extension of the field, has an automorphism which inverts every finite-order element. This formulation includes universe lifts of ℚ.

Source context 4 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups
open ClassFormation KummerTheory

Lean source · full declaration

theorem exists_separableClosureAutomorphism_inverting_torsion_of_ratEquiv
    (k : Type u) [Field k] [PerfectField k] (e : k ≃+* ℚ) :
    letI : Algebra k (SeparableClosure ℚ) :=
      ((algebraMap ℚ (SeparableClosure ℚ)).comp e.toRingHom).toAlgebra
    ∃ sigma : SeparableClosure ℚ ≃ₐ[k] SeparableClosure ℚ,
      ∀ z : SeparableClosure ℚ, IsOfFinOrder z → sigma z = z⁻¹ := by
  let : Algebra k (SeparableClosure ℚ) :=
    ((algebraMap ℚ (SeparableClosure ℚ)).comp e.toRingHom).toAlgebra
  obtain ⟨sigmaQ, hsigmaQ⟩ :=
    exists_separableClosureRatAutomorphism_inverting_torsion
  refine ⟨AlgEquiv.ofRingEquiv (f := sigmaQ.toRingEquiv) ?_, hsigmaQ⟩
  intro x
  exact sigmaQ.commutes (e x)

theorem

exists_algEquiv_inverting_torsionUnits_of_separableClosure_linearDisjoint

L248 ↗

EtaleFundamentalGroups.exists_algEquiv_inverting_torsionUnits_of_separableClosure_linearDisjoint

Documentation

Let F / ℚ be a field and let Omega be a separable closure of F. If F is linearly disjoint from the separable closure of ℚ inside Omega, then an F-automorphism of Omega inverts every finite-order unit. The linear-disjointness hypothesis is the field-theoretic form of regularity used for geometrically integral characteristic-zero generic fibres.

Source context 4 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups
open ClassFormation KummerTheory

Lean source · statement

theorem exists_algEquiv_inverting_torsionUnits_of_separableClosure_linearDisjoint
    {F : Type u} {Omega : Type v}
    [Field F] [Field Omega]
    [Algebra ℚ F] [Algebra F Omega] [Algebra ℚ Omega]
    [IsScalarTower ℚ F Omega] [IsSepClosure F Omega]
    (hdisjoint : (separableClosure ℚ Omega).LinearDisjoint F) :
    ∃ tau : Omega ≃ₐ[F] Omega,
      ∀ z : Omegaˣ, IsOfFinOrder z →
        Units.mapEquiv tau.toMulEquiv z = z⁻¹

theorem

exists_algEquiv_inverting_torsionUnits_of_separableClosure_linearDisjoint_of_ratEquiv

L319 ↗

EtaleFundamentalGroups.exists_algEquiv_inverting_torsionUnits_of_separableClosure_linearDisjoint_of_ratEquiv

Documentation

Cyclotomic inversion over a rational base field presented by a ring equivalence with ℚ. This version applies directly to ULift ℚ, so it is compatible with arithmetic schemes in an arbitrary universe.

Source context 4 commands

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

noncomputable section
universe u v w
namespace EtaleFundamentalGroups
open ClassFormation KummerTheory

Lean source · statement

theorem exists_algEquiv_inverting_torsionUnits_of_separableClosure_linearDisjoint_of_ratEquiv
    {k : Type u} {F : Type v} {Omega : Type w}
    [Field k] [PerfectField k] [Field F] [Field Omega]
    [Algebra k F] [Algebra F Omega] [Algebra k Omega]
    [IsScalarTower k F Omega] [IsSepClosure F Omega]
    (e : k ≃+* ℚ)
    (hdisjoint : (separableClosure k Omega).LinearDisjoint F) :
    ∃ tau : Omega ≃ₐ[F] Omega,
      ∀ z : Omegaˣ, IsOfFinOrder z →
        Units.mapEquiv tau.toMulEquiv z = z⁻¹

theorem

exists_inertiaConjugate_eq_inv_of_residue_linearDisjoint

L404 ↗

TameAbhyankar.SGA1.exists_inertiaConjugate_eq_inv_of_residue_linearDisjoint

Documentation

If the characteristic-zero decomposition residue field is regular over ℚ in the linear-disjointness form, one decomposition element conjugates every element of finite tame inertia to its inverse.

Source context 5 commands

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

noncomputable section
universe u v w
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · full declaration

theorem exists_inertiaConjugate_eq_inv_of_residue_linearDisjoint
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    [IsGalois K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    [CharZero (decompositionResidueField K V)]
    [Finite (inertiaGroup K V)]
    [IsSepClosure (decompositionResidueField K V) (selectedResidueField V)] :
    letI : CharZero (selectedResidueField V) :=
      charZero_of_injective_algebraMap
        (algebraMap (decompositionResidueField K V)
          (selectedResidueField V)).injective
    letI : Algebra ℚ (decompositionResidueField K V) :=
      DivisionRing.toRatAlgebra
    letI : Algebra ℚ (selectedResidueField V) :=
      DivisionRing.toRatAlgebra
    letI : IsScalarTower ℚ (decompositionResidueField K V)
        (selectedResidueField V) :=
      IsScalarTower.of_algebraMap_eq fun q => by simp
    (
      (separableClosure ℚ (selectedResidueField V)).LinearDisjoint
        (decompositionResidueField K V)) →
    ∃ g : decompositionGroup K V,
      ∀ sigma : inertiaGroup K V,
        inertiaConjugate K V g sigma = sigma⁻¹ := by
  intro hdisjoint
  let : CharZero (selectedResidueField V) :=
    charZero_of_injective_algebraMap
      (algebraMap (decompositionResidueField K V)
        (selectedResidueField V)).injective
  obtain ⟨tau, htau⟩ :=
    EtaleFundamentalGroups.exists_algEquiv_inverting_torsionUnits_of_separableClosure_linearDisjoint
        (F := decompositionResidueField K V)
        (Omega := selectedResidueField V) hdisjoint
  obtain ⟨g, hg, hresidue⟩ :=
    exists_galoisAutomorphism_stabilizing_of_residueAutomorphism K V tau
  let g' : decompositionGroup K V := ⟨g, hg⟩
  refine ⟨g', ?_⟩
  intro sigma
  apply inertiaConjugate_eq_inv_of_torsion_residue_inversion K V g'
  intro z hz
  have haction :
      residueAction K V g' (z : selectedResidueField V) =
        tau (z : selectedResidueField V) := by
    exact DFunLike.congr_fun hresidue (z : selectedResidueField V)
  apply Units.ext
  rw [Units.coe_mapEquiv, Units.val_inv_eq_inv_val]
  change residueAction K V g' (z : selectedResidueField V) =
    (z : selectedResidueField V)⁻¹
  rw [haction]
  have hinv := congrArg Units.val (htau z hz)
  rw [Units.coe_mapEquiv, Units.val_inv_eq_inv_val] at hinv
  exact hinv

theorem

inertia_isConj_inv_of_residue_linearDisjoint

L459 ↗

TameAbhyankar.SGA1.inertia_isConj_inv_of_residue_linearDisjoint

Documentation

Under the same regularity input, every finite inertia element is conjugate to its inverse inside the decomposition group.

Source context 5 commands

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

noncomputable section
universe u v w
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · full declaration

theorem inertia_isConj_inv_of_residue_linearDisjoint
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    [IsGalois K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    [CharZero (decompositionResidueField K V)]
    [Finite (inertiaGroup K V)]
    [IsSepClosure (decompositionResidueField K V) (selectedResidueField V)] :
    letI : CharZero (selectedResidueField V) :=
      charZero_of_injective_algebraMap
        (algebraMap (decompositionResidueField K V)
          (selectedResidueField V)).injective
    letI : Algebra ℚ (decompositionResidueField K V) :=
      DivisionRing.toRatAlgebra
    letI : Algebra ℚ (selectedResidueField V) :=
      DivisionRing.toRatAlgebra
    letI : IsScalarTower ℚ (decompositionResidueField K V)
        (selectedResidueField V) :=
      IsScalarTower.of_algebraMap_eq fun q => by simp
    (
      (separableClosure ℚ (selectedResidueField V)).LinearDisjoint
        (decompositionResidueField K V)) →
    ∀ sigma : inertiaGroup K V,
      IsConj (sigma : decompositionGroup K V)
        ((sigma⁻¹ : inertiaGroup K V) : decompositionGroup K V) := by
  intro hdisjoint
  obtain ⟨g, hg⟩ :=
    exists_inertiaConjugate_eq_inv_of_residue_linearDisjoint K V hdisjoint
  intro sigma
  refine isConj_iff.mpr ⟨g, ?_⟩
  exact congrArg Subtype.val (hg sigma)

theorem

exists_inertiaConjugate_eq_inv_of_residue_linearDisjoint_of_ratEquiv

L492 ↗

TameAbhyankar.SGA1.exists_inertiaConjugate_eq_inv_of_residue_linearDisjoint_of_ratEquiv

Documentation

Cyclotomic inversion in finite inertia over any rational base field presented by an equivalence with ℚ.

Source context 5 commands

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

noncomputable section
universe u v w
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem exists_inertiaConjugate_eq_inv_of_residue_linearDisjoint_of_ratEquiv
    (k : Type v) [Field k] [PerfectField 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]
    [CharZero (decompositionResidueField K V)]
    [Finite (inertiaGroup K V)]
    [IsSepClosure (decompositionResidueField K V) (selectedResidueField V)]
    [Algebra k (decompositionResidueField K V)]
    [Algebra k (selectedResidueField V)]
    [IsScalarTower k (decompositionResidueField K V)
      (selectedResidueField V)]
    (hdisjoint :
      (separableClosure k (selectedResidueField V)).LinearDisjoint
        (decompositionResidueField K V)) :
    ∃ g : decompositionGroup K V,
      ∀ sigma : inertiaGroup K V,
        inertiaConjugate K V g sigma = sigma⁻¹

theorem

inertia_isConj_inv_of_residue_linearDisjoint_of_ratEquiv

L541 ↗

TameAbhyankar.SGA1.inertia_isConj_inv_of_residue_linearDisjoint_of_ratEquiv

Documentation

Under the rational-base regularity input, every finite inertia element is conjugate to its inverse inside the decomposition group.

Source context 5 commands

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

noncomputable section
universe u v w
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem inertia_isConj_inv_of_residue_linearDisjoint_of_ratEquiv
    (k : Type v) [Field k] [PerfectField 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]
    [CharZero (decompositionResidueField K V)]
    [Finite (inertiaGroup K V)]
    [IsSepClosure (decompositionResidueField K V) (selectedResidueField V)]
    [Algebra k (decompositionResidueField K V)]
    [Algebra k (selectedResidueField V)]
    [IsScalarTower k (decompositionResidueField K V)
      (selectedResidueField V)]
    (hdisjoint :
      (separableClosure k (selectedResidueField V)).LinearDisjoint
        (decompositionResidueField K V)) :
    ∀ sigma : inertiaGroup K V,
      IsConj (sigma : decompositionGroup K V)
        ((sigma⁻¹ : inertiaGroup K V) : decompositionGroup K V)

theorem

inertia_isConj_inv_of_geometricallyIntegral_residue_of_ratEquiv

L569 ↗

TameAbhyankar.SGA1.inertia_isConj_inv_of_geometricallyIntegral_residue_of_ratEquiv

Documentation

Geometric integrality over a rational base field, including a universe lift of ℚ, directly supplies conjugacy of every finite inertia element with its inverse.

Source context 5 commands

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

noncomputable section
universe u v w
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem inertia_isConj_inv_of_geometricallyIntegral_residue_of_ratEquiv
    (k : Type v) [Field k] [PerfectField 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]
    [CharZero (decompositionResidueField K V)]
    [Finite (inertiaGroup K V)]
    [IsSepClosure (decompositionResidueField K V) (selectedResidueField 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)

L593 ↗

Source context 6 commands

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

noncomputable section
universe u v w
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
section IntegerBase

Lean source · statement

instance : IsDomain (ULift.{v} ℤ)

abbrev

integerGenericResidueField

L596 ↗

TameAbhyankar.SGA1.integerGenericResidueField

Source context 7 commands

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

noncomputable section
universe u v w
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_residue_over_integers

L607 ↗

TameAbhyankar.SGA1.inertia_isConj_inv_of_geometricallyIntegral_residue_over_integers

Documentation

Geometric integrality over the generic residue field of the integer base supplies conjugacy of every finite inertia element with its inverse.

The rational base field and its perfectness are consequences of the generic point of Spec (ULift ℤ); they are not additional hypotheses.

Source context 7 commands

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

noncomputable section
universe u v w
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_residue_over_integers
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    [IsGalois K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    [CharZero (decompositionResidueField K V)]
    [Finite (inertiaGroup K V)]
    [IsSepClosure (decompositionResidueField K V) (selectedResidueField 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)

theorem

inertia_isConj_inv_of_geometricallyIntegral_residue

L638 ↗

TameAbhyankar.SGA1.inertia_isConj_inv_of_geometricallyIntegral_residue

Documentation

Geometric integrality of the characteristic-zero decomposition residue field supplies the linear disjointness needed for cyclotomic inversion. Consequently every finite inertia element is conjugate to its inverse.

Source context 5 commands

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

noncomputable section
universe u v w
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · full declaration

theorem inertia_isConj_inv_of_geometricallyIntegral_residue
    (K : Type) {L : Type} [Field K] [Field L] [Algebra K L]
    [IsGalois K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    [CharZero (decompositionResidueField K V)]
    [Finite (inertiaGroup K V)]
    [IsSepClosure (decompositionResidueField K V) (selectedResidueField V)] :
    letI : CharZero (selectedResidueField V) :=
      charZero_of_injective_algebraMap
        (algebraMap (decompositionResidueField K V)
          (selectedResidueField V)).injective
    letI : Algebra ℚ (decompositionResidueField K V) :=
      DivisionRing.toRatAlgebra
    letI : Algebra ℚ (selectedResidueField V) :=
      DivisionRing.toRatAlgebra
    letI : IsScalarTower ℚ (decompositionResidueField K V)
        (selectedResidueField V) :=
      IsScalarTower.of_algebraMap_eq fun q => by simp
    AlgebraicGeometry.GeometricallyIntegral
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom
        (algebraMap ℚ (decompositionResidueField K V)))) →
    ∀ sigma : inertiaGroup K V,
      IsConj (sigma : decompositionGroup K V)
        ((sigma⁻¹ : inertiaGroup K V) : decompositionGroup K V) := by
  intro hgeo
  let : CharZero (selectedResidueField V) :=
    charZero_of_injective_algebraMap
      (algebraMap (decompositionResidueField K V)
        (selectedResidueField V)).injective
  apply inertia_isConj_inv_of_residue_linearDisjoint K V
  exact
    EtaleFundamentalGroups.separableClosure_linearDisjoint_of_geometricallyIntegral

Module documentation

Cyclotomic inversion and tame inertia

Declarations