NYLL
Module

FiniteIdealTameFactorization.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteIdealTameFactorization
2 declarations indexed from sourceView source ↗

Module documentation

Tame and wild orders with inseparable residue degree

The actual finite tame and principal-unit wild orders multiply to the ramification index times the inseparable degree of the native residue extension. The existential factorization interface follows from this explicit identity.

Imports3
Imported by4

Declarations

theorem

finiteIdealTameOrder_mul_wildOrder_eq_ramificationIdx_mul_finInsepDegree

L29 ↗
EtaleFundamentalGroups.Inertia.finiteIdealTameOrder_mul_wildOrder_eq_ramificationIdx_mul_finInsepDegree
Documentation

The actual original finite tame and wild orders satisfy the ramification identity with the inseparable degree of the actual residue extension. Both residue fields and their coefficient action are the native ideal quotients.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem finiteIdealTameOrder_mul_wildOrder_eq_ramificationIdx_mul_finInsepDegree
    (A : Type u) (B : Type v)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [CommRing B] [IsDedekindDomain B] [Algebra A B]
    [Module.Finite A B] [Module.IsTorsionFree A B]
    (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver (IsLocalRing.maximalIdeal A)] (hQ : Q ≠ ⊥)
    (G : Type w) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] :
    finiteIdealTameOrder B G Q hQ * finiteIdealWildOrder B G Q hQ =
      Q.ramificationIdx A *
        Field.finInsepDegree (A ⧸ IsLocalRing.maximalIdeal A) (B ⧸ Q)
theorem

finiteIdealTameOrder_mul_wildOrder_eq_ramificationIdx_mul

L49 ↗
EtaleFundamentalGroups.Inertia.finiteIdealTameOrder_mul_wildOrder_eq_ramificationIdx_mul
Documentation

The original existential interface follows from the explicit inseparable residue-degree identity.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem finiteIdealTameOrder_mul_wildOrder_eq_ramificationIdx_mul
    (A : Type u) (B : Type v)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [CommRing B] [IsDedekindDomain B] [Algebra A B]
    [Module.Finite A B] [Module.IsTorsionFree A B]
    (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver (IsLocalRing.maximalIdeal A)] (hQ : Q ≠ ⊥)
    (G : Type w) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] :
    ∃ f : ℕ, finiteIdealTameOrder B G Q hQ * finiteIdealWildOrder B G Q hQ =
      Q.ramificationIdx A * f

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