Tame and wild ramification

DefinitionResidue separability at a prime#✓fully proved

Let \(R\) and \(S\) be commutative rings with \(S\) an \(R\)-algebra, let \(q\) be a prime ideal of \(S\), and let \(p\) be its preimage in \(R\). Then \(q\) is residue separable over \(R\) when the residue field \(\kappa(q)\) is separable over the residue field \(\kappa(p)\), for the algebra structure induced by the canonical local homomorphism \(R_p \to S_q\) of localizations.

def IsResidueSeparableAt : Prop :=
  letI := Localization.AtPrime.algebraOfLiesOver (q.under R) q;
    Algebra.IsSeparable (q.under R).ResidueField q.ResidueField

Used by 12

Used byResidue separability, unfolded · Unramified primes are residue separable · Tame primes are residue separable · Tamely ramified prime · Characterization of tame ramification · Tameness in residue characteristic zero · Criterion for tame ramification · Unramified primes are tamely ramified · Wild ramification under residue separability · Divisibility of the ramification index forces wild ramification · An inseparable residue field extension forces wild ramification · The residue characteristic of a tame prime does not divide its ramification index

DefinitionTamely ramified prime#✓fully proved

Let \(R\) and \(S\) be commutative rings with \(S\) an \(R\)-algebra, and let \(q\) be a prime ideal of \(S\). Then \(q\) is tamely ramified over \(R\) when \(q\) is residue separable over \(R\) and the characteristic of the residue field \(\kappa(q)\) does not divide the ramification index of \(q\) over \(R\).

def IsTamelyRamifiedAt : Prop :=
  IsResidueSeparableAt R q ∧ ¬ ringChar q.ResidueField ∣ q.ramificationIdx R

Uses 1 · Used by 11

Statement usesResidue separability at a prime

Used byTame primes are residue separable · Characterization of tame ramification · Tameness in residue characteristic zero · Criterion for tame ramification · Unramified primes are tamely ramified · Wildly ramified prime · Wild ramification is the failure of tame ramification · Wild ramification under residue separability · Divisibility of the ramification index forces wild ramification · An inseparable residue field extension forces wild ramification · The residue characteristic of a tame prime does not divide its ramification index

DefinitionWildly ramified prime#✓fully proved

Let \(R\) be a commutative ring, \(S\) a commutative \(R\)-algebra and \(q\) a prime ideal of \(S\). Then \(q\) is wildly ramified over \(R\) if it is not tamely ramified over \(R\).

def IsWildlyRamifiedAt : Prop :=
  ¬ IsTamelyRamifiedAt R q

Uses 1 · Used by 4

Statement usesTamely ramified prime

Used byWild ramification is the failure of tame ramification · Wild ramification under residue separability · Divisibility of the ramification index forces wild ramification · An inseparable residue field extension forces wild ramification

TheoremResidue separability, unfolded#✓fully proved

Let \(R\) and \(S\) be commutative rings with \(S\) an \(R\)-algebra, let \(q\) be a prime ideal of \(S\), and let \(p\) be its preimage in \(R\). Then \(q\) is residue separable over \(R\) if and only if the residue field \(\kappa(q)\) is separable over the residue field \(\kappa(p)\), for the algebra structure induced by the canonical local homomorphism \(R_p \to S_q\) of localizations.

theorem isResidueSeparableAt_iff :
    IsResidueSeparableAt R q ↔
      letI := Localization.AtPrime.algebraOfLiesOver (q.under R) q;
      Algebra.IsSeparable (q.under R).ResidueField q.ResidueField

Uses 1

Statement usesResidue separability at a prime

TheoremCharacterization of tame ramification#✓fully proved

Let \(R\) and \(S\) be commutative rings with \(S\) an \(R\)-algebra, and let \(q\) be a prime ideal of \(S\). Then \(q\) is tamely ramified over \(R\) if and only if \(q\) is residue separable over \(R\) and the characteristic of the residue field \(\kappa(q)\) does not divide the ramification index of \(q\) over \(R\).

theorem isTamelyRamifiedAt_iff :
    IsTamelyRamifiedAt R q ↔
      IsResidueSeparableAt R q ∧
        ¬ ringChar q.ResidueField ∣ q.ramificationIdx R

Uses 2 · Used by 1

Statement usesResidue separability at a prime · Tamely ramified prime

Used byTameness in residue characteristic zero

TheoremWild ramification is the failure of tame ramification#✓fully proved

Let \(R\) be a commutative ring, \(S\) a commutative \(R\)-algebra and \(q\) a prime ideal of \(S\). Then \(q\) is wildly ramified over \(R\) if and only if \(q\) is not tamely ramified over \(R\).

theorem isWildlyRamifiedAt_iff :
    IsWildlyRamifiedAt R q ↔ ¬ IsTamelyRamifiedAt R q

Uses 2

Statement usesTamely ramified prime · Wildly ramified prime

TheoremCriterion for tame ramification#✓fully proved

Let \(R\) and \(S\) be commutative rings with \(S\) an \(R\)-algebra, and let \(q\) be a prime ideal of \(S\). If \(q\) is residue separable over \(R\) and the characteristic of the residue field \(\kappa(q)\) does not divide the ramification index of \(q\) over \(R\), then \(q\) is tamely ramified over \(R\).

theorem isTamelyRamifiedAt_mk (hsep : IsResidueSeparableAt R q)
    (hchar : ¬ ringChar q.ResidueField ∣ q.ramificationIdx R) :
    IsTamelyRamifiedAt R q

Uses 2

Statement usesResidue separability at a prime · Tamely ramified prime

TheoremTame primes are residue separable#✓fully proved

Let \(R\) and \(S\) be commutative rings with \(S\) an \(R\)-algebra, and let \(q\) be a prime ideal of \(S\). If \(q\) is tamely ramified over \(R\), then \(q\) is residue separable over \(R\).

theorem IsTamelyRamifiedAt.isSeparable (h : IsTamelyRamifiedAt R q) :
    IsResidueSeparableAt R q

Uses 2

Statement usesResidue separability at a prime · Tamely ramified prime

TheoremThe residue characteristic of a tame prime does not divide its ramification index#✓fully proved

Let \(R\) be a commutative ring, \(S\) a commutative \(R\)-algebra and \(q\) a prime ideal of \(S\) with residue field \(\kappa(q)\). If \(q\) is tamely ramified over \(R\), then the characteristic of \(\kappa(q)\) does not divide the ramification index of \(q\) over \(R\).

theorem IsTamelyRamifiedAt.not_dvd (h : IsTamelyRamifiedAt R q) :
    ¬ ringChar q.ResidueField ∣ q.ramificationIdx R

Uses 2

Statement usesTamely ramified prime

Proof usesResidue separability at a prime

TheoremWild ramification under residue separability#✓fully proved

Let \(R\) and \(S\) be commutative rings with \(S\) an \(R\)-algebra, and let \(q\) be a prime ideal of \(S\) that is residue separable over \(R\). Then \(q\) is wildly ramified over \(R\) if and only if the characteristic of the residue field \(\kappa(q)\) divides the ramification index of \(q\) over \(R\).

theorem isWildlyRamifiedAt_iff_char_dvd (hsep : IsResidueSeparableAt R q) :
    IsWildlyRamifiedAt R q ↔ ringChar q.ResidueField ∣ q.ramificationIdx R

Uses 3

Statement usesResidue separability at a prime · Wildly ramified prime

Proof usesTamely ramified prime

TheoremDivisibility of the ramification index forces wild ramification#✓fully proved

Let \(R\) be a commutative ring, \(S\) a commutative \(R\)-algebra and \(q\) a prime ideal of \(S\) with residue field \(\kappa(q)\). If the characteristic of \(\kappa(q)\) divides the ramification index of \(q\) over \(R\), then \(q\) is wildly ramified over \(R\).

No separability hypothesis on the residue field extension is needed.

theorem isWildlyRamifiedAt_of_char_dvd
    (hdvd : ringChar q.ResidueField ∣ q.ramificationIdx R) :
    IsWildlyRamifiedAt R q

Uses 3

Statement usesWildly ramified prime

Proof usesResidue separability at a prime · Tamely ramified prime

TheoremAn inseparable residue field extension forces wild ramification#✓fully proved

Let \(R\) be a commutative ring, \(S\) a commutative \(R\)-algebra, \(q\) a prime ideal of \(S\) and \(p\) the preimage of \(q\) in \(R\). If the residue field extension \(\kappa(p) \to \kappa(q)\) is not separable, then \(q\) is wildly ramified over \(R\).

theorem isWildlyRamifiedAt_of_not_isResidueSeparableAt
    (h : ¬ IsResidueSeparableAt R q) : IsWildlyRamifiedAt R q

Uses 3

Statement usesResidue separability at a prime · Wildly ramified prime

Proof usesTamely ramified prime

TheoremUnramified primes are residue separable#✓fully proved

Let \(R\) and \(S\) be commutative rings with \(S\) an \(R\)-algebra that is essentially of finite type, and let \(q\) be a prime ideal of \(S\) at which \(S\) is unramified over \(R\), that is, the localization \(S_q\) is formally unramified over \(R\). Then \(q\) is residue separable over \(R\).

theorem isResidueSeparableAt_of_isUnramifiedAt [Algebra.EssFiniteType R S]
    [Algebra.IsUnramifiedAt R q] : IsResidueSeparableAt R q

Uses 1 · Used by 1

Statement usesResidue separability at a prime

Used byUnramified primes are tamely ramified

TheoremUnramified primes are tamely ramified#✓fully proved

Let \(R\) and \(S\) be commutative rings with \(S\) an \(R\)-algebra that is essentially of finite type, and let \(q\) be a prime ideal of \(S\) at which \(S\) is unramified over \(R\), that is, the localization \(S_q\) is formally unramified over \(R\). Then \(q\) is tamely ramified over \(R\).

theorem isTamelyRamifiedAt_of_isUnramifiedAt [Algebra.EssFiniteType R S]
    [Algebra.IsUnramifiedAt R q] : IsTamelyRamifiedAt R q

Uses 3

Statement usesTamely ramified prime

Proof usesResidue separability at a prime · Unramified primes are residue separable

TheoremTameness in residue characteristic zero#✓fully proved

Let \(R\) and \(S\) be commutative rings with \(S\) an \(R\)-algebra that is finite as an \(R\)-module, and let \(q\) be a prime ideal of \(S\) whose residue field \(\kappa(q)\) has characteristic \(0\). Then \(q\) is tamely ramified over \(R\) if and only if \(q\) is residue separable over \(R\).

theorem isTamelyRamifiedAt_iff_isSeparable_of_charZero [Module.Finite R S]
    (hchar : ringChar q.ResidueField = 0) :
    IsTamelyRamifiedAt R q ↔ IsResidueSeparableAt R q

Uses 3

Statement usesResidue separability at a prime · Tamely ramified prime

Proof usesCharacterization of tame ramification

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.