Nyll.SchemeTheory.AbhyankarLemma.Geometry.Inertia.TrivialImpliesUnramified

Module documentation

Trivial inertia implies unramifiedness

For a finite Galois extension of Dedekind domains, cardinality one of the ideal inertia group forces both ramification index one and separability of the residue extension. Thus it gives mathlib's Algebra.IsUnramifiedAt without a separate residue-separability hypothesis.

theorem

isUnramifiedAt_of_inertia_card_eq_one

L36 ↗

TameAbhyankar.SGA1.isUnramifiedAt_of_inertia_card_eq_one

Documentation

In a finite Galois Dedekind extension, trivial ideal inertia is equivalent to the two local conditions needed for unramifiedness, and hence implies Algebra.IsUnramifiedAt.

Source context 9 commands

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

noncomputable section
namespace TameAbhyankar.SGA1
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] [Module.IsTorsionFree A B]
variable [Group G] [Finite G] [MulSemiringAction G B]
variable [IsGaloisGroup G A B]

Lean source · statement

theorem isUnramifiedAt_of_inertia_card_eq_one
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥)
    (P : Ideal B) [P.IsMaximal] [P.LiesOver p]
    (hcard : Nat.card (P.toAddSubgroup.inertia G) = 1) :
    Algebra.IsUnramifiedAt A P

Module documentation

Trivial inertia implies unramifiedness

Declarations

isUnramifiedAt_of_inertia_card_eq_one