Module

Tame.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.Residue.Tame

3 declarations indexed from sourceView source ↗

Module documentation

Tame inertia forces a separable residue extension

This file supplies the residue-field step in the SGA 1 form of Abhyankar's lemma. It works at an arbitrary nonzero maximal ideal of a finite Galois extension of Dedekind domains; no completeness or Henselian hypothesis is used.

Imports2

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.Basic
Mathlib.FieldTheory.PurelyInseparable.Basic

Imported by3

theorem

residueModule_finite_of_liesOver

L30 ↗

TameAbhyankar.SGA1.residueModule_finite_of_liesOver

Documentation

A finite algebra remains finite after passing to residue rings at a pair of ideals with the upper ideal lying over the lower one.

Source context 5 commands

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

noncomputable section
namespace TameAbhyankar.SGA1
open Algebra Module
open HilbertRamification.Dedekind
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem residueModule_finite_of_liesOver
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Module.Finite R S]
    (p : Ideal R) (P : Ideal S) [P.LiesOver p] :
    Module.Finite (R ⧸ p) (S ⧸ P)

theorem

inertia_card_eq_ramificationIdx_mul_finInsepDegree

L60 ↗

TameAbhyankar.SGA1.inertia_card_eq_ramificationIdx_mul_finInsepDegree

Documentation

For a finite Galois extension of Dedekind domains, the inertia-group cardinality at a nonzero maximal ideal is the ramification index times the inseparable degree of the residue-field extension.

This is the form of the inertia-cardinality formula that does not assume the residue extension is separable.

Source context 11 commands

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

noncomputable section
namespace TameAbhyankar.SGA1
open Algebra Module
open HilbertRamification.Dedekind
attribute [local instance] Ideal.Quotient.field
variable {A B G : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [IsDedekindDomain A] [IsDedekindDomain B]
variable [Module.Finite A B] [IsTorsionFree A B]
variable [Group G] [Finite G] [MulSemiringAction G B]
variable [IsGaloisGroup G A B]

Lean source · statement

theorem inertia_card_eq_ramificationIdx_mul_finInsepDegree
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥)
    (P : Ideal B) [P.IsMaximal] [P.LiesOver p] :
    Nat.card (P.toAddSubgroup.inertia G) =
      p.ramificationIdx' P *
        Field.finInsepDegree (A ⧸ p) (B ⧸ P)

theorem

residue_isSeparable_of_inertia_card_coprime_ringExpChar

L123 ↗

TameAbhyankar.SGA1.residue_isSeparable_of_inertia_card_coprime_ringExpChar

Documentation

If the inertia-group cardinality is prime to the exponential characteristic of the residue field, then the residue-field extension is separable.

Source context 11 commands

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

noncomputable section
namespace TameAbhyankar.SGA1
open Algebra Module
open HilbertRamification.Dedekind
attribute [local instance] Ideal.Quotient.field
variable {A B G : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [IsDedekindDomain A] [IsDedekindDomain B]
variable [Module.Finite A B] [IsTorsionFree A B]
variable [Group G] [Finite G] [MulSemiringAction G B]
variable [IsGaloisGroup G A B]

Lean source · statement

theorem residue_isSeparable_of_inertia_card_coprime_ringExpChar
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥)
    (P : Ideal B) [P.IsMaximal] [P.LiesOver p]
    (hcop : Nat.Coprime (Nat.card (P.toAddSubgroup.inertia G))
      (ringExpChar (A ⧸ p))) :
    Algebra.IsSeparable (A ⧸ p) (B ⧸ P)

Module documentation

Tame inertia forces a separable residue extension

Declarations

residueModule_finite_of_liesOver

inertia_card_eq_ramificationIdx_mul_finInsepDegree

residue_isSeparable_of_inertia_card_coprime_ringExpChar