Module

FiniteInertiaCardinality.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FiniteInertiaCardinality

4 declarations indexed from sourceView source ↗

Module documentation

Finite inertia cardinality with inseparable residue degree

The residue extension need not be separable. Its automorphism group has order its separable degree. Cancelling this factor from the actual decomposition identity gives |I| = e * f_insep, which is the cardinal input for Stacks 0BUA.

Imports3

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

Imported by2

theorem

card_aut_eq_finSepDegree_of_normal

L24 ↗

HilbertRamification.Dedekind.card_aut_eq_finSepDegree_of_normal

Documentation

Normality identifies field automorphisms with all field embeddings.

Source context 2 commands

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

noncomputable section
namespace HilbertRamification.Dedekind

Lean source · statement

theorem card_aut_eq_finSepDegree_of_normal
    (k l : Type*) [Field k] [Field l] [Algebra k l] [Normal k l] :
    Nat.card (l ≃ₐ[k] l) = Field.finSepDegree k l

theorem

decompositionQuotientInertia_card_eq_finSepDegree

L39 ↗

HilbertRamification.Dedekind.decompositionQuotientInertia_card_eq_finSepDegree

Documentation

The residue quotient of decomposition has the separable residue degree, without a separability hypothesis on the residue extension.

Source context 3 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem decompositionQuotientInertia_card_eq_finSepDegree
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) [p.IsMaximal] (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    Nat.card (decompositionGroup Q G ⧸
      (inertiaGroup Q G).subgroupOf (decompositionGroup Q G)) =
      Field.finSepDegree (A ⧸ p) (B ⧸ Q)

theorem

decomposition_card_eq_finSepDegree_mul_inertia_card

L54 ↗

HilbertRamification.Dedekind.decomposition_card_eq_finSepDegree_mul_inertia_card

Documentation

The actual finite decomposition order factors through the separable residue degree and the actual ideal inertia group.

Source context 3 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem decomposition_card_eq_finSepDegree_mul_inertia_card
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) [p.IsMaximal] (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    Nat.card (decompositionGroup Q G) =
      Field.finSepDegree (A ⧸ p) (B ⧸ Q) * Nat.card (inertiaGroup Q G)

theorem

inertia_card_eq_ramificationIdx_mul_finInsepDegree

L66 ↗

HilbertRamification.Dedekind.inertia_card_eq_ramificationIdx_mul_finInsepDegree

Documentation

The original finite inertia cardinality, including the inseparable residue factor. No perfectness or residue-separability premise is imposed.

Source context 3 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem inertia_card_eq_ramificationIdx_mul_finInsepDegree
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
    [IsDedekindDomain A] [IsDedekindDomain B]
    [Module.Finite A B] [Module.IsTorsionFree A B]
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥)
    (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    Nat.card (inertiaGroup Q G) =
      Q.ramificationIdx A * Field.finInsepDegree (A ⧸ p) (B ⧸ Q)

Module documentation

Finite inertia cardinality with inseparable residue degree

Declarations

card_aut_eq_finSepDegree_of_normal

decompositionQuotientInertia_card_eq_finSepDegree

decomposition_card_eq_finSepDegree_mul_inertia_card

inertia_card_eq_ramificationIdx_mul_finInsepDegree